Grace/Cumulus/NumberTheory/DivisibilityMore.g17

Open in Workbench Download source

Imports

Modular · Nat.Distance

Declarations

Source

1-- Further divisibility laws for the natural numbers: truncated subtraction,2-- powers, cancellation of a common factor, remainders, minimum and maximum,3-- parity, the distance between naturals, and factorials4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.DivisibilityMore10import Modular11import Nat.Distance1213theorem divides.intro (a b k : Nat)14  requires product : a * k = b15  shows a ∣ b16proof17  witness k18  exact product1920theorem divides.of_eq (a b : Nat)21  requires same : a = b22  shows a ∣ b23proof24  rw same25  exact divides.reflexive at b2627theorem divides.mul_left_self (a b : Nat)28  shows a ∣ a * b29proof30  witness b31  rfl3233theorem divides.mul_right_self (a b : Nat)34  shows a ∣ b * a35proof36  witness b37  ring3839theorem divides.mul_self (a b : Nat)40  requires hab : a ∣ b41  shows a ∣ b * b42proof43  exact divides.multiply_right with hab4445theorem divides.of_mul_left (a b c : Nat)46  requires product : a * b ∣ c47  shows a ∣ c48proof49  have factor := divides.mul_left_self at a, b50  exact divides.transitive at a, a * b, c with factor, product5152theorem divides.of_mul_right (a b c : Nat)53  requires product : a * b ∣ c54  shows b ∣ c55proof56  have factor := divides.mul_right_self at b, a57  exact divides.transitive at b, a * b, c with factor, product5859theorem divides.mul_mono (a b c d : Nat)60  requires left : a ∣ b61  requires right : c ∣ d62  shows a * c ∣ b * d63proof64  obtain ⟨k, kNat, kEquation⟩ := left65  obtain ⟨l, lNat, lEquation⟩ := right66  witness k * l67  rw [← kEquation, ← lEquation]68  ring6970theorem divides.mul_cancel_left (a b c : Nat)71  requires nonzero : a ≠ 072  shows a * b ∣ a * c ↔ b ∣ c73proof74  constructor75  . intro scaled76    obtain ⟨k, kNat, equation⟩ := scaled77    have rearranged : a * (b * k) = a * c78    . rw ← equation79      ring80    have cancelled := mul.left_cancel_positive with nonzero, rearranged81    witness k82    exact cancelled83  . intro plain84    obtain ⟨k, kNat, equation⟩ := plain85    witness k86    rw ← equation87    ring8889theorem divides.mul_cancel_right (a b c : Nat)90  requires nonzero : a ≠ 091  shows b * a ∣ c * a ↔ b ∣ c92proof93  have left : b * a = a * b by ring94  have right : c * a = a * c by ring95  rw [left, right]96  exact divides.mul_cancel_left with nonzero9798theorem divides.zero_iff (a : Nat)99  shows 0 ∣ a ↔ a = 0100proof101  constructor102  . intro h103    exact zero.divides_only_zero with h104  . intro zero105    rw zero106    exact divides.reflexive at 0107108theorem divides.one_iff (a : Nat)109  shows a ∣ 1 ↔ a = 1110proof111  constructor112  . intro h113    exact divides.one_only at a with *114  . intro one115    rw one116    exact divides.reflexive at 1117118theorem divides.antisymmetric_iff (a b : Nat)119  shows a ∣ b ∧ b ∣ a ↔ a = b120proof121  constructor122  . intro both123    rcases both with ⟨forward, backward⟩124    exact divides.antisymmetric with forward, backward125  . intro same126    rw same127    have reflexive := divides.reflexive at b128    exact ⟨reflexive, reflexive⟩129130theorem divides.nonzero (a b : Nat)131  requires hab : a ∣ b132  requires nonzero : b ≠ 0133  shows a ≠ 0134proof135  intro zero136  rw zero at hab137  have bZero := zero.divides_only_zero with hab138  exact nonzero with bZero139140theorem divides.lt_of_ne (a b : Nat)141  requires hab : a ∣ b142  requires nonzero : b ≠ 0143  requires distinct : a ≠ b144  shows a < b145proof146  have below := divides.le at a, b with hab, nonzero147  exact Less.of_LessEqual_ne with below, distinct148149theorem divides.factor_le (a b k : Nat)150  requires product : a * k = b151  requires nonzero : b ≠ 0152  shows k ≤ b153proof154  have factor : k ∣ b155    witness a156    rw ← product157    ring158  exact divides.le at k, b with factor, nonzero159160theorem divides.sub (a b c : Nat)161  requires left : a ∣ b162  requires right : a ∣ c163  shows a ∣ b - c164proof165  have total := LessEqual.total at c, b166  cases total with below | above167  . have split := sub.add_cancel_left at b, c with below168    rw ← split at left169    exact divides.add_cancel_left at a, c, b - c with right, left170  . have zero := sub.eq_zero_of_le at b, c with above171    rw zero172    exact divides.zero at a173174theorem divides.of_sub (a b c : Nat)175  requires below : c ≤ b176  requires right : a ∣ c177  requires difference : a ∣ b - c178  shows a ∣ b179proof180  have split := sub.add_cancel_left at b, c with below181  rw ← split182  exact divides.add at a, c, b - c with right, difference183184theorem divides.natDist (a b c : Nat)185  requires left : a ∣ b186  requires right : a ∣ c187  shows a ∣ natDist(b, c)188proof189  have first := divides.sub at a, b, c with left, right190  have second := divides.sub at a, c, b with right, left191  have value := natDist.value at b, c192  rw value193  exact divides.add at a, b - c, c - b with first, second194195theorem divides.pow (a b n : Nat)196  requires hab : a ∣ b197  shows a ∣ b ^ (n + 1)198proof199  have expand := pow.add_one at b, n200  rw expand201  exact divides.multiply_right with hab202203theorem divides.self_pow (a n : Nat)204  shows a ∣ a ^ (n + 1)205proof206  have reflexive := divides.reflexive at a207  exact divides.pow with reflexive208209theorem divides.pow_of_le (a m n : Nat)210  requires below : m ≤ n211  shows a ^ m ∣ a ^ n212proof213  obtain ⟨k, kNat, split⟩ := LessEqual.exists_add with below214  rw split215  have expand := pow.add at a, k, m216  rw expand217  exact divides.mul_left_self at a ^ m, a ^ k218219theorem divides.pow_mono (a b n : Nat)220  requires hab : a ∣ b221  shows a ^ n ∣ b ^ n222proof223  obtain ⟨k, kNat, equation⟩ := hab224  witness k ^ n225  rw ← equation226  symm227  exact pow.mul_base at a, k, n228229theorem divides.two_iff_even (n : Nat)230  shows 2 ∣ n ↔ Even(n)231proof232  have characterization := Even.iff_two_mul at n233  constructor234  . intro h235    obtain ⟨k, kNat, equation⟩ := h236    apply characterization.backward237    refine ⟨k, kNat, _⟩238    symm239    exact equation240  . intro h241    obtain ⟨k, kNat, equation⟩ := characterization.forward with h242    witness k243    symm244    exact equation245246theorem divides.not_two_iff_odd (n : Nat)247  shows ¬(2 ∣ n) ↔ Odd(n)248proof249  have even := divides.two_iff_even at n250  have odd := Odd.iff_not_even at n251  constructor252  . intro notDivides253    apply odd.backward254    intro isEven255    exact notDivides with (even.backward with isEven)256  . intro isOdd257    intro h258    have isEven := even.forward with h259    exact odd.forward with isOdd, isEven260261theorem divides.iff_mod_zero (d n : Nat)262  shows d ∣ n ↔ n % d = 0263proof264  have split : d = 0 ∨ d ≠ 0 by tauto265  cases split with zero | nonzero266  . rw zero267    have value := mod.zero_right at n268    rw value269    exact divides.zero_iff at n270  . have characterization := mod.zero_iff at d, n with nonzero271    constructor272    . intro h273      exact characterization.backward with h274    . intro h275      exact characterization.forward with h276277theorem divides.mod (d n m : Nat)278  requires left : d ∣ n279  requires right : d ∣ m280  shows d ∣ n % m281proof282  have split : m = 0 ∨ m ≠ 0 by tauto283  cases split with zero | nonzero284  . rw zero285    have value := mod.zero_right at n286    rw value287    exact left288  . obtain ⟨q, qNat, equation⟩ := mod.equation at n, m with nonzero289    have multiple := divides.multiply_right at d, m, q with right290    rw equation at left291    exact divides.add_cancel_left at d, m * q, n % m with multiple, left292293theorem divides.mod_iff (d n m : Nat)294  requires right : d ∣ m295  shows d ∣ n ↔ d ∣ n % m296proof297  have split : m = 0 ∨ m ≠ 0 by tauto298  cases split with zero | nonzero299  . rw zero300    have value := mod.zero_right at n301    rw value302    tauto303  . obtain ⟨q, qNat, equation⟩ := mod.equation at n, m with nonzero304    exact divides.remainder_iff at d, n, m, q, n % m with equation, right305306theorem divides.add_right_iff (a b c : Nat)307  requires hab : a ∣ b308  shows a ∣ b + c ↔ a ∣ c309proof310  constructor311  . intro sum312    exact divides.add_cancel_left at a, b, c with hab, sum313  . intro hac314    exact divides.add at a, b, c with hab, hac315316theorem divides.add_left_iff (a b c : Nat)317  requires hac : a ∣ c318  shows a ∣ b + c ↔ a ∣ b319proof320  have commute : b + c = c + b by ring321  rw commute322  exact divides.add_right_iff at a, c, b with hac323324theorem divides.add_mul_iff (a b k : Nat)325  shows a ∣ b + a * k ↔ a ∣ b326proof327  have multiple := divides.mul_left_self at a, k328  exact divides.add_left_iff at a, b, a * k with multiple329330theorem divides.natMin (a b c : Nat)331  requires left : a ∣ b332  requires right : a ∣ c333  shows a ∣ natMin(b, c)334proof335  have alternatives := natMin.cases at b, c336  cases alternatives with first | second337  . rw first338    exact left339  . rw second340    exact right341342theorem divides.natMax (a b c : Nat)343  requires left : a ∣ b344  requires right : a ∣ c345  shows a ∣ natMax(b, c)346proof347  have alternatives := natMax.cases at b, c348  cases alternatives with first | second349  . rw first350    exact left351  . rw second352    exact right353354theorem divides.quotient_equation (a b : Nat)355  requires nonzero : a ≠ 0356  requires hab : a ∣ b357  shows b = a * quotientNat(b, a)358proof359  have equation := quotientNat.equation at a, b360  have remainder := divides.iff_mod_zero at a, b361  have zero := remainder.forward with hab362  rw zero at equation363  have shape : a * quotientNat(b, a) + 0 = a * quotientNat(b, a) by ring364  rw shape at equation365  exact equation366367theorem divides.quotient (a b : Nat)368  requires nonzero : a ≠ 0369  requires hab : a ∣ b370  shows quotientNat(b, a) ∣ b371proof372  have equation := divides.quotient_equation with nonzero, hab373  witness a374  have shape : quotientNat(b, a) * a = a * quotientNat(b, a) by ring375  rw shape376  symm377  exact equation378379theorem divides.factorial_of_le (p n : Nat)380  requires positive : 0 < p381  requires below : p ≤ n382  shows p ∣ n!383proof384  have zeroMember := membership.of_Less at 0, p with *, positive385  have bound : p < succ(n) by arith386  have member := membership.of_Less at p, succ(n) with *, bound387  exact factorial.divisible_through at p, n with *, zeroMember, member388