This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stirlinglem9

Description: ( ( BN ) - ( B( N + 1 ) ) ) is expressed as a limit of a series. This result will be used both to prove that B is decreasing and to prove that B is bounded (below). It will follow that B converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem9.1 ⊢ A = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
stirlinglem9.2 ⊢ B = n ∈ ℕ ⟼ log ⁡ A ⁡ n
stirlinglem9.3 ⊢ J = n ∈ ℕ ⟼ 1 + 2 ⁢ n 2 ⁢ log ⁡ n + 1 n − 1
stirlinglem9.4 ⊢ K = k ∈ ℕ ⟼ 1 2 ⁢ k + 1 ⁢ 1 2 ⋅ N + 1 2 ⁢ k
Assertion stirlinglem9 ⊢ N ∈ ℕ → seq 1 + K ⇝ B ⁡ N − B ⁡ N + 1

Proof

Step Hyp Ref Expression
1 stirlinglem9.1 ⊢ A = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
2 stirlinglem9.2 ⊢ B = n ∈ ℕ ⟼ log ⁡ A ⁡ n
3 stirlinglem9.3 ⊢ J = n ∈ ℕ ⟼ 1 + 2 ⁢ n 2 ⁢ log ⁡ n + 1 n − 1
4 stirlinglem9.4 ⊢ K = k ∈ ℕ ⟼ 1 2 ⁢ k + 1 ⁢ 1 2 ⋅ N + 1 2 ⁢ k
5 eqid ⊢ k ∈ ℕ 0 ⟼ 2 ⁢ 1 2 ⁢ k + 1 ⁢ 1 2 ⋅ N + 1 2 ⁢ k + 1 = k ∈ ℕ 0 ⟼ 2 ⁢ 1 2 ⁢ k + 1 ⁢ 1 2 ⋅ N + 1 2 ⁢ k + 1
6 3 4 5 stirlinglem7 ⊢ N ∈ ℕ → seq 1 + K ⇝ J ⁡ N
7 1 2 3 stirlinglem4 ⊢ N ∈ ℕ → B ⁡ N − B ⁡ N + 1 = J ⁡ N
8 6 7 breqtrrd ⊢ N ∈ ℕ → seq 1 + K ⇝ B ⁡ N − B ⁡ N + 1