Grace/Cumulus/NumberTheory/GCDMore.g17

Imports

Declarations

gcd.self theorem derivation
gcd.one_left theorem derivation
gcd.one_right theorem derivation
gcd.divides_iff theorem derivation
gcd.le_left theorem derivation
gcd.le_right theorem derivation
gcd.nonzero theorem derivation
gcd.nonzero_right theorem derivation
gcd.positive theorem derivation
gcd.greatest_le theorem derivation
gcd.divides_add theorem derivation
gcd.divides_mul theorem derivation
gcd.add_left theorem derivation
gcd.add_left_swap theorem derivation
gcd.add_right theorem derivation
gcd.add_right_swap theorem derivation
gcd.add_mul_left theorem derivation
gcd.add_mul_right theorem derivation
gcd.sub_left theorem derivation
gcd.sub_right theorem derivation
gcd.eq_left_iff theorem derivation
gcd.eq_right_iff theorem derivation
gcd.mul_left_self theorem derivation
gcd.mul_right_self theorem derivation
gcd.mul_self_left theorem derivation
gcd.idempotent_left theorem derivation
gcd.idempotent_right theorem derivation
gcd.consecutive theorem derivation
gcd.consecutive_left theorem derivation
gcd.associative theorem derivation
gcd.mul_right_distribute theorem derivation
gcd.mul_left_distribute theorem derivation
gcd.coprime_mul theorem derivation
gcd.coprime_mul_left theorem derivation
gcd.eq_one_iff theorem derivation
coprime.symmetric theorem derivation
coprime.divisor_one theorem derivation
coprime.cancel_right theorem derivation
coprime.mul_of_coprime theorem derivation
coprime.of_mul_left theorem derivation
coprime.of_mul_right theorem derivation
coprime.mul_iff theorem derivation
coprime.pow_left theorem derivation
coprime.pow_right theorem derivation
coprime.pow theorem derivation
coprime.mul_divides theorem derivation
Prime.gcd_of_not_divides theorem derivation
Prime.coprime_or_divides theorem derivation
Prime.divides_pow theorem derivation
Source

