Compfiles/Imo1964P1.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. determine Imo1964P1.solution_set line 30 source

   no axioms what this means

   Statement uses: Set, Nat

   Proof uses: Set.ofPred, Eq, HMod.hMod, OfNat.ofNat

   3 instances, coercions and auxiliary constants left out.

2. problem Imo1964P1.imo1964_p1a IMO 1964 Problem 1(a): when 7 divides 2^n - 1 line 32 source

   L4DEL explanation

   2^n is congruent to 1 modulo 7 exactly when n is a multiple of 3.

   1. Problem part (a): find all natural n with 7 dividing 2^n - 1. The formal answer is the determined set solution_set = {n | n % 3 = 0}, and the statement is n in solution_set iff 2^n is congruent to 1 mod 7.
   2. Solution (complete, no sorry): if n = 3m then 2^n = 8^m, which is 1 mod 7.
   3. Conversely write n = 3q + r; since 2^3 = 1 mod 7 the power reduces to 2^r, and r = 1 or r = 2 gives 2 or 4, not 1.
   4. Part (b), that 7 never divides 2^n + 1, is the separate declaration imo1964_p1b in the same file, proved by the same residue argument.

   Prerequisites: Imo1964P1.solution_set

   See also: Imo1964P1.imo1964_p1b

   Sources and attribution: Pinned Lean source (47b19bbfe5f3)

   standard axioms: propext what this means

   Statement uses: Nat, Iff, Membership.mem, Set, Imo1964P1.solution_set, Nat.ModEq, OfNat.ofNat, HPow.hPow

   Proof uses: Iff.intro, Eq, HMul.hMul, Dvd.dvd, Nat.dvd_of_mod_eq_zero, id, Eq.mpr, HMod.hMod, congrArg, Nat.pow_mul, Nat.pow_mod, of_eq_true, Eq.trans, True, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat and 29 more

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 22 steps

   Open to load the checked before-and-after goal states.

   problem imo1964_p1a (n : ℕ) : n ∈ solution_set ↔ 2^n ≡ 1 [MOD 7] := by
   …

   Mentions: Imo1964P1.solution_set

3. problem Imo1964P1.imo1964_p1b line 49 source

   standard axioms: propext what this means

   Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, HAdd.hAdd, HPow.hPow

   Proof uses: Eq, HMod.hMod, Eq.refl, Mathlib.Tactic.ModCases.NatMod.onModCases_start, False, Bool, Bool.true, Mathlib.Tactic.ModCases.NatMod.onModCases_succ, Nat.ModEq, False.elim, noConfusion_of_Nat, Nat.ctorIdx, Eq.mp, HDiv.hDiv, congrArg, one_pow, Nat.pow_mod, HMul.hMul, pow_mul, Nat.add_mod and 8 more

   35 instances, coercions and auxiliary constants left out.

   Tactic trace: 15 steps

   Open to load the checked before-and-after goal states.

4. theorem Imo1964P1.imo_1964_p1b' An alternative proof, heavily golfed line 75 source

   Source comment

   An alternative proof, heavily golfed. The statement here is slightly modified from the original one.

   standard axioms: propext what this means

   Statement uses: Nat, Ne, HMod.hMod, HAdd.hAdd, HPow.hPow, OfNat.ofNat

   20 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

   theorem imo_1964_p1b' : ∀ (n : ℕ), (2 ^ n + 1) % 7 ≠ 0
       | 0 | 1 | 2 => by decide
       | n + 3 => by
         rw [pow_add, Nat.add_mod, Nat.mul_mod, show 2 ^ 3 % 7 = 1 by rfl]
         simp [imo_1964_p1b' n]
   
   snip end
   
   end Imo1964P1