Compfiles/Imo1975P4.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1975, Problem 4

When $4444^{4444}$ is written in decimal notation, the sum of its digits is $A$. Let $B$ be the sum of the digits of $A$. Find the sum of the digits of $B$. ($A$ and $B$ are written in decimal notation.)

Imports (2)
Imported by 1 file
  1. def Imo1975P4.A line 27 source

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

    Statement uses: Nat

    Proof uses: List.sum, Nat.digits, OfNat.ofNat, HPow.hPow

    8 instances, coercions and auxiliary constants left out.

  2. def Imo1975P4.B line 29 source

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

    Statement uses: Nat

    Proof uses: List.sum, Nat.digits, OfNat.ofNat, Imo1975P4.A

    4 instances, coercions and auxiliary constants left out.

  3. determine Imo1975P4.sum_digits_B line 31 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  4. theorem Imo1975P4.Nat.mod_eq_iff_eq line 43 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, Iff, Eq, HMod.hMod

    Proof uses: Eq.mpr, id, congrArg, Iff.mpr, Nat.mod_eq_iff_lt, Nat.ne_zero_of_lt, Iff.rfl

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. theorem Imo1975P4.Nat.modEq_iff_eq_lt line 48 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, Iff, Nat.ModEq, Eq

    Proof uses: Eq.mpr, HMod.hMod, id, congrArg, Nat.ModEq.eq_1, Iff.mpr, Nat.mod_eq_iff_lt, Nat.ne_zero_of_lt, Imo1975P4.Nat.mod_eq_iff_eq

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  6. theorem Imo1975P4.Nat.digits_sum_le_mul_digits_length line 56 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, List.sum, Nat.digits, HMul.hMul, List.length, HSub.hSub

    Proof uses: List.sum_le_length_nsmul, Membership.mem, List, Eq.mpr, id, Eq, congrArg, propext, Nat.le_sub_one_iff_lt, Nat.zero_lt_of_lt, Nat.digits_lt_base

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  7. theorem Imo1975P4.Nat.digits_sum_le_log line 62 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, LT.lt, LE.le, List.sum, Nat.digits, HMul.hMul, HAdd.hAdd, Nat.log, HSub.hSub

    Proof uses: Eq.mpr, List.length, id, Eq, congrArg, Eq.symm, Nat.length_digits, Imo1975P4.Nat.digits_sum_le_mul_digits_length

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  8. theorem Imo1975P4.Nat.digits_sum_le_of_le line 66 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, List.sum, Nat.digits, HMul.hMul, HAdd.hAdd, Nat.clog, HSub.hSub

    Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, List, List.nil, Nat.digits_zero, Eq.symm, Not, Trans.simple, Nat.log, Imo1975P4.Nat.digits_sum_le_log, Eq.mpr, id, propext, mul_le_mul_iff_left₀, add_le_add_iff_right and 4 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  9. theorem Imo1975P4.Nat.clog_pow_le_clog_mul line 77 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Nat.clog, HPow.hPow, HMul.hMul

    Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congr, congrArg, pow_zero, Nat.clog_one_right, MulZeroClass.mul_zero, Eq.symm, Not, Eq.mpr, id, propext, Nat.clog_le_iff_le_pow, pow_mul, Nat.pow_le_pow_iff_left, Nat.le_pow_clog

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  10. problem Imo1975P4.imo1975_p4 line 87 source

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

    Statement uses: Eq, Nat, Imo1975P4.sum_digits_B, List.sum, Nat.digits, OfNat.ofNat, Imo1975P4.B

    Proof uses: Nat.ModEq, HPow.hPow, Eq.mpr, HMod.hMod, id, congrArg, Nat.ModEq.eq_1, Nat.pow_mod, of_eq_true, eq_self, HAdd.hAdd, HMul.hMul, congrFun', Eq.trans, pow_add, congr, pow_mul, pow_one, Nat.mul_mod, one_pow and 23 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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