case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (succ n)
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (succ n)
cases' log_stirlingSeq_bounded_by_constant with c h
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ exp c ≤ stirlingSeq (succ n)
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (succ n)
refine' ⟨exp c, exp_pos _, fun n => _⟩
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ c ≤ Real.log (stirlingSeq (succ n))
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ exp c ≤ stirlingSeq (succ n)
rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]
no goals
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ c ≤ Real.log (stirlingSeq (succ n))
exact h n