`Compfiles/Usa1989P1.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1989, Problem 1

For each positive integer n, let Sn = 1 + 1/2 + 1/3 + ··· + 1/n Tn = S1 + S2 + S3 + ··· + Sn Un = T1/2 + T2/3 + T3/4 + ··· + Tn/(n+1) Find, with proof, integers 0 < a, b, c, d < 1000000 such that T1988 = a * S1989 - b U1988 = c * S1989 - d

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa1989P1.s line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv
9 instances, coercions and auxiliary constants left out.
def Usa1989P1.t line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, Usa1989P1.s
4 instances, coercions and auxiliary constants left out.
def Usa1989P1.u line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, Usa1989P1.t, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.
theorem Usa1989P1.extract_one line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Eq, Finset.sum, Finset.Icc, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, Insert.insert, Finset, id, congrArg, Eq.symm, Finset.insert_Icc_right_eq_Icc_add_one, of_eq_true, LE.le, Eq.trans, True, Function.swap, Finset.sum_insert, Not, Membership.mem, False, And, congr, and_false, not_false_eq_true and 1 more
64 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1989P1.l1 line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Usa1989P1.t, HSub.hSub, OfNat.ofNat, HMul.hMul, Usa1989P1.s
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Finset.sum_congr, Finset.Icc, EmptyCollection.emptyCollection, Finset, zero_tsub, Finset.Icc_eq_empty_of_lt, LT.lt, eq_self, Membership.mem, Eq.refl, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, sub_self and 30 more
96 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1989P1.l2 line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Usa1989P1.u, HSub.hSub, OfNat.ofNat, HMul.hMul, HAdd.hAdd, Usa1989P1.s
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Finset.sum_congr, Finset.Icc, EmptyCollection.emptyCollection, Finset, HDiv.hDiv, Usa1989P1.t, Finset.sum, Inv.inv, zero_tsub, Finset.Icc_eq_empty_of_lt, LT.lt, eq_self, Membership.mem, congrFun' and 65 more
132 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
determine Usa1989P1.solutions line 82 source
no axioms what this means
Statement uses: Prod, Nat
Proof uses: Prod.mk, OfNat.ofNat, HMul.hMul
3 instances, coercions and auxiliary constants left out.
problem Usa1989P1.usa1989_p1 line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Rat, Usa1989P1.t, OfNat.ofNat, Nat, HSub.hSub, HMul.hMul, Prod.fst, Prod, Usa1989P1.solutions, Usa1989P1.s, Prod.snd, Usa1989P1.u
Proof uses: id, Prod.mk, And.intro, Usa1989P1.l1, Eq.mpr, congrArg, HAdd.hAdd, Usa1989P1.l2, Or, Eq.trans, Or.inl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_overlap, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_add and 2 more
47 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.