Compfiles/Usa1973P5.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

6 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1973, Problem 5

Show that the cube roots of three distinct primes cannot be terms in an arithmetic progression (whether consecutive or not).

Imports (7)
Imported by 1 file
  1. lemma Usa1973P5.cbrt_cubed Cubing a real cube root line 33 source

    Source documentation

    Cubing a real cube root.

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

    Statement uses: Real, LE.le, OfNat.ofNat, Eq, HPow.hPow, Nat, HDiv.hDiv

    Proof uses: HMul.hMul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_mul, Eq.refl, Mathlib.Meta.NormNum.isNNRat_div, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Mathlib.Meta.NormNum.isNat_natCast, Eq.mpr, id, congrArg, Eq.symm, Real.rpow_natCast and 2 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    lemma cbrt_cubed {x : ℝ} (hx : 0 ≤ x) : (x ^ ((1 : ℝ) / 3)) ^ 3 = x := by
…
  2. lemma Usa1973P5.factorization_pqr The prime p occurs with multiplicity exactly one in a product of three pairwise distinct primes p, q, r line 39 source

    Source documentation

    The prime p occurs with multiplicity exactly one in a product of three pairwise distinct primes p, q, r.

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

    Statement uses: Nat, Nat.Prime, Ne, Eq, Finsupp, Nat.factorization, HMul.hMul, OfNat.ofNat

    Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Nat.factorization_mul, mul_ne_zero, LT.lt.ne', Nat.Prime.pos, Eq.refl, Finsupp.add_apply, Finsupp.single, Nat.Prime.factorization, Finsupp.single_eq_same, Finsupp.single_eq_of_ne

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma factorization_pqr {p q r : ℕ} (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (hpr : p ≠ r) : (p * q * r).factorization p = 1 := by
…
  3. lemma Usa1973P5.not_cube_mul_cube Documented declaration: not_cube_mul_cube line 53 source

    Source documentation

    A product of three pairwise distinct primes times a nonzero cube is never a cube: comparing the exponent of p in the prime factorizations of both sides of p * q * r * b ^ 3 = a ^ 3 would give 1 + 3k = 3j.

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

    Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, HMul.hMul, HPow.hPow

    Proof uses: Eq, Finsupp, Nat.factorization, congrArg, Eq.mp, HAdd.hAdd, HSMul.hSMul, congrFun', Usa1973P5.factorization_pqr, Nat.factorization_pow, Nat.factorization_mul, mul_ne_zero, LT.lt.ne', Nat.Prime.pos, pow_ne_zero

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma not_cube_mul_cube {p q r a b : ℕ} (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (_hqr : q ≠ r) (hpr : p ≠ r) (hb : b ≠ 0) :
    p * q * r * b ^ 3 ≠ a ^ 3 := by
…
  4. lemma Usa1973P5.cube_root_pqr_ne_rat The cube root of a product of three pairwise distinct primes is irrational: it cannot be written as a quotient of two integers line 69 source

    Source documentation

    The cube root of a product of three pairwise distinct primes is irrational: it cannot be written as a quotient of two integers. Indeed, from ∛(pqr) = A / B we would get p * q * r * B³ = A³ in ℕ, contradicting not_cube_mul_cube.

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

    Statement uses: Nat, Nat.Prime, Ne, Int, OfNat.ofNat, Eq, Real, HPow.hPow, HMul.hMul, HDiv.hDiv, False

    Proof uses: cast, Eq.trans, Not, congrArg, Eq.symm, Nat.cast_zero, Int.cast_zero, Eq.mpr, id, div_mul_cancel₀, Eq.refl, Eq.mp, mul_pow, congr, Nat.cast_mul, congrFun', Int.cast_mul, Int.cast_natCast, Usa1973P5.cbrt_cubed, Nat.cast_nonneg' and 9 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

    lemma cube_root_pqr_ne_rat {p q r : ℕ} (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (hqr : q ≠ r) (hpr : p ≠ r) {A B : ℤ} (hB : B ≠ 0)
    (h : ((p * q * r : ℕ) : ℝ) ^ ((1 : ℝ) / 3) = (A : ℝ) / (B : ℝ)) : False := by
…

    Mentions: h

  5. lemma Usa1973P5.key_algebra The algebraic heart of the argument line 88 source

    Source documentation

    The algebraic heart of the argument. If ∛q = ∛p + m d and ∛r = ∛p + n d, then n ∛q - m ∛r = (n - m) ∛p; cubing that relation and regrouping expresses 3 m n (n - m) ∛p ∛q ∛r as an integer polynomial in p, q, r.

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

    Statement uses: Real, Int, Eq, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, HPow.hPow

    Proof uses: Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left and 50 more

    83 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma key_algebra {x y z : ℝ} {m n : ℤ}
    (h1 : (n : ℝ) * y - (m : ℝ) * z = ((n - m : ℤ) : ℝ) * x) :
    3 * (n : ℝ) * (m : ℝ) * ((n - m : ℤ) : ℝ) * (y * z * x)
      = (n : ℝ) ^ 3 * y ^ 3 - (m : ℝ) ^ 3 * z ^ 3 - ((n - m : ℤ) : ℝ) ^ 3 * x ^ 3 := by
…
  6. problem Usa1973P5.usa1973_p5 Documented declaration: usa1973_p5 line 104 source

    Source comment

    If `∛p, ∛q, ∛r` are terms of an arithmetic progression with common difference `d`, at integer positions differing by `m` and `n` from the position of `∛p`, then `∛q = ∛p + m d` and `∛r = ∛p + n d` as below, so it suffices to show that this is impossible for distinct primes `p, q, r`.

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

    Statement uses: Nat, Nat.Prime, Ne, Not, Exists, Int, Real, And, Eq, HPow.hPow, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, HMul.hMul

    Proof uses: False, rfl, Eq.mpr, id, congrArg, Usa1973P5.cbrt_cubed, Nat.cast_nonneg', congrFun', Eq.trans, Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right and 78 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 64 steps

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

    problem usa1973_p5 (p q r : ℕ) (hp : p.Prime) (hq : q.Prime) (hr : r.Prime)
    (hpq : p ≠ q) (hqr : q ≠ r) (hpr : p ≠ r) :
    ¬∃ (m n : ℤ) (d : ℝ),
      (q : ℝ) ^ ((1 : ℝ) / 3) = (p : ℝ) ^ ((1 : ℝ) / 3) + (m : ℝ) * d ∧
      (r : ℝ) ^ ((1 : ℝ) / 3) = (p : ℝ) ^ ((1 : ℝ) / 3) + (n : ℝ) * d := by
…