Theorem: exp_factorial_bound (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ rexp x
Tactic:
rw [exp_eq_exp_ℝ]
State after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ _root_.exp ℝ x

State before:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ _root_.exp ℝ x
Tactic:
exact le_hasSum (expSeries_div_hasSum_exp ℝ x) n (fun _ _ => by positivity)
State after:
no goals

State before:
x : ℝ
hx : 0 ≤ x
n x✝¹ : ℕ
x✝ : x✝¹ ≠ n
⊢ 0 ≤ x ^ x✝¹ / ↑x✝¹!
Tactic:
positivity
State after:
no goals