1-- Further laws of the greatest common divisor: units and self, order bounds,2-- shifting by multiples, subtraction, distributivity over a common factor,3-- associativity, consecutive numbers, and coprimality under products and4-- powers5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.NumberTheory.GCDMore11import CoprimeCancel12import DivisibilityMore1314theorem gcd.self (a : Nat)15  shows gcd(a, a) = a16proof17  have reflexive := divides.reflexive at a18  exact gcd.of_divides with reflexive1920theorem gcd.one_left (a : Nat)21  shows gcd(1, a) = 122proof23  have one := one.divides at a24  exact gcd.of_divides with one2526theorem gcd.one_right (a : Nat)27  shows gcd(a, 1) = 128proof29  have commute := gcd.commutative at a, 130  rw commute31  exact gcd.one_left at a3233theorem gcd.divides_iff (a b d : Nat)34  shows d ∣ gcd(a, b) ↔ d ∣ a ∧ d ∣ b35proof36  constructor37  . intro h38    have left := gcd.divides_left at a, b39    have right := gcd.divides_right at a, b40    constructor41    . exact divides.transitive at d, gcd(a, b), a with h, left42    . exact divides.transitive at d, gcd(a, b), b with h, right43  . intro both44    rcases both with ⟨left, right⟩45    exact gcd.greatest with left, right4647theorem gcd.le_left (a b : Nat)48  requires nonzero : a ≠ 049  shows gcd(a, b) ≤ a50proof51  have left := gcd.divides_left at a, b52  exact divides.le at gcd(a, b), a with left, nonzero5354theorem gcd.le_right (a b : Nat)55  requires nonzero : b ≠ 056  shows gcd(a, b) ≤ b57proof58  have right := gcd.divides_right at a, b59  exact divides.le at gcd(a, b), b with right, nonzero6061theorem gcd.nonzero (a b : Nat)62  requires nonzero : a ≠ 063  shows gcd(a, b) ≠ 064proof65  intro zero66  have both := gcd.zero_iff at a, b67  have zeros := both.forward with zero68  exact nonzero with zeros.left6970theorem gcd.nonzero_right (a b : Nat)71  requires nonzero : b ≠ 072  shows gcd(a, b) ≠ 073proof74  intro zero75  have both := gcd.zero_iff at a, b76  have zeros := both.forward with zero77  exact nonzero with zeros.right7879theorem gcd.positive (a b : Nat)80  requires nonzero : a ≠ 081  shows 0 < gcd(a, b)82proof83  have distinct := gcd.nonzero at a, b with nonzero84  exact Less.positive_of_ne_zero with distinct8586theorem gcd.greatest_le (a b d : Nat)87  requires nonzero : a ≠ 088  requires left : d ∣ a89  requires right : d ∣ b90  shows d ≤ gcd(a, b)91proof92  have common := gcd.greatest with left, right93  have distinct := gcd.nonzero at a, b with nonzero94  exact divides.le at d, gcd(a, b) with common, distinct9596theorem gcd.divides_add (a b : Nat)97  shows gcd(a, b) ∣ a + b98proof99  have left := gcd.divides_left at a, b100  have right := gcd.divides_right at a, b101  exact divides.add at gcd(a, b), a, b with left, right102103theorem gcd.divides_mul (a b c : Nat)104  shows gcd(a, b) ∣ a * c105proof106  have left := gcd.divides_left at a, b107  exact divides.multiply_right at gcd(a, b), a, c with left108109theorem gcd.add_left (a b : Nat)110  shows gcd(a + b, b) = gcd(a, b)111proof112  have correct := gcd.correct at a, b113  have certificate := IsGCD.add_right_iff at a, b, gcd(a, b)114  have shifted := certificate.backward with correct115  exact gcd.unique with shifted116117theorem gcd.add_left_swap (a b : Nat)118  shows gcd(b + a, b) = gcd(a, b)119proof120  have commute : b + a = a + b by ring121  rw commute122  exact gcd.add_left at a, b123124theorem gcd.add_right (a b : Nat)125  shows gcd(a, a + b) = gcd(a, b)126proof127  have first := gcd.commutative at a, a + b128  have second := gcd.add_left_swap at b, a129  have third := gcd.commutative at b, a130  rw [first, second, third]131  rfl132133theorem gcd.add_right_swap (a b : Nat)134  shows gcd(a, b + a) = gcd(a, b)135proof136  have commute : b + a = a + b by ring137  rw commute138  exact gcd.add_right at a, b139140theorem gcd.add_mul_left (a b k : Nat)141  shows gcd(a + k * b, b) = gcd(a, b)142proof143  have correct := gcd.correct at a, b144  have swapped := IsGCD.symmetric with correct145  have equation : a + k * b = b * k + a by ring146  have certificate := IsGCD.euclidean_iff at a + k * b, b, k, a, gcd(a, b)147    with equation148  have shifted := certificate.backward with swapped149  exact gcd.unique with shifted150151theorem gcd.add_mul_right (a b k : Nat)152  shows gcd(a, b + k * a) = gcd(a, b)153proof154  have first := gcd.commutative at a, b + k * a155  have second := gcd.add_mul_left at b, a, k156  have third := gcd.commutative at b, a157  rw [first, second, third]158  rfl159160theorem gcd.sub_left (a b : Nat)161  requires below : b ≤ a162  shows gcd(a - b, b) = gcd(a, b)163proof164  have split := sub.add_cancel at a, b with below165  have shifted := gcd.add_left at a - b, b166  rw split at shifted167  symm168  exact shifted169170theorem gcd.sub_right (a b : Nat)171  requires below : b ≤ a172  shows gcd(b, a - b) = gcd(a, b)173proof174  have first := gcd.commutative at b, a - b175  have second := gcd.sub_left at a, b with below176  rw [first, second]177  rfl178179theorem gcd.eq_left_iff (a b : Nat)180  shows gcd(a, b) = a ↔ a ∣ b181proof182  constructor183  . intro same184    have right := gcd.divides_right at a, b185    rw same at right186    exact right187  . intro hab188    exact gcd.of_divides with hab189190theorem gcd.eq_right_iff (a b : Nat)191  shows gcd(a, b) = b ↔ b ∣ a192proof193  have commute := gcd.commutative at a, b194  rw commute195  exact gcd.eq_left_iff at b, a196197theorem gcd.mul_left_self (a b : Nat)198  shows gcd(a, a * b) = a199proof200  have factor := divides.mul_left_self at a, b201  exact gcd.of_divides with factor202203theorem gcd.mul_right_self (a b : Nat)204  shows gcd(a, b * a) = a205proof206  have factor := divides.mul_right_self at a, b207  exact gcd.of_divides with factor208209theorem gcd.mul_self_left (a b : Nat)210  shows gcd(a * b, a) = a211proof212  have commute := gcd.commutative at a * b, a213  rw commute214  exact gcd.mul_left_self at a, b215216theorem gcd.idempotent_left (a b : Nat)217  shows gcd(gcd(a, b), b) = gcd(a, b)218proof219  have right := gcd.divides_right at a, b220  exact gcd.of_divides with right221222theorem gcd.idempotent_right (a b : Nat)223  shows gcd(a, gcd(a, b)) = gcd(a, b)224proof225  have commute := gcd.commutative at a, gcd(a, b)226  rw commute227  have left := gcd.divides_left at a, b228  exact gcd.of_divides with left229230theorem gcd.consecutive (n : Nat)231  shows gcd(n, n + 1) = 1232proof233  have shifted := gcd.add_right at n, 1234  rw shifted235  exact gcd.one_right at n236237theorem gcd.consecutive_left (n : Nat)238  shows gcd(n + 1, n) = 1239proof240  have commute := gcd.commutative at n + 1, n241  rw commute242  exact gcd.consecutive at n243244theorem gcd.associative (a b c : Nat)245  shows gcd(gcd(a, b), c) = gcd(a, gcd(b, c))246proof247  have innerLeft := gcd.divides_left at a, b248  have innerRight := gcd.divides_right at a, b249  have outerLeft := gcd.divides_left at gcd(a, b), c250  have outerRight := gcd.divides_right at gcd(a, b), c251  have dividesA := divides.transitive at gcd(gcd(a, b), c), gcd(a, b), a252    with outerLeft, innerLeft253  have dividesB := divides.transitive at gcd(gcd(a, b), c), gcd(a, b), b254    with outerLeft, innerRight255  have dividesBC := gcd.greatest at b, c, gcd(gcd(a, b), c)256    with dividesB, outerRight257  have certificate : IsGCD(a, gcd(b, c), gcd(gcd(a, b), c))258    apply IsGCD.intro259    . exact dividesA260    . exact dividesBC261    . intros d dNat dA dBC262      have left := gcd.divides_left at b, c263      have right := gcd.divides_right at b, c264      have dB := divides.transitive at d, gcd(b, c), b with dBC, left265      have dC := divides.transitive at d, gcd(b, c), c with dBC, right266      have dAB := gcd.greatest at a, b, d with dA, dB267      exact gcd.greatest at gcd(a, b), c, d with dAB, dC268  symm269  exact gcd.unique with certificate270271-- A common factor comes out of the greatest common divisor; the greatest272-- property passes through Bézout's identity over the integers.273theorem gcd.mul_right_distribute (a b c : Nat)274  shows gcd(a * c, b * c) = gcd(a, b) * c275proof276  have left := gcd.divides_left at a, b277  have right := gcd.divides_right at a, b278  have reflexive := divides.reflexive at c279  have scaledLeft := divides.mul_mono at gcd(a, b), a, c, c with left, reflexive280  have scaledRight := divides.mul_mono at gcd(a, b), b, c, c281    with right, reflexive282  have certificate : IsGCD(a * c, b * c, gcd(a, b) * c)283    apply IsGCD.intro284    . exact scaledLeft285    . exact scaledRight286    . intros d dNat dA dB287      obtain ⟨u, uInteger, v, vInteger, identity⟩ := gcd.bezout at a, b288      have bridgeA := IntegerDivides.natural_left at d, integerOfNat(a * c)289      have bridgeB := IntegerDivides.natural_left at d, integerOfNat(b * c)290      have bridgeG := IntegerDivides.natural_left at d, integerOfNat(gcd(a, b) * c)291      have magnitudeA := integerNatAbs.ofNat at a * c292      have magnitudeB := integerNatAbs.ofNat at b * c293      have magnitudeG := integerNatAbs.ofNat at gcd(a, b) * c294      rw magnitudeA at bridgeA295      rw magnitudeB at bridgeB296      rw magnitudeG at bridgeG297      have integerA := bridgeA.backward with dA298      have integerB := bridgeB.backward with dB299      have combination : IntegerDivides(integerOfNat(d),300          u * integerOfNat(a * c) + v * integerOfNat(b * c))301        exact IntegerDivides.linear_combination with integerA, integerB302      have value : u * integerOfNat(a * c) + v * integerOfNat(b * c) =303          integerOfNat(gcd(a, b) * c)304        have productA := integerOfNat.mul at a, c305        have productB := integerOfNat.mul at b, c306        have productG := integerOfNat.mul at gcd(a, b), c307        unfold integerLinearCombination at identity308        rw [productA, productB, productG, ← identity]309        ring310      rw value at combination311      exact bridgeG.forward with combination312  exact gcd.unique with certificate313314theorem gcd.mul_left_distribute (a b c : Nat)315  shows gcd(c * a, c * b) = c * gcd(a, b)316proof317  have left : c * a = a * c by ring318  have right : c * b = b * c by ring319  have product : gcd(a, b) * c = c * gcd(a, b) by ring320  rw [left, right, ← product]321  exact gcd.mul_right_distribute at a, b, c322323theorem gcd.coprime_mul (a b c : Nat)324  requires coprimeAB : gcd(a, b) = 1325  shows gcd(a, b * c) = gcd(a, c)326proof327  have left := gcd.divides_left at a, c328  have right := gcd.divides_right at a, c329  have scaled := divides.multiply_left at gcd(a, c), c, b with *330  have certificate : IsGCD(a, b * c, gcd(a, c))331    apply IsGCD.intro332    . exact left333    . exact scaled334    . intros d dNat dA dBC335      have dividesB := gcd.divides_left at b, d336      have dividesD := gcd.divides_right at b, d337      have dividesA := divides.transitive at gcd(b, d), d, a with dividesD, dA338      have common := gcd.greatest at a, b, gcd(b, d) with dividesA, dividesB339      rw coprimeAB at common340      have one := divides.one_only at gcd(b, d) with *341      have cancelled := coprime.cancel at b, d, c with one, dBC342      exact gcd.greatest at a, c, d with dA, cancelled343  exact gcd.unique with certificate344345theorem gcd.coprime_mul_left (a b c : Nat)346  requires coprimeAB : gcd(a, b) = 1347  shows gcd(a * c, b) = gcd(c, b)348proof349  have first := gcd.commutative at a * c, b350  have swapped := gcd.commutative at a, b351  rw swapped at coprimeAB352  have second := gcd.coprime_mul at b, a, c with coprimeAB353  have third := gcd.commutative at b, c354  rw [first, second, third]355  rfl356357theorem gcd.eq_one_iff (a b : Nat)358  shows gcd(a, b) = 1 ↔ ∀ d, Nat(d) → d ∣ a → d ∣ b → d = 1359proof360  constructor361  . intros one d dNat left right362    have common := gcd.greatest at a, b, d with left, right363    rw one at common364    exact divides.one_only at d with *365  . intro every366    have left := gcd.divides_left at a, b367    have right := gcd.divides_right at a, b368    exact every with gcd(a, b), left, right369370theorem coprime.symmetric (a b : Nat)371  requires coprimeAB : gcd(a, b) = 1372  shows gcd(b, a) = 1373proof374  have commute := gcd.commutative at b, a375  rw commute376  exact coprimeAB377378theorem coprime.divisor_one (a b d : Nat)379  requires coprimeAB : gcd(a, b) = 1380  requires left : d ∣ a381  requires right : d ∣ b382  shows d = 1383proof384  have every := gcd.eq_one_iff at a, b385  exact every.forward with coprimeAB, d, left, right386387theorem coprime.cancel_right (a n t : Nat)388  requires coprimeAN : gcd(a, n) = 1389  requires product : n ∣ t * a390  shows n ∣ t391proof392  have commute : t * a = a * t by ring393  rw commute at product394  exact coprime.cancel at a, n, t with coprimeAN, product395396theorem coprime.mul_of_coprime (a b n : Nat)397  requires first : gcd(a, n) = 1398  requires second : gcd(b, n) = 1399  shows gcd(a * b, n) = 1400proof401  have swapped := coprime.symmetric at a, n with first402  have reduced := gcd.coprime_mul at n, a, b with swapped403  have commute := gcd.commutative at a * b, n404  rw [commute, reduced]405  exact coprime.symmetric at b, n with second406407theorem coprime.of_mul_left (a b n : Nat)408  requires product : gcd(a * b, n) = 1409  shows gcd(a, n) = 1410proof411  have left := gcd.divides_left at a, n412  have right := gcd.divides_right at a, n413  have scaled := divides.multiply_right at gcd(a, n), a, b with left414  have common := gcd.greatest at a * b, n, gcd(a, n) with scaled, right415  rw product at common416  exact divides.one_only at gcd(a, n) with *417418theorem coprime.of_mul_right (a b n : Nat)419  requires product : gcd(a * b, n) = 1420  shows gcd(b, n) = 1421proof422  have commute : a * b = b * a by ring423  rw commute at product424  exact coprime.of_mul_left at b, a, n with product425426theorem coprime.mul_iff (a b n : Nat)427  shows gcd(a * b, n) = 1 ↔ gcd(a, n) = 1 ∧ gcd(b, n) = 1428proof429  constructor430  . intro product431    constructor432    . exact coprime.of_mul_left at a, b, n with product433    . exact coprime.of_mul_right at a, b, n with product434  . intro both435    rcases both with ⟨first, second⟩436    exact coprime.mul_of_coprime at a, b, n with first, second437438theorem coprime.pow_left (a b n : Nat)439  requires coprimeAB : gcd(a, b) = 1440  shows gcd(a ^ n, b) = 1441proof442  induction n443  | zero =>444    have zero := pow.zero at a445    rw zero446    exact gcd.one_left at b447  | k + 1 using ih =>448    have expand := pow.add_one at a, k449    rw expand450    exact coprime.mul_of_coprime at a, a ^ k, b with coprimeAB, ih451452theorem coprime.pow_right (a b n : Nat)453  requires coprimeAB : gcd(a, b) = 1454  shows gcd(a, b ^ n) = 1455proof456  have swapped := coprime.symmetric at a, b with coprimeAB457  have power := coprime.pow_left at b, a, n with swapped458  exact coprime.symmetric at b ^ n, a with power459460theorem coprime.pow (a b m n : Nat)461  requires coprimeAB : gcd(a, b) = 1462  shows gcd(a ^ m, b ^ n) = 1463proof464  have left := coprime.pow_left at a, b, m with coprimeAB465  exact coprime.pow_right at a ^ m, b, n with left466467theorem coprime.mul_divides (a b n : Nat)468  requires coprimeAB : gcd(a, b) = 1469  requires left : a ∣ n470  requires right : b ∣ n471  shows a * b ∣ n472proof473  obtain ⟨k, kNat, equation⟩ := left474  have scaled : b ∣ a * k475    rw equation476    exact right477  have cancelled := coprime.cancel at a, b, k with coprimeAB, scaled478  obtain ⟨m, mNat, kEquation⟩ := cancelled479  witness m480  rw [← equation, ← kEquation]481  ring482483theorem Prime.gcd_of_not_divides (p a : Nat)484  requires prime : Prime(p)485  requires notDivides : ¬(p ∣ a)486  shows gcd(p, a) = 1487proof488  have certificate := Prime.coprime_of_not_divides with prime, notDivides489  exact gcd.unique with certificate490491theorem Prime.coprime_or_divides (p a : Nat)492  requires prime : Prime(p)493  shows gcd(p, a) = 1 ∨ p ∣ a494proof495  have split : p ∣ a ∨ ¬(p ∣ a) by tauto496  cases split with yes | no497  . right498    exact yes499  . left500    exact Prime.gcd_of_not_divides with prime, no501502theorem Prime.divides_pow (p a n : Nat)503  requires prime : Prime(p)504  requires power : p ∣ a ^ n505  shows p ∣ a506proof507  induction n508  | zero =>509    intro power510    exfalso511    have zero := pow.zero at a512    rw zero at power513    have one := divides.one_only at p with *514    have above := Prime.greater_than_one with prime515    rw one at above516    exact Less.irreflexive at 1 with above517  | k + 1 using ih =>518    intro power519    have expand := pow.add_one at a, k520    rw expand at power521    have split := Prime.divides_mul at p, a, a ^ k with prime, power522    cases split with base | rest523    . exact base524    . exact ih with rest525