Theorem: lt_exp_div (Ray/Dynamics/Multibrot/Specific.lean)

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
⊢ c < (↑a / ↑b).exp
Tactic:
have e : exp (a/b : ℝ) = exp 1 ^ (a / b : ℝ) := by rw [Real.exp_one_rpow]
State after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c < (↑a / ↑b).exp

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c < (↑a / ↑b).exp
Tactic:
rw [e, div_eq_mul_inv, Real.rpow_mul (Real.exp_nonneg _), Real.lt_rpow_inv_iff_of_pos,
  Real.rpow_natCast, Real.rpow_natCast]
State after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c ^ b < exp 1 ^ a

case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c

case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a

case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
⊢ (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
Tactic:
rw [Real.exp_one_rpow]
State after:
no goals

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c ^ b < exp 1 ^ a
Tactic:
exact _root_.trans h0 (pow_lt_pow_left Real.exp_one_gt_d9 (by norm_num) a0)
State after:
no goals

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
State after:
no goals

State before:
case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c
Tactic:
exact c0.le
State after:
no goals

State before:
case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a
Tactic:
apply Real.rpow_nonneg (Real.exp_nonneg _)
State after:
no goals

State before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b
Tactic:
simp only [Nat.cast_pos, Nat.pos_iff_ne_zero]
State after:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0

State before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Tactic:
exact b0
State after:
no goals