Theorem: exp_div_lt (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 (2.7182818286 ^ a < c ^ b) _auto✝
⊢ (↑a / ↑b).exp < c
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 (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ (↑a / ↑b).exp < c

State before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ (↑a / ↑b).exp < c
Tactic:
rw [e, div_eq_mul_inv, Real.rpow_mul (Real.exp_nonneg _), Real.rpow_inv_lt_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 (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ exp 1 ^ a < c ^ b

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

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

case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _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 (2.7182818286 ^ a < c ^ b) _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 (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ exp 1 ^ a < c ^ b
Tactic:
exact _root_.trans (pow_lt_pow_left Real.exp_one_lt_d9 (Real.exp_nonneg _) a0) h0
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 (2.7182818286 ^ a < c ^ b) _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 hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c
Tactic:
exact c0.le
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 (2.7182818286 ^ a < c ^ b) _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 (2.7182818286 ^ a < c ^ b) _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 (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Tactic:
exact b0
State after:
no goals