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

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ (-↑a).exp < b
Tactic:
rw [Real.exp_neg, inv_lt, ←Real.exp_one_pow a]
State after:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ b⁻¹ < exp 1 ^ a

case ha
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < (↑a).exp

case hb
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < b

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 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 : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
State after:
no goals

State before:
case ha
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < (↑a).exp
Tactic:
exact Real.exp_pos _
State after:
no goals

State before:
case hb
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < b
Tactic:
exact b0
State after:
no goals