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

State before:
n : ℝ
hn : 0 < n
⊢ 4 ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [(by norm_num : (4 : ℝ) = 2 ^ 2)]
State after:
n : ℝ
hn : 0 < n
⊢ (2 ^ 2) ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
⊢ (2 ^ 2) ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [← Real.rpow_mul (by norm_num)]
State after:
n : ℝ
hn : 0 < n
⊢ 2 ^ (2 * n) < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
⊢ 2 ^ (2 * n) < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [Real.rpow_lt_rpow_left_iff (by linarith)]
State after:
n : ℝ
hn : 0 < n
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Tactic:
have h_nonneg : 0 < (2 * n) ^ (2 / 3) := by apply Real.rpow_pos_of_pos; linarith
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Tactic:
rw [← @Real.rpow_lt_rpow_iff _ _ 3 (by linarith) (by linarith) (by norm_num)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < (20 * (2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < (20 * (2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Tactic:
rw [@Real.mul_rpow 20 _ _ (by norm_num) (by linarith)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * ((2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * ((2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Tactic:
rw [← Real.rpow_mul (by linarith)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ (2 / 3 * 3) ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ (2 / 3 * 3) ↔ n < 4000
Tactic:
simp
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [(by norm_num : (3:ℝ) = 1 + 2)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ (1 + 2) < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ (1 + 2) < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [@Real.rpow_add (2*n) (by linarith)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [@Real.rpow_add 20 (by norm_num)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ 1 * 20 ^ 2 * (2 * n) ^ 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ 1 * 20 ^ 2 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
norm_num
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n * (2 * n) ^ 2 < 8000 * (2 * n) ^ 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n * (2 * n) ^ 2 < 8000 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [mul_lt_mul_right (by apply sq_pos_of_pos; linarith)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 8000 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 8000 ↔ n < 4000
Tactic:
rw [mul_comm]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n * 2 < 8000 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n * 2 < 8000 ↔ n < 4000
Tactic:
rw [← lt_div_iff (by norm_num)]
State after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n < 8000 / 2 ↔ n < 4000

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n < 8000 / 2 ↔ n < 4000
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 0 < n
⊢ 4 = 2 ^ 2
Tactic:
norm_num
State after:
no goals

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

State before:
n : ℝ
hn : 0 < n
⊢ 1 < 2
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
⊢ 0 < (2 * n) ^ (2 / 3)
Tactic:
apply Real.rpow_pos_of_pos
State after:
case hx
n : ℝ
hn : 0 < n
⊢ 0 < 2 * n

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

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 20 * (2 * n) ^ (2 / 3)
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 20
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ (2 * n) ^ (2 / 3)
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 3 = 1 + 2
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 20
Tactic:
norm_num
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < (2 * n) ^ 2
Tactic:
apply sq_pos_of_pos
State after:
case ha
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n

State before:
case ha
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals