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 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem9.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
stirlinglem9.3 ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
stirlinglem9.4 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
Assertion stirlinglem9 ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 stirlinglem9.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 stirlinglem9.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
3 stirlinglem9.3 ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
4 stirlinglem9.4 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
5 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
6 3 4 5 stirlinglem7 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( 𝐽 ‘ 𝑁 ) )
7 1 2 3 stirlinglem4 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐽 ‘ 𝑁 ) )
8 6 7 breqtrrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) )