Grace/Cumulus/NumberTheory/IntegerDivisibility.g17

Open in Workbench Download source

Imports

Coprime · Int · ModularMore

Declarations

Source

1-- Divisibility over the integers: the basic laws, signs and absolute values,2-- cancellation, the bridge to natural divisibility, the bound |a| ≤ |b| for a3-- divisor of a nonzero integer, the units ±1, evenness as divisibility by4-- two, and further laws of integer congruence5-- 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.IntegerDivisibility11import Coprime12import Int13import ModularMore1415theorem IntegerDivides.intro (x y q : Integer)16  requires product : x * q = y17  shows IntegerDivides(x, y)18proof19  witness q20  exact product2122theorem IntegerDivides.reflexive (x : Integer)23  shows IntegerDivides(x, x)24proof25  witness integerOne26  ring2728theorem IntegerDivides.zero (x : Integer)29  shows IntegerDivides(x, integerZero)30proof31  witness integerZero32  ring3334theorem IntegerDivides.one_left (x : Integer)35  shows IntegerDivides(integerOne, x)36proof37  witness x38  ring3940theorem IntegerDivides.zero_left_iff (x : Integer)41  shows IntegerDivides(integerZero, x) ↔ x = 042proof43  constructor44  . intro h45    obtain ⟨q, qInteger, equation⟩ := h46    have vanish : integerZero * q = 0 by ring47    rw ← equation48    exact vanish49  . intro zero50    rw zero51    exact IntegerDivides.zero at integerZero5253theorem IntegerDivides.transitive (x y z : Integer)54  requires first : IntegerDivides(x, y)55  requires second : IntegerDivides(y, z)56  shows IntegerDivides(x, z)57proof58  obtain ⟨p, pInteger, pEquation⟩ := first59  obtain ⟨q, qInteger, qEquation⟩ := second60  witness p * q61  rw [← qEquation, ← pEquation]62  ring6364theorem IntegerDivides.mul_right (x y z : Integer)65  requires hxy : IntegerDivides(x, y)66  shows IntegerDivides(x, y * z)67proof68  obtain ⟨q, qInteger, equation⟩ := hxy69  witness q * z70  rw ← equation71  ring7273theorem IntegerDivides.mul_left (x y z : Integer)74  requires hxy : IntegerDivides(x, y)75  shows IntegerDivides(x, z * y)76proof77  obtain ⟨q, qInteger, equation⟩ := hxy78  witness z * q79  rw ← equation80  ring8182theorem IntegerDivides.mul_left_self (x y : Integer)83  shows IntegerDivides(x, x * y)84proof85  witness y86  rfl8788theorem IntegerDivides.mul_right_self (x y : Integer)89  shows IntegerDivides(x, y * x)90proof91  witness y92  ring9394theorem IntegerDivides.add (d x y : Integer)95  requires left : IntegerDivides(d, x)96  requires right : IntegerDivides(d, y)97  shows IntegerDivides(d, x + y)98proof99  obtain ⟨p, pInteger, pEquation⟩ := left100  obtain ⟨q, qInteger, qEquation⟩ := right101  witness p + q102  rw [← pEquation, ← qEquation]103  ring104105theorem IntegerDivides.neg_right (x y : Integer)106  requires hxy : IntegerDivides(x, y)107  shows IntegerDivides(x, -y)108proof109  obtain ⟨q, qInteger, equation⟩ := hxy110  witness -q111  rw ← equation112  ring113114theorem IntegerDivides.sub (d x y : Integer)115  requires left : IntegerDivides(d, x)116  requires right : IntegerDivides(d, y)117  shows IntegerDivides(d, x - y)118proof119  obtain ⟨p, pInteger, pEquation⟩ := left120  obtain ⟨q, qInteger, qEquation⟩ := right121  witness p - q122  rw [← pEquation, ← qEquation]123  ring124125theorem IntegerDivides.neg_right_iff (x y : Integer)126  shows IntegerDivides(x, -y) ↔ IntegerDivides(x, y)127proof128  constructor129  . intro h130    have doubled := IntegerDivides.neg_right at x, -y with h131    have involutive := integerNegValue.involutive at y132    rw involutive at doubled133    exact doubled134  . intro h135    exact IntegerDivides.neg_right at x, y with h136137theorem IntegerDivides.neg_left (x y : Integer)138  requires hxy : IntegerDivides(x, y)139  shows IntegerDivides(-x, y)140proof141  obtain ⟨q, qInteger, equation⟩ := hxy142  witness -q143  rw ← equation144  ring145146theorem IntegerDivides.neg_left_iff (x y : Integer)147  shows IntegerDivides(-x, y) ↔ IntegerDivides(x, y)148proof149  constructor150  . intro h151    have doubled := IntegerDivides.neg_left at -x, y with h152    have involutive := integerNegValue.involutive at x153    rw involutive at doubled154    exact doubled155  . intro h156    exact IntegerDivides.neg_left at x, y with h157158theorem IntegerDivides.abs_left_iff (x y : Integer)159  shows IntegerDivides(integerAbs(x), y) ↔ IntegerDivides(x, y)160proof161  have left := IntegerDivides.magnitude_iff at integerAbs(x), y162  have right := IntegerDivides.magnitude_iff at x, y163  have magnitude : integerNatAbs(integerAbs(x)) = integerNatAbs(x)164    have value := integerAbs.value at x165    rw value166    exact integerNatAbs.ofNat at integerNatAbs(x)167  rw magnitude at left168  constructor169  . intro h170    exact right.backward with (left.forward with h)171  . intro h172    exact left.backward with (right.forward with h)173174theorem IntegerDivides.abs_right_iff (x y : Integer)175  shows IntegerDivides(x, integerAbs(y)) ↔ IntegerDivides(x, y)176proof177  have left := IntegerDivides.magnitude_iff at x, integerAbs(y)178  have right := IntegerDivides.magnitude_iff at x, y179  have magnitude : integerNatAbs(integerAbs(y)) = integerNatAbs(y)180    have value := integerAbs.value at y181    rw value182    exact integerNatAbs.ofNat at integerNatAbs(y)183  rw magnitude at left184  constructor185  . intro h186    exact right.backward with (left.forward with h)187  . intro h188    exact left.backward with (right.forward with h)189190theorem IntegerDivides.mul_mono (a b c d : Integer)191  requires left : IntegerDivides(a, b)192  requires right : IntegerDivides(c, d)193  shows IntegerDivides(a * c, b * d)194proof195  obtain ⟨p, pInteger, pEquation⟩ := left196  obtain ⟨q, qInteger, qEquation⟩ := right197  witness p * q198  rw [← pEquation, ← qEquation]199  ring200201theorem IntegerDivides.mul_cancel_left (a b c : Integer)202  requires nonzero : a ≠ 0203  shows IntegerDivides(a * b, a * c) ↔ IntegerDivides(b, c)204proof205  constructor206  . intro scaled207    obtain ⟨q, qInteger, equation⟩ := scaled208    have rearranged : a * (b * q) = a * c209    . rw ← equation210      ring211    have cancelled := integerMulValue.left_cancel at b * q, c, a212      with nonzero, rearranged213    witness q214    exact cancelled215  . intro plain216    obtain ⟨q, qInteger, equation⟩ := plain217    witness q218    rw ← equation219    ring220221theorem IntegerDivides.add_right_iff (d x y : Integer)222  requires left : IntegerDivides(d, x)223  shows IntegerDivides(d, x + y) ↔ IntegerDivides(d, y)224proof225  constructor226  . intro sum227    have difference := IntegerDivides.sub at d, x + y, x with sum, left228    have shape : x + y - x = y by ring229    rw shape at difference230    exact difference231  . intro right232    exact IntegerDivides.add at d, x, y with left, right233234theorem IntegerDivides.ofNat_iff (a b : Nat)235  shows IntegerDivides(integerOfNat(a), integerOfNat(b)) ↔ a ∣ b236proof237  have bridge := IntegerDivides.natural_left at a, integerOfNat(b)238  have magnitude := integerNatAbs.ofNat at b239  rw magnitude at bridge240  exact bridge241242theorem IntegerDivides.of_natural (a b : Nat)243  requires hab : a ∣ b244  shows IntegerDivides(integerOfNat(a), integerOfNat(b))245proof246  have bridge := IntegerDivides.ofNat_iff at a, b247  exact bridge.backward with hab248249theorem IntegerDivides.natAbs_le (x y : Integer)250  requires nonzero : y ≠ 0251  requires hxy : IntegerDivides(x, y)252  shows integerNatAbs(x) ≤ integerNatAbs(y)253proof254  have magnitudes := IntegerDivides.to_magnitudes with hxy255  have distinct : integerNatAbs(y) ≠ 0256    intro zero257    have characterization := integerNatAbs.zero_iff at y258    have yZero := characterization.forward with zero259    exact nonzero with yZero260  exact divides.le at integerNatAbs(x), integerNatAbs(y)261    with magnitudes, distinct262263theorem IntegerDivides.abs_le (x y : Integer)264  requires nonzero : y ≠ 0265  requires hxy : IntegerDivides(x, y)266  shows integerAbs(x) ≤ integerAbs(y)267proof268  have below := IntegerDivides.natAbs_le with nonzero, hxy269  have left := integerAbs.value at x270  have right := integerAbs.value at y271  rw [left, right]272  exact integerOfNat.monotone with below273274theorem IntegerDivides.antisymmetric_natAbs (x y : Integer)275  requires forward : IntegerDivides(x, y)276  requires backward : IntegerDivides(y, x)277  shows integerNatAbs(x) = integerNatAbs(y)278proof279  have first := IntegerDivides.to_magnitudes with forward280  have second := IntegerDivides.to_magnitudes with backward281  exact divides.antisymmetric with first, second282283theorem IntegerDivides.antisymmetric (x y : Integer)284  requires forward : IntegerDivides(x, y)285  requires backward : IntegerDivides(y, x)286  shows x = y ∨ x = -y287proof288  have magnitudes := IntegerDivides.antisymmetric_natAbs with forward, backward289  have same : integerAbs(x) = integerAbs(y)290    have left := integerAbs.value at x291    have right := integerAbs.value at y292    rw [left, right, magnitudes]293    rfl294  have characterization := integerAbs.eq_iff at x, y295  exact characterization.forward with same296297theorem IntegerDivides.unit_iff (z : Integer)298  shows IntegerDivides(z, integerOne) ↔ z = integerOne ∨ z = -integerOne299proof300  have oneForm := integerOfNat.one301  constructor302  . intro h303    have magnitudes := IntegerDivides.to_magnitudes with h304    rw ← oneForm at magnitudes305    have magnitude := integerNatAbs.ofNat at 1306    rw magnitude at magnitudes307    have unit := divides.one_only at integerNatAbs(z) with *308    have signs := integerNatAbs.cases at z309    rw unit at signs310    cases signs with positive | negative311    . left312      rw [positive, oneForm]313      rfl314    . right315      have negated := integerNegativeOfNat.eq_neg at 1316      rw [negative, negated, oneForm]317      rfl318  . intro signs319    cases signs with positive | negative320    . rw positive321      exact IntegerDivides.reflexive at integerOne322    . rw negative323      witness -integerOne324      ring325326theorem IntegerDivides.unit_left (z x : Integer)327  requires unit : z = integerOne ∨ z = -integerOne328  shows IntegerDivides(z, x)329proof330  cases unit with positive | negative331  . rw positive332    exact IntegerDivides.one_left at x333  . rw negative334    witness -x335    ring336337theorem IntegerDivides.two_iff_even (z : Integer)338  shows IntegerDivides(integerOfNat(2), z) ↔ IntegerEven(z)339proof340  have two : integerOfNat(2) = integerOne + integerOne341    have split := integerOfNat.add at 1, 1342    have sum : 1 + 1 = 2 by compute343    rw [sum, integerOfNat.one] at split344    exact split345  constructor346  . intro h347    obtain ⟨q, qInteger, equation⟩ := h348    have shape : z = q + q349      rw [← equation, two]350      ring351    rw shape352    exact IntegerEven.double at q353  . intro even354    obtain ⟨k, kMember, shape⟩ := even355    have kInteger : Integer(k) by typecheck356    witness k357    rw [two, shape]358    ring359360theorem IntegerDivides.not_two_iff_odd (z : Integer)361  shows ¬IntegerDivides(integerOfNat(2), z) ↔ IntegerOdd(z)362proof363  have even := IntegerDivides.two_iff_even at z364  have odd := IntegerOdd.iff_not_even at z365  constructor366  . intro notDivides367    apply odd.backward368    intro isEven369    exact notDivides with (even.backward with isEven)370  . intro isOdd371    intro h372    have isEven := even.forward with h373    exact odd.forward with isOdd, isEven374375theorem IntegerDivides.pow (x y : Integer, n : Nat)376  requires hxy : IntegerDivides(x, y)377  shows IntegerDivides(x, integerPow(y, n + 1))378proof379  have expand := integerPow.add_one at y, n380  rw expand381  exact IntegerDivides.mul_right at x, y, integerPow(y, n) with hxy382383theorem IntegerCongruent.zero_right_iff (m a : Integer)384  shows IntegerCongruent(m, a, integerZero) ↔ IntegerDivides(m, a)385proof386  have shape : a - integerZero = a by ring387  constructor388  . intro congruent389    unfold IntegerCongruent at congruent390    rw shape at congruent391    exact congruent392  . intro h393    unfold IntegerCongruent394    rw shape395    exact h396397theorem IntegerCongruent.of_eq (m a b : Integer)398  requires same : a = b399  shows IntegerCongruent(m, a, b)400proof401  rw same402  exact IntegerCongruent.reflexive at m, b403404theorem IntegerCongruent.one_modulus (a b : Integer)405  shows IntegerCongruent(integerOne, a, b)406proof407  unfold IntegerCongruent408  exact IntegerDivides.one_left at a - b409410theorem IntegerCongruent.neg (m a b : Integer)411  requires congruent : IntegerCongruent(m, a, b)412  shows IntegerCongruent(m, -a, -b)413proof414  unfold IntegerCongruent at congruent415  unfold IntegerCongruent416  have negated := IntegerDivides.neg_right at m, a - b with congruent417  have shape : -(a - b) = -a - (-b) by ring418  rw shape at negated419  exact negated420421theorem IntegerCongruent.sub (m a b c d : Integer)422  requires first : IntegerCongruent(m, a, b)423  requires second : IntegerCongruent(m, c, d)424  shows IntegerCongruent(m, a - c, b - d)425proof426  have negated := IntegerCongruent.neg at m, c, d with second427  have sum := IntegerCongruent.add at m, a, b, -c, -d with first, negated428  have left : a + (-c) = a - c by ring429  have right : b + (-d) = b - d by ring430  rw [left, right] at sum431  exact sum432433theorem IntegerCongruent.mul_left (m a b c : Integer)434  requires congruent : IntegerCongruent(m, a, b)435  shows IntegerCongruent(m, c * a, c * b)436proof437  have reflexive := IntegerCongruent.reflexive at m, c438  exact IntegerCongruent.mul at m, c, c, a, b with reflexive, congruent439440theorem IntegerCongruent.mul_right (m a b c : Integer)441  requires congruent : IntegerCongruent(m, a, b)442  shows IntegerCongruent(m, a * c, b * c)443proof444  have reflexive := IntegerCongruent.reflexive at m, c445  exact IntegerCongruent.mul at m, a, b, c, c with congruent, reflexive446447theorem IntegerCongruent.add_right_cancel (m a b c : Integer)448  requires congruent : IntegerCongruent(m, a + c, b + c)449  shows IntegerCongruent(m, a, b)450proof451  unfold IntegerCongruent at congruent452  unfold IntegerCongruent453  have shape : a + c - (b + c) = a - b by ring454  rw shape at congruent455  exact congruent456457theorem IntegerCongruent.add_left_cancel (m a b c : Integer)458  requires congruent : IntegerCongruent(m, c + a, c + b)459  shows IntegerCongruent(m, a, b)460proof461  unfold IntegerCongruent at congruent462  unfold IntegerCongruent463  have shape : c + a - (c + b) = a - b by ring464  rw shape at congruent465  exact congruent466467theorem IntegerCongruent.pow (m a b : Integer, n : Nat)468  requires congruent : IntegerCongruent(m, a, b)469  shows IntegerCongruent(m, integerPow(a, n), integerPow(b, n))470proof471  induction n472  | zero =>473    have left := integerPow.zero at a474    have right := integerPow.zero at b475    rw [left, right]476    exact IntegerCongruent.reflexive at m, integerOne477  | k + 1 using ih =>478    have left := integerPow.add_one at a, k479    have right := integerPow.add_one at b, k480    rw [left, right]481    exact IntegerCongruent.mul at m, a, b, integerPow(a, k), integerPow(b, k)482      with congruent, ih483484theorem IntegerCongruent.divides_modulus (m n a b : Integer)485  requires hmn : IntegerDivides(m, n)486  requires congruent : IntegerCongruent(n, a, b)487  shows IntegerCongruent(m, a, b)488proof489  unfold IntegerCongruent at congruent490  unfold IntegerCongruent491  exact IntegerDivides.transitive at m, n, a - b with hmn, congruent492493theorem IntegerCongruent.neg_modulus (m a b : Integer)494  shows IntegerCongruent(-m, a, b) ↔ IntegerCongruent(m, a, b)495proof496  have characterization := IntegerDivides.neg_left_iff at m, a - b497  constructor498  . intro congruent499    unfold IntegerCongruent at congruent500    unfold IntegerCongruent501    exact characterization.forward with congruent502  . intro congruent503    unfold IntegerCongruent at congruent504    unfold IntegerCongruent505    exact characterization.backward with congruent506507-- Integer congruence of embedded naturals is natural congruence.508theorem IntegerCongruent.ofNat_iff (m a b : Nat)509  shows510    IntegerCongruent(integerOfNat(m), integerOfNat(a), integerOfNat(b)) ↔511      CongruentMod(a, b, m)512proof513  have bridge := IntegerDivides.natural_left at m, integerOfNat(a) - integerOfNat(b)514  have distance := integerNatAbs.ofNat_sub at a, b515  rw distance at bridge516  have characterization := CongruentMod.iff_divides_natDist at a, b, m517  constructor518  . intro congruent519    unfold IntegerCongruent at congruent520    have distanceDivides := bridge.forward with congruent521    exact characterization.backward with distanceDivides522  . intro congruent523    unfold IntegerCongruent524    have distanceDivides := characterization.forward with congruent525    exact bridge.backward with distanceDivides526