Grace/Cumulus/NumberTheory/Divisors.g17

Open in Workbench Download source

Imports

ModularMore · Cardinal.ListSupport

Declarations

Source

1-- The set of divisors of a natural number: membership, finiteness, the2-- divisors of 0, 1, and a prime, a characterisation of primes by their3-- divisors, and the small primes4-- 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.Divisors10import ModularMore11import Cardinal.ListSupport1213def divisors (n : Nat) : Set := { d ∈ n + 1 | d ∣ n }1415theorem divisors.natural (n : Nat, d : Set)16  requires member : d ∈ divisors(n)17  shows Nat(d)18proof19  have both := divisors.membership.forward with member20  have all := natural.member at n + 121  exact all with d, both.left2223theorem divisors.divides (n d : Nat)24  requires member : d ∈ divisors(n)25  shows d ∣ n26proof27  have both := divisors.membership.forward with member28  exact both.right2930theorem divisors.le (n d : Nat)31  requires member : d ∈ divisors(n)32  shows d ≤ n33proof34  have both := divisors.membership.forward with member35  have below := Less.of_membership at d, n + 1 with both.left36  arith3738theorem divisors.membership_le (n d : Nat)39  shows d ∈ divisors(n) ↔ d ≤ n ∧ d ∣ n40proof41  constructor42  . intro member43    have below := divisors.le with member44    have factor := divisors.divides with member45    exact ⟨below, factor⟩46  . intro both47    rcases both with ⟨below, factor⟩48    have bound : d < n + 1 by arith49    have member := membership.of_Less at d, n + 1 with *, bound50    exact divisors.membership.backward with ⟨member, factor⟩5152theorem divisors.subset_successor (n : Nat)53  shows divisors(n) ⊆ n + 154proof55  intros d member56  have both := divisors.membership.forward with member57  exact both.left5859theorem divisors.subset_naturals (n : Nat)60  shows divisors(n) ⊆ ℕ61proof62  intros d member63  have dNat := divisors.natural with member64  exact nat.omega.forward with dNat6566theorem divisors.finite (n : Nat)67  shows Finite(divisors(n))68proof69  have bounded := Finite.natural at n + 170  have subset := divisors.subset_successor at n71  exact Finite.subset with bounded, subset7273theorem divisors.self_member (n : Nat)74  shows n ∈ divisors(n)75proof76  have reflexive := divides.reflexive at n77  have below := LessEqual.reflexive at n78  have characterization := divisors.membership_le at n, n79  exact characterization.backward with ⟨below, reflexive⟩8081theorem divisors.one_member (n : Nat)82  requires nonzero : n ≠ 083  shows 1 ∈ divisors(n)84proof85  have one := one.divides at n86  have positive := LessEqual.one_iff_ne_zero at n87  have below := positive.backward with nonzero88  have characterization := divisors.membership_le at n, 189  exact characterization.backward with ⟨below, one⟩9091theorem divisors.nonempty (n : Nat)92  shows Nonempty(divisors(n))93proof94  have member := divisors.self_member at n95  exact ⟨n, member⟩9697theorem divisors.zero98  shows divisors(0) = {0}99proof100  ext x101  constructor102  . intro member103    have xNat := divisors.natural at 0, x with member104    have below := divisors.le at 0, x with member105    have xZero := LessEqual.eq_zero with below106    rw xZero107    apply singleton.membership.backward108    rfl109  . intro member110    have xZero := singleton.membership.forward with member111    rw xZero112    exact divisors.self_member at 0113114theorem divisors.one115  shows divisors(1) = {1}116proof117  ext x118  constructor119  . intro member120    have xNat := divisors.natural at 1, x with member121    have factor := divisors.divides at 1, x with member122    have xOne := divides.one_only at x with *123    rw xOne124    apply singleton.membership.backward125    rfl126  . intro member127    have xOne := singleton.membership.forward with member128    rw xOne129    exact divisors.self_member at 1130131theorem divisors.subset_of_divides (a b : Nat)132  requires nonzero : b ≠ 0133  requires hab : a ∣ b134  shows divisors(a) ⊆ divisors(b)135proof136  intros d member137  have dNat := divisors.natural at a, d with member138  have factor := divisors.divides at a, d with member139  have chained := divides.transitive at d, a, b with factor, hab140  have below := divides.le at d, b with chained, nonzero141  have characterization := divisors.membership_le at b, d142  exact characterization.backward with ⟨below, chained⟩143144theorem divisors.prime (p : Nat)145  requires prime : Prime(p)146  shows divisors(p) = {1, p}147proof148  have nonzero := Prime.nonzero with prime149  ext x150  constructor151  . intro member152    have xNat := divisors.natural at p, x with member153    have factor := divisors.divides at p, x with member154    have below := divisors.le at p, x with member155    have alternatives := LessEqual.cases at x, p with below156    apply pair.membership.backward157    cases alternatives with strict | same158    . left159      have proper := membership.of_Less at x, p with *, strict160      exact Prime.divisor at p, x with prime, xNat, proper, factor161    . right162      exact same163  . intro member164    have alternatives := pair.membership.forward with member165    cases alternatives with one | self166    . rw one167      exact divisors.one_member at p with nonzero168    . rw self169      exact divisors.self_member at p170171theorem Prime.of_divisors (p : Nat)172  requires aboveOne : 1 < p173  requires same : divisors(p) = {1, p}174  shows Prime(p)175proof176  have oneMember := membership.of_Less at 1, p with *, aboveOne177  refine ⟨oneMember, _⟩178  intros d dNat proper factor179  have strict := Less.of_membership at d, p with proper180  have below : d ≤ p by arith181  have characterization := divisors.membership_le at p, d182  have member := characterization.backward with ⟨below, factor⟩183  rw same at member184  have alternatives := pair.membership.forward with member185  cases alternatives with one | self186  . exact one187  . exfalso188    rw self at strict189    exact Less.irreflexive at p with strict190191theorem Prime.iff_divisors (p : Nat)192  shows Prime(p) ↔ 1 < p ∧ divisors(p) = {1, p}193proof194  constructor195  . intro prime196    have aboveOne := Prime.greater_than_one with prime197    have same := divisors.prime with prime198    exact ⟨aboveOne, same⟩199  . intro both200    rcases both with ⟨aboveOne, same⟩201    exact Prime.of_divisors with aboveOne, same202203theorem Prime.ne_one (p : Nat)204  requires prime : Prime(p)205  shows p ≠ 1206proof207  have aboveOne := Prime.greater_than_one with prime208  intro one209  rw one at aboveOne210  exact Less.irreflexive at 1 with aboveOne211212theorem Prime.two_le (p : Nat)213  requires prime : Prime(p)214  shows 2 ≤ p215proof216  have aboveOne := Prime.greater_than_one with prime217  arith218219theorem Prime.not_divides_one (p : Nat)220  requires prime : Prime(p)221  shows ¬(p ∣ 1)222proof223  intro unit224  have one := divides.one_only at p with *225  exact Prime.ne_one with prime, one226227theorem Prime.two228  shows Prime(2)229proof230  have oneMember : 1 ∈ 2 by typecheck231  refine ⟨oneMember, _⟩232  intros d dNat proper factor233  have strict := Less.of_membership at d, 2 with proper234  have alternatives := natural.below_two with strict235  cases alternatives with zero | one236  . exfalso237    rw zero at factor238    have bad := zero.divides_only_zero with factor239    have distinct : 2 ≠ 0 by arith240    exact distinct with bad241  . exact one242243theorem Prime.three244  shows Prime(3)245proof246  have oneMember : 1 ∈ 3 by typecheck247  refine ⟨oneMember, _⟩248  intros d dNat proper factor249  have strict := Less.of_membership at d, 3 with proper250  have alternatives := natural.below_three with strict251  rcases alternatives with zero | one | two252  . exfalso253    rw zero at factor254    have bad := zero.divides_only_zero with factor255    have distinct : 3 ≠ 0 by arith256    exact distinct with bad257  . exact one258  . exfalso259    rw two at factor260    have even := divides.two_iff_even at 3261    have isEven := even.forward with factor262    exact Even.not_three with isEven263264theorem divisors.two265  shows divisors(2) = {1, 2}266proof267  have prime := Prime.two268  exact divisors.prime with prime269270theorem divisors.three271  shows divisors(3) = {1, 3}272proof273  have prime := Prime.three274  exact divisors.prime with prime275276theorem Prime.two_or_odd (p : Nat)277  requires prime : Prime(p)278  shows p = 2 ∨ Odd(p)279proof280  have parity := parity.exhaustive at p281  cases parity with even | odd282  . left283    have characterization := divides.two_iff_even at p284    have two := characterization.backward with even285    have nonzero := Prime.nonzero with prime286    have below := divides.le at 2, p with two, nonzero287    have alternatives := LessEqual.cases at 2, p with below288    cases alternatives with strict | same289    . exfalso290      have proper := membership.of_Less at 2, p with *, strict291      have one := Prime.divisor at p, 2 with *292      have distinct : 2 ≠ 1 by arith293      exact distinct with one294    . symm295      exact same296  . right297    exact odd298299theorem Prime.odd_of_ne_two (p : Nat)300  requires prime : Prime(p)301  requires distinct : p ≠ 2302  shows Odd(p)303proof304  have alternatives := Prime.two_or_odd with prime305  cases alternatives with two | odd306  . exfalso307    exact distinct with two308  . exact odd309