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

Metamath Proof Explorer

Theorem stirling

Description: Stirling's approximation formula for n factorial. The proof follows two major steps: first it is proven that S and n factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis stirling.1 ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
Assertion stirling ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1

Proof

Step Hyp Ref Expression
1 stirling.1 ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
2 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
3 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ) )
4 2 3 stirlinglem14 ⊢ ∃ 𝑐 ∈ ℝ+ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐
5 nfv ⊢ Ⅎ 𝑛 𝑐 ∈ ℝ+
6 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
7 nfcv ⊢ Ⅎ 𝑛 ⇝
8 nfcv ⊢ Ⅎ 𝑛 𝑐
9 6 7 8 nfbr ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐
10 5 9 nfan ⊢ Ⅎ 𝑛 ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 )
11 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) )
12 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
13 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
14 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ↑ 4 ) / ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) ‘ 𝑛 ) ↑ 2 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ 𝑛 ) ↑ 4 ) / ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ‘ ( 2 · 𝑛 ) ) ) ‘ 𝑛 ) ↑ 2 ) ) )
15 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
16 simpl ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → 𝑐 ∈ ℝ+ )
17 simpr ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 )
18 10 1 2 11 12 13 14 15 16 17 stirlinglem15 ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 ) → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )
19 18 rexlimiva ⊢ ( ∃ 𝑐 ∈ ℝ+ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) ⇝ 𝑐 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )
20 4 19 ax-mp ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1