Theorem: twoMulLtTwoPow (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
n : ℝ
hn : 32 ≤ n
⊢ 2 * n = (2 * n) ^ (6⁻¹ * 6)
Tactic:
simp
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ (6⁻¹ * 6) = ((2 * n) ^ 6⁻¹) ^ 6
Tactic:
apply Real.rpow_mul (by linarith)
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ ((2 * n) ^ 6⁻¹) ^ 6 < (↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6
Tactic:
apply Real.rpow_lt_rpow _ _ (by norm_num)
State after:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1

State before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
. apply Real.rpow_nonneg_of_nonneg; linarith
State after:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1

State before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
. apply Nat.lt_floor_add_one
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ 0 < 6
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_nonneg_of_nonneg
State after:
case hx
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n

State before:
case hx
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
apply Nat.lt_floor_add_one
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ (↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊)
Tactic:
norm_cast
State after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ⌊(2 * n) ^ 6⁻¹⌋₊)

State before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ⌊(2 * n) ^ 6⁻¹⌋₊)
Tactic:
conv => rhs; rhs; rw [mul_comm]
State after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (⌊(2 * n) ^ 6⁻¹⌋₊ * 6)

State before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (⌊(2 * n) ^ 6⁻¹⌋₊ * 6)
Tactic:
rw [Nat.pow_mul]
State after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < (2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊) ^ 6

State before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < (2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊) ^ 6
Tactic:
apply Nat.pow_lt_pow_of_lt_left _ (by norm_num)
State after:
n : ℝ
hn : 32 ≤ n
⊢ ⌊(2 * n) ^ 6⁻¹⌋₊ + 1 < 2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊

State before:
n : ℝ
hn : 32 ≤ n
⊢ ⌊(2 * n) ^ 6⁻¹⌋₊ + 1 < 2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
apply succLtTwoPow
State after:
case h2
n : ℝ
hn : 32 ≤ n
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊

State before:
case h2
n : ℝ
hn : 32 ≤ n
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
have h0 : 0 ≤ (2 * n) ^ 6⁻¹
State after:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊

State before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
. apply le_of_lt; apply Real.rpow_pos_of_pos; linarith
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
rw [Nat.le_floor_iff h0]
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑2 ≤ (2 * n) ^ 6⁻¹

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑2 ≤ (2 * n) ^ 6⁻¹
Tactic:
norm_cast
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ (2 * n) ^ 6⁻¹

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ (2 * n) ^ 6⁻¹
Tactic:
rw [← Real.rpow_le_rpow_iff (by norm_num) h0 (by norm_num : (0:ℝ) < 6)]
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ ((2 * n) ^ 6⁻¹) ^ 6

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ ((2 * n) ^ 6⁻¹) ^ 6
Tactic:
rw [← Real.rpow_mul (by linarith)]
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ (2 * n) ^ (6⁻¹ * 6)

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ (2 * n) ^ (6⁻¹ * 6)
Tactic:
simp
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ 2 * n

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ 2 * n
Tactic:
rw [mul_comm]
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ n * 2

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ n * 2
Tactic:
rw [← div_le_iff (by norm_num)]
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 / 2 ≤ n

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 / 2 ≤ n
Tactic:
norm_cast
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑(2 ^ 6) / 2 ≤ n

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑(2 ^ 6) / 2 ≤ n
Tactic:
norm_num
State after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 32 ≤ n

State before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 32 ≤ n
Tactic:
assumption
State after:
no goals

State before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹
Tactic:
apply le_of_lt
State after:
case h0.a
n : ℝ
hn : 32 ≤ n
⊢ 0 < (2 * n) ^ 6⁻¹

State before:
case h0.a
n : ℝ
hn : 32 ≤ n
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_pos_of_pos
State after:
case h0.a.hx
n : ℝ
hn : 32 ≤ n
⊢ 0 < 2 * n

State before:
case h0.a.hx
n : ℝ
hn : 32 ≤ n
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 < 6
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ 2 ^ (6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊) ≤ 2 ^ (6 * (2 * n) ^ 6⁻¹)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_num)]
State after:
n : ℝ
hn : 32 ≤ n
⊢ 6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ 6 * (2 * n) ^ 6⁻¹

State before:
n : ℝ
hn : 32 ≤ n
⊢ 6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ 6 * (2 * n) ^ 6⁻¹
Tactic:
rw [mul_le_mul_left (by norm_num)]
State after:
n : ℝ
hn : 32 ≤ n
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹

State before:
n : ℝ
hn : 32 ≤ n
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
have h0 : 0 ≤ (2 * n) ^ 6⁻¹
State after:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹

State before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
. apply le_of_lt; apply Real.rpow_pos_of_pos; linarith
State after:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹

State before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
exact Nat.floor_le h0
State after:
no goals

State before:
n : ℝ
hn : 32 ≤ n
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals