/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 933
[Er76d] Erdős, P, Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.
open Filter
namespace Erdos933The 2-adic valuation of $n(n+1)$.
def k (n : ℕ) : ℕ := padicValNat 2 (n * (n + 1))The 3-adic valuation of $n(n+1)$.
def l (n : ℕ) : ℕ := padicValNat 3 (n * (n + 1))
If $n(n+1)=2^k3^lm$, where $(m,6)=1$, then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$?
@[category research open, AMS 11]
theorem erdos_933 :
answer(sorry) ↔
atTop.limsup (fun n : ℕ ↦
((((2 ^ k n * 3 ^ l n : ℕ) : ℝ) / ((n : ℝ) * Real.log (n : ℝ))) : EReal)) = ⊤ := ⊢ True ↔ limsup (fun n => ↑↑(2 ^ k n * 3 ^ l n) / (↑↑n * ↑(Real.log ↑n))) atTop = ⊤
All goals completed! 🐙
Mahler proved (a more general result that implies in particular) that $2^k3^l<n^{1+o(1)}$.
@[category research solved, AMS 11]
theorem erdos_933.variants.mahler :
∃ c : ℕ → ℝ, (c =o[atTop] (1 : ℕ → ℝ)) ∧
∀ᶠ n in atTop, ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) < (n : ℝ) ^ (1 + c n) := ⊢ ∃ c, c =o[atTop] 1 ∧ ∀ᶠ (n : ℕ) in atTop, ↑(2 ^ k n * 3 ^ l n) < ↑n ^ (1 + c n)
All goals completed! 🐙
Erdős [Er76d] wrote 'it is easy to see' that for infinitely many $n$, $2^k 3^l > n\log n$.
Steinerberger has noted a simple proof of this fact follows from taking $n=2^{3^r}$ for any integer $r\geq 1$, when $k=3^r$ and $l=r+1$.
@[category research solved, AMS 11]
theorem erdos_933.variants.lower_bound :
Set.Infinite { n : ℕ | ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) > (n : ℝ) * Real.log (n : ℝ) } := ⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite
-- Witness: n = 2^(3^(r+1)); k n = 3^(r+1), l n = r+2 by LTE, and 3 > log 2.
⊢ Function.Injective fun r => 2 ^ 3 ^ (r + 1)r:ℕ⊢ (fun r => 2 ^ 3 ^ (r + 1)) r ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
⊢ Function.Injective fun r => 2 ^ 3 ^ (r + 1) exact (Nat.pow_right_injective (a := 2) (⊢ 2 ≤ 2 All goals completed! 🐙)).comp
((Nat.pow_right_injective (a := 3) (⊢ 2 ≤ 3 All goals completed! 🐙)).comp (add_left_injective 1))
r:ℕm:ℕ := 3 ^ (r + 1)⊢ (fun r => 2 ^ 3 ^ (r + 1)) r ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
have hk : k (2 ^ m) = m := ⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite
All goals completed! 🐙
have hl : l (2 ^ m) = r + 2 := ⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))⊢ padicValNat 3 (2 ^ m + 1) = r + 2
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))⊢ padicValNat 3 (2 + 1) + padicValNat 3 m = r + 2
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))⊢ 1 + (r + 1) = r + 2
All goals completed! 🐙
have hlog : (m : ℝ) * Real.log 2 < (3 : ℝ) ^ (r + 2) := ⊢ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}.Infinite
calc
_ < (m : ℝ) * 3 := mul_lt_mul_of_pos_left (r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))⊢ Real.log 2 < 3 All goals completed! 🐙) (r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))⊢ 0 < ↑m All goals completed! 🐙)
_ = _ := r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))⊢ ↑m * 3 = 3 ^ (r + 2) All goals completed! 🐙
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))hlog:↑m * Real.log 2 < 3 ^ (r + 2) :=
Trans.trans
(mul_lt_mul_of_pos_left
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 360445753))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 360445753))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 360445753))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0)))
(Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 3)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)
(Eq.refl 468750000)))
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Eq.refl (Int.negOfNat 156250000)))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 468750000)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.zero_mul
(Nat.rawCast 3 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 468750000 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 360445753))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 468750000))
(Eq.refl (Int.ofNat 108304247)))))
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 156250000)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 108304247))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 108304247 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Eq.refl (Int.negOfNat 108304247)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 108304247).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 108304247)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 156250000))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.add_neg
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)) (Eq.refl false)))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false))))
(Eq.mp
(congrArg (fun _a => _a < 0)
(CancelDenoms.derive_trans
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 6931471808 6931471808
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow)
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(Mathlib.Meta.NormNum.IsNatPowT.trans
(Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
Mathlib.Meta.NormNum.IsNatPowT.bit1)
Mathlib.Meta.NormNum.IsNatPowT.bit0)))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 6931471808) 6931471808
(Mathlib.Meta.NormNum.isNat_intOfNat
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 6931471808 1)) (Eq.refl 10000000000))))))))
(Eq.refl 108304247) (Eq.refl 156250000)))
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))))
(CancelDenoms.sub_subst rfl
(CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 156250000 1)) (Eq.refl 156250000))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl 156250000))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))))))
(Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false)))))))
(Nat.cast_pos'.mpr
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl (Nat.ble 1 3)))
(r + 1))))
(of_eq_true
(Eq.trans
(Eq.trans
(congr
(congrArg (fun x => Eq (x * 3))
(Eq.trans (Eq.trans (congrArg Nat.cast (pow_succ 3 r)) (Nat.cast_mul (3 ^ r) 3))
(congr
(congrArg HMul.hMul
(Eq.trans (Nat.cast_pow 3 r)
(congrArg (fun x => x ^ r)
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Eq.trans (pow_succ 3 (r + 1)) (congrArg (fun x => x * 3) (pow_succ 3 r))))
(eq_self (3 ^ r * 3 * 3)))
(eq_true True.intro)))⊢ 2 ^ m ∈ {n | ↑(2 ^ k n * 3 ^ l n) > ↑n * Real.log ↑n}
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))hlog:↑m * Real.log 2 < 3 ^ (r + 2) :=
Trans.trans
(mul_lt_mul_of_pos_left
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 360445753))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 360445753))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 360445753))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0)))
(Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 3)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)
(Eq.refl 468750000)))
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Eq.refl (Int.negOfNat 156250000)))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 468750000)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.zero_mul
(Nat.rawCast 3 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 468750000 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 360445753))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 468750000))
(Eq.refl (Int.ofNat 108304247)))))
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 156250000)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 108304247))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 108304247 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Eq.refl (Int.negOfNat 108304247)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 108304247).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 108304247)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 156250000))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.add_neg
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)) (Eq.refl false)))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false))))
(Eq.mp
(congrArg (fun _a => _a < 0)
(CancelDenoms.derive_trans
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 6931471808 6931471808
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow)
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(Mathlib.Meta.NormNum.IsNatPowT.trans
(Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
Mathlib.Meta.NormNum.IsNatPowT.bit1)
Mathlib.Meta.NormNum.IsNatPowT.bit0)))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 6931471808) 6931471808
(Mathlib.Meta.NormNum.isNat_intOfNat
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 6931471808 1)) (Eq.refl 10000000000))))))))
(Eq.refl 108304247) (Eq.refl 156250000)))
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))))
(CancelDenoms.sub_subst rfl
(CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 156250000 1)) (Eq.refl 156250000))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl 156250000))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))))))
(Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false)))))))
(Nat.cast_pos'.mpr
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl (Nat.ble 1 3)))
(r + 1))))
(of_eq_true
(Eq.trans
(Eq.trans
(congr
(congrArg (fun x => Eq (x * 3))
(Eq.trans (Eq.trans (congrArg Nat.cast (pow_succ 3 r)) (Nat.cast_mul (3 ^ r) 3))
(congr
(congrArg HMul.hMul
(Eq.trans (Nat.cast_pow 3 r)
(congrArg (fun x => x ^ r)
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Eq.trans (pow_succ 3 (r + 1)) (congrArg (fun x => x * 3) (pow_succ 3 r))))
(eq_self (3 ^ r * 3 * 3)))
(eq_true True.intro)))⊢ ↑(2 ^ m * 3 ^ (r + 2)) > ↑(2 ^ m) * Real.log ↑(2 ^ m)
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))hlog:↑m * Real.log 2 < 3 ^ (r + 2) :=
Trans.trans
(mul_lt_mul_of_pos_left
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 360445753))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 360445753))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 360445753))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0)))
(Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 3)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)
(Eq.refl 468750000)))
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Eq.refl (Int.negOfNat 156250000)))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 468750000)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.zero_mul
(Nat.rawCast 3 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 468750000 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 360445753))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 468750000))
(Eq.refl (Int.ofNat 108304247)))))
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 156250000)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 108304247))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 108304247 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Eq.refl (Int.negOfNat 108304247)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 108304247).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 108304247)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 156250000))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.add_neg
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)) (Eq.refl false)))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false))))
(Eq.mp
(congrArg (fun _a => _a < 0)
(CancelDenoms.derive_trans
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 6931471808 6931471808
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow)
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(Mathlib.Meta.NormNum.IsNatPowT.trans
(Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
Mathlib.Meta.NormNum.IsNatPowT.bit1)
Mathlib.Meta.NormNum.IsNatPowT.bit0)))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 6931471808) 6931471808
(Mathlib.Meta.NormNum.isNat_intOfNat
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 6931471808 1)) (Eq.refl 10000000000))))))))
(Eq.refl 108304247) (Eq.refl 156250000)))
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))))
(CancelDenoms.sub_subst rfl
(CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 156250000 1)) (Eq.refl 156250000))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl 156250000))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))))))
(Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false)))))))
(Nat.cast_pos'.mpr
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl (Nat.ble 1 3)))
(r + 1))))
(of_eq_true
(Eq.trans
(Eq.trans
(congr
(congrArg (fun x => Eq (x * 3))
(Eq.trans (Eq.trans (congrArg Nat.cast (pow_succ 3 r)) (Nat.cast_mul (3 ^ r) 3))
(congr
(congrArg HMul.hMul
(Eq.trans (Nat.cast_pow 3 r)
(congrArg (fun x => x ^ r)
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Eq.trans (pow_succ 3 (r + 1)) (congrArg (fun x => x * 3) (pow_succ 3 r))))
(eq_self (3 ^ r * 3 * 3)))
(eq_true True.intro)))⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * Real.log (2 ^ m)
r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))hlog:↑m * Real.log 2 < 3 ^ (r + 2) :=
Trans.trans
(mul_lt_mul_of_pos_left
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 360445753))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 360445753))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 360445753))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0)))
(Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 3)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)
(Eq.refl 468750000)))
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Eq.refl (Int.negOfNat 156250000)))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 468750000)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.zero_mul
(Nat.rawCast 3 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 468750000 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 360445753))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 468750000))
(Eq.refl (Int.ofNat 108304247)))))
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 156250000)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 108304247))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 108304247 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Eq.refl (Int.negOfNat 108304247)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 108304247).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 108304247)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 156250000))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.add_neg
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)) (Eq.refl false)))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false))))
(Eq.mp
(congrArg (fun _a => _a < 0)
(CancelDenoms.derive_trans
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 6931471808 6931471808
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow)
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(Mathlib.Meta.NormNum.IsNatPowT.trans
(Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
Mathlib.Meta.NormNum.IsNatPowT.bit1)
Mathlib.Meta.NormNum.IsNatPowT.bit0)))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 6931471808) 6931471808
(Mathlib.Meta.NormNum.isNat_intOfNat
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 6931471808 1)) (Eq.refl 10000000000))))))))
(Eq.refl 108304247) (Eq.refl 156250000)))
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))))
(CancelDenoms.sub_subst rfl
(CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 156250000 1)) (Eq.refl 156250000))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl 156250000))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))))))
(Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false)))))))
(Nat.cast_pos'.mpr
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl (Nat.ble 1 3)))
(r + 1))))
(of_eq_true
(Eq.trans
(Eq.trans
(congr
(congrArg (fun x => Eq (x * 3))
(Eq.trans (Eq.trans (congrArg Nat.cast (pow_succ 3 r)) (Nat.cast_mul (3 ^ r) 3))
(congr
(congrArg HMul.hMul
(Eq.trans (Nat.cast_pow 3 r)
(congrArg (fun x => x ^ r)
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Eq.trans (pow_succ 3 (r + 1)) (congrArg (fun x => x * 3) (pow_succ 3 r))))
(eq_self (3 ^ r * 3 * 3)))
(eq_true True.intro)))⊢ 2 ^ m * 3 ^ (r + 2) > 2 ^ m * (↑m * Real.log 2)
exact mul_lt_mul_of_pos_left hlog (r:ℕm:ℕ := 3 ^ (r + 1)hk:k (2 ^ m) = m :=
Eq.mpr (id (congrArg (fun _a => _a = m) (k.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = m)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr (id (congrArg (fun _a => _a + padicValNat 2 (2 ^ m + 1) = m) (padicValNat.prime_pow m)))
(Eq.mpr
(id
(congrArg (fun _a => m + _a = m)
(padicValNat.eq_zero_of_not_dvd
(Odd.not_two_dvd_nat
(Even.add_one
(Even.pow_of_ne_zero
((Iff.symm Nat.even_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))))
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Eq.refl (Nat.ble 1 3)))
(r + 1)))))))))
(Eq.mpr (id (congrArg (fun _a => _a = m) (add_zero m))) (Eq.refl m)))))hl:l (2 ^ m) = r + 2 :=
Eq.mpr (id (congrArg (fun _a => _a = r + 2) (l.eq_1 (2 ^ m))))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.mul
(ne_of_gt
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m))
(ne_of_gt
(add_pos'
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Eq.refl (Nat.ble 1 2)))
m)
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
(Eq.refl (Nat.ble 1 1))))))))
(Eq.mpr
(id
(congrArg (fun _a => _a + padicValNat 3 (2 ^ m + 1) = r + 2)
(padicValNat_prime_prime_pow m
(Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))))
(Eq.mpr (id (congrArg (fun _a => _a = r + 2) (zero_add (padicValNat 3 (2 ^ m + 1)))))
(Eq.mpr
(id
(congrArg (fun _a => padicValNat 3 _a = r + 2)
(have this :=
of_eq_true
(Eq.trans
(Eq.trans (congrArg (fun x => 2 ^ m + 1 = 2 ^ m + x) (one_pow m)) Nat.add_left_cancel_iff._simp_1)
(eq_self 1));
this)))
(Eq.mpr
(id
(congrArg (fun _a => _a = r + 2)
(padicValNat.pow_add_pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))))
(Mathlib.Meta.NormNum.isNat_dvd_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 3))
(Eq.refl 0))
(Mathlib.Meta.NormNum.isNat_dvd_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.succ 1)))
(id
(Odd.pow
((Iff.symm Nat.odd_iff).mp
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_natMod (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 1))
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))))))))
(Eq.mpr
(id
(congrArg (fun x => x = r + 2)
(congr (congrArg HAdd.hAdd (padicValNat.self (of_eq_true Nat.one_lt_ofNat._simp_1)))
(padicValNat.prime_pow (r + 1)))))
(Decidable.byContradiction fun a => lower_bound._proof_3 r a)))))))hlog:↑m * Real.log 2 < 3 ^ (r + 2) :=
Trans.trans
(mul_lt_mul_of_pos_left
(lt_of_not_ge fun a =>
Mathlib.Tactic.Linarith.lt_irrefl
(Eq.mp
(congrArg (fun _a => _a < 0)
(Mathlib.Tactic.Ring.of_eq
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.add_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)))
(Mathlib.Tactic.Ring.neg_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1)))))
Mathlib.Tactic.Ring.neg_zero))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 360445753))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 360445753))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 360445753))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0)))
(Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 360445753).rawCast + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_mul (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
(Eq.refl (Int.negOfNat 1))))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 3)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)
(Eq.refl 468750000)))
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Eq.refl (Int.negOfNat 156250000)))))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 468750000)
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.zero_mul
(Nat.rawCast 3 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))
(Mathlib.Tactic.Ring.add_pf_add_zero
(Nat.rawCast 468750000 + (Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap
(Mathlib.Meta.NormNum.IsNat.to_raw_eq
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 360445753))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 468750000))
(Eq.refl (Int.ofNat 108304247)))))
(Mathlib.Tactic.Ring.add_pf_zero_add
(Real.log 2 ^ Nat.rawCast 1 * (Int.negOfNat 156250000).rawCast + 0))))
(Mathlib.Tactic.Ring.sub_congr
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Tactic.Ring.atom_pf (Real.log 2))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add
(Mathlib.Tactic.Ring.mul_pf_right (Real.log 2) (Nat.rawCast 1)
(Mathlib.Tactic.Ring.mul_one (Nat.rawCast 156250000)))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 156250000))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0))))
(Mathlib.Tactic.Ring.mul_congr
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Tactic.Ring.add_mul
(Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 108304247))
(Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0)))
(Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 108304247 + 0))
(Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 108304247 + 0))))
(Mathlib.Tactic.Ring.sub_pf
(Mathlib.Tactic.Ring.neg_add
(Mathlib.Tactic.Ring.neg_one_mul
(Mathlib.Meta.NormNum.IsInt.to_raw_eq
(Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Eq.refl (Int.negOfNat 108304247)))))
Mathlib.Tactic.Ring.neg_zero)
(Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 108304247).rawCast
(Mathlib.Tactic.Ring.add_pf_add_zero (Real.log 2 ^ Nat.rawCast 1 * Nat.rawCast 156250000 + 0)))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 108304247))
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 108304247)) (Eq.refl (Int.ofNat 0))))
(Mathlib.Tactic.Ring.add_pf_add_overlap_zero
(Mathlib.Tactic.Ring.add_overlap_pf_zero (Real.log 2) (Nat.rawCast 1)
(Mathlib.Meta.NormNum.IsInt.to_isNat
(Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
(Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 156250000))
(Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 156250000))
(Eq.refl (Int.ofNat 0)))))
(Mathlib.Tactic.Ring.add_pf_zero_add 0))))
(Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
(Mathlib.Tactic.Linarith.add_neg
(Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
(Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 360445753)) (Eq.refl false)))
(Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false))))
(Eq.mp
(congrArg (fun _a => _a < 0)
(CancelDenoms.derive_trans
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true
(Mathlib.Meta.NormNum.isNNRat_ratCast
(Mathlib.Meta.NormNum.IsRat.to_isNNRat
(Mathlib.Meta.NormNum.isRat_mkRat
(Mathlib.Meta.NormNum.IsNat.to_isInt
(Mathlib.Meta.NormNum.isNat_natCast 6931471808 6931471808
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808)))
(Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow)
(Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
(Mathlib.Meta.NormNum.IsNat.raw_refl 10)
(Mathlib.Meta.NormNum.IsNatPowT.run
(Mathlib.Meta.NormNum.IsNatPowT.trans
(Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
Mathlib.Meta.NormNum.IsNatPowT.bit1)
Mathlib.Meta.NormNum.IsNatPowT.bit0)))
(Mathlib.Meta.NormNum.IsNNRat.to_isRat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_intCast (Int.ofNat 6931471808) 6931471808
(Mathlib.Meta.NormNum.isNat_intOfNat
(Mathlib.Meta.NormNum.IsNat.raw_refl 6931471808))))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_natCast 10000000000 10000000000
(Mathlib.Meta.NormNum.IsNat.raw_refl 10000000000))))
(Eq.refl (Nat.mul 6931471808 1)) (Eq.refl 10000000000))))))))
(Eq.refl 108304247) (Eq.refl 156250000)))
(Eq.trans
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))
(congrArg (HSub.hSub (Real.log 2))
(Mathlib.Meta.NormNum.IsNNRat.to_eq
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 108304247)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 108304247 1)) (Eq.refl 156250000)))
(Eq.refl 108304247) (Eq.refl 156250000)))))
(CancelDenoms.sub_subst rfl
(CancelDenoms.div_subst rfl
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_div
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.IsNNRat.to_isNat
(Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))
(Mathlib.Meta.NormNum.isNNRat_inv_pos
(Mathlib.Meta.NormNum.IsNat.to_isNNRat
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000))))
(Eq.refl (Nat.mul 156250000 1)) (Eq.refl 156250000))))))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
(Mathlib.Meta.NormNum.isNat_eq_true
(Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl 156250000))
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)))))))
(Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9)
(Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
(Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 156250000)) (Eq.refl false)))))))
(Nat.cast_pos'.mpr
(pow_pos
(Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)) (Eq.refl (Nat.ble 1 3)))
(r + 1))))
(of_eq_true
(Eq.trans
(Eq.trans
(congr
(congrArg (fun x => Eq (x * 3))
(Eq.trans (Eq.trans (congrArg Nat.cast (pow_succ 3 r)) (Nat.cast_mul (3 ^ r) 3))
(congr
(congrArg HMul.hMul
(Eq.trans (Nat.cast_pow 3 r)
(congrArg (fun x => x ^ r)
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Mathlib.Meta.NormNum.IsNat.to_eq
(Mathlib.Meta.NormNum.isNat_natCast 3 3 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 3)))
(Eq.refl 3)))))
(Eq.trans (pow_succ 3 (r + 1)) (congrArg (fun x => x * 3) (pow_succ 3 r))))
(eq_self (3 ^ r * 3 * 3)))
(eq_true True.intro)))⊢ 0 < 2 ^ m All goals completed! 🐙)
end Erdos933