Compfiles/Usa2019P5.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. inductive Usa2019P5.Writable The rational numbers that Evan can write on the board, starting from m / n and n / m line 39 source

   Source documentation

   The rational numbers that Evan can write on the board, starting from m / n and n / m.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Rat

   inductive Writable (m n : ℕ) : ℚ → Prop
     | base₁ : Writable m n ((m : ℚ) / n)
     | base₂ : Writable m n ((n : ℚ) / m)
     | am {x y : ℚ} : Writable m n x → Writable m n y → Writable m n ((x + y) / 2)
     | hm {x y : ℚ} : Writable m n x → Writable m n y → Writable m n (2 * x * y / (x + y))
   
   /-- If `p ∣ a + b` and `p ∣ c + d`, then `a * d + b * c ≡ -2 * b * d (mod p)`. -/

2. theorem Usa2019P5.sum_dvd_cong If p ∣ a + b and p ∣ c + d, then a * d + b * c ≡ -2 * b * d (mod p) line 46 source

   Source documentation

   If p ∣ a + b and p ∣ c + d, then a * d + b * c ≡ -2 * b * d (mod p).

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Int, Dvd.dvd, HAdd.hAdd, Int.ModEq, HMul.hMul, Neg.neg, OfNat.ofNat

   Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, propext, Int.modEq_iff_dvd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 44 more

   63 instances, coercions and auxiliary constants left out.

   Tactic trace: 15 steps

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

   theorem sum_dvd_cong {p a b c d : ℤ} (hpab : p ∣ a + b) (hpcd : p ∣ c + d) :
       a * d + b * c ≡ -2 * b * d [ZMOD p] := by
   …

3. theorem Usa2019P5.dvd_two_mul_mul_of_dvd If p ∣ a * d + b * c and a * d + b * c ≡ -2 * b * d (mod p), then p ∣ 2 * b * d line 64 source

   Source documentation

   If p ∣ a * d + b * c and a * d + b * c ≡ -2 * b * d (mod p), then p ∣ 2 * b * d.

   standard axioms: Quot.sound, propext what this means

   Statement uses: Int, Dvd.dvd, HAdd.hAdd, HMul.hMul, Int.ModEq, Neg.neg, OfNat.ofNat

   Proof uses: HSub.hSub, dvd_add, Eq.mp, congrArg, propext, Int.modEq_iff_dvd, Iff.mp, dvd_neg, neg_mul, add_sub_cancel

   39 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

   theorem dvd_two_mul_mul_of_dvd {p a b c d : ℤ}
       (h : p ∣ a * d + b * c) (hcong : a * d + b * c ≡ -2 * b * d [ZMOD p]) :
       p ∣ 2 * b * d := by
   …

   Mentions: h

4. theorem Usa2019P5.not_dvd_two_mul_mul An odd prime dividing neither b nor d does not divide 2 * b * d line 73 source

   Source documentation

   An odd prime dividing neither b nor d does not divide 2 * b * d.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Int, Not, Dvd.dvd, HMul.hMul

   Proof uses: Prime, Iff.mp, Nat.prime_iff_prime_int, cast, le_antisymm, Nat.le_of_dvd, two_pos, Nat.Prime.two_le, Or, False, Prime.dvd_mul

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 16 steps

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

   theorem not_dvd_two_mul_mul {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) {b d : ℤ}
       (hpb : ¬(p : ℤ) ∣ b) (hpd : ¬(p : ℤ) ∣ d) : ¬(p : ℤ) ∣ 2 * b * d := by
   …

5. theorem Usa2019P5.Writable.exists_rep The key invariant: if an odd prime p divides m + n, then every number that Evan can write has a representation a / b with p ∣ a + b and p ∤ b line 90 source

   Source documentation

   The key invariant: if an odd prime p divides m + n, then every number that Evan can write has a representation a / b with p ∣ a + b and p ∤ b. (Equivalently, in lowest terms the value is ≡ -1 (mod p).)

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Coprime, Nat.Prime, Ne, Dvd.dvd, HAdd.hAdd, Rat, Usa2019P5.Writable, Exists, Int, And, Eq, HDiv.hDiv, Not

   Proof uses: Usa2019P5.Writable.rec, Nat.gcd, Exists.intro, And.intro, cast, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, LT.lt.ne', of_eq_true, True, congr, Int.cast_natCast, eq_self, Iff.mp, Nat.dvd_add_left, Eq.mp, propext, Int.natCast_dvd_natCast and 114 more

   150 instances, coercions and auxiliary constants left out.

   Tactic trace: 72 steps

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

   theorem Writable.exists_rep {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hmn : m.Coprime n)
       {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) (hpd : p ∣ m + n)
       {x : ℚ} (hx : Writable m n x) :
       ∃ a b : ℤ, b ≠ 0 ∧ x = (a : ℚ) / b ∧ (p : ℤ) ∣ a + b ∧ ¬(p : ℤ) ∣ b := by
   …

   Mentions: Usa2019P5.Writable

6. theorem Usa2019P5.exists_odd_prime_dvd Any natural number ≥ 2 that is not a power of two has an odd prime factor line 159 source

   Source documentation

   Any natural number ≥ 2 that is not a power of two has an odd prime factor.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Ne, HPow.hPow, Exists, And, Nat.Prime, Odd, Dvd.dvd

   Proof uses: Eq, HMul.hMul, Nat.exists_eq_two_pow_mul_odd, False, Eq.mp, congrArg, mul_one, Eq.symm, MulZeroClass.mul_zero, Nat.exists_prime_and_dvd, Odd.ne_two_of_dvd_nat, Exists.intro, And.intro, Nat.Prime.odd_of_ne_two, Eq.rec, dvd_mul_of_dvd_right

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 13 steps

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

   theorem exists_odd_prime_dvd {N : ℕ} (hN : 2 ≤ N) (h : ∀ k : ℕ, N ≠ 2 ^ k) :
       ∃ p : ℕ, p.Prime ∧ Odd p ∧ p ∣ N := by
   …

   Mentions: h

7. theorem Usa2019P5.writable_combo Any dyadic weighted average of two writable numbers is writable (using arithmetic means alone) line 176 source

   Source documentation

   Any dyadic weighted average of two writable numbers is writable (using arithmetic means alone).

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Rat, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Usa2019P5.Writable, HDiv.hDiv, HMul.hMul

   Proof uses: Nat.recAux, Or, And, Eq.mp, congrArg, pow_zero, Eq.mpr, id, Eq.trans, congr, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, Nat.cast_one, one_mul, zero_add, div_one, Eq.symm, add_zero, Ne and 97 more

   135 instances, coercions and auxiliary constants left out.

   Tactic trace: 44 steps

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

   theorem writable_combo {m n : ℕ} (k : ℕ) :
       ∀ {a b : ℕ} {x y : ℚ}, a + b = 2 ^ k → Writable m n x → Writable m n y →
         Writable m n (((a : ℚ) * x + (b : ℚ) * y) / ((2 ^ k : ℕ) : ℚ)) := by
   …

   Mentions: Usa2019P5.Writable

8. determine Usa2019P5.solution_set line 219 source

   standard axioms: propext what this means

   Statement uses: Set, Prod, Nat

   Proof uses: Set.ofPred, Usa2019P5.solution_set.match_1, Exists, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat

   7 instances, coercions and auxiliary constants left out.

9. problem Usa2019P5.usa2019_p5 line 221 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Coprime, Iff, Membership.mem, Prod, Set, Usa2019P5.solution_set, Prod.mk, Usa2019P5.Writable, Rat

   Proof uses: Iff.intro, id, Exists, Eq, HAdd.hAdd, HPow.hPow, HDiv.hDiv, HMul.hMul, Usa2019P5.writable_combo, Usa2019P5.Writable.base₁, Usa2019P5.Writable.base₂, Ne, cast, Not, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, LT.lt.ne', congrFun' and 72 more

   121 instances, coercions and auxiliary constants left out.

   Tactic trace: 49 steps

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