Theorem: lt_exp_neg_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 (2.7182818286 ^ a < c⁻¹ ^ b) _auto✝
⊢ c < (-(↑a / ↑b)).exp
Tactic:
rw [Real.exp_neg, lt_inv c0 (Real.exp_pos _)]
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✝
⊢ (↑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✝
⊢ (↑a / ↑b).exp < c⁻¹
Tactic:
exact exp_div_lt a0 b0 (inv_pos.mpr c0) h0
State after:
no goals