Compfiles/Usa2007P5.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2007 P5

Prove that for every nonnegative integer n, the number 7^7^n + 1 is the product of at least 2n + 3 (not necessarily distinct) primes.

Imports (2)
Imported by 1 file
  1. lemma USA2007P5.factor_poly_an line 29 source

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

    Statement uses: Nat, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul, HSub.hSub

    Proof uses: Nat.casesAuxOn, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. lemma USA2007P5.factor_poly_bn line 34 source

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

    Statement uses: Nat, Eq, HAdd.hAdd, HSub.hSub, HPow.hPow, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.casesAuxOn, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. problem USA2007P5.usa2007_p5 line 41 source

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

    Statement uses: Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, List.length, Nat.primeFactorsList, HPow.hPow

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MulZeroClass.mul_zero, zero_add, List.cons, List.nil, List, pow_zero, pow_one, Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq, Mathlib.Meta.Simproc.FactorsHelper.cons_self, Mathlib.Meta.NormNum.isNat_mul, rfl, Mathlib.Meta.NormNum.IsNat.mk, Eq.refl and 122 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 48 steps

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