/- 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 FormalConjecturesUtil

Erdős Problem 933

References:

    erdosproblems.com/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 Erdos933

The 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 declaration uses 'sorry'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 declaration uses 'sorry'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