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 ⊢ S = n ∈ ℕ 0 ⟼ 2 ⁢ π ⁢ n ⁢ n e n
Assertion stirling ⊢ n ∈ ℕ ⟼ n ! S ⁡ n ⇝ 1

Proof

Step Hyp Ref Expression
1 stirling.1 ⊢ S = n ∈ ℕ 0 ⟼ 2 ⁢ π ⁢ n ⁢ n e n
2 eqid ⊢ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n = n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
3 eqid ⊢ n ∈ ℕ ⟼ log ⁡ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ n = n ∈ ℕ ⟼ log ⁡ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ n
4 2 3 stirlinglem14 ⊢ ∃ c ∈ ℝ + n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c
5 nfv ⊢ Ⅎ n c ∈ ℝ +
6 nfmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n
7 nfcv ⊢ Ⅎ _ n ⇝
8 nfcv ⊢ Ⅎ _ n c
9 6 7 8 nfbr ⊢ Ⅎ n n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c
10 5 9 nfan ⊢ Ⅎ n c ∈ ℝ + ∧ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c
11 eqid ⊢ n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ 2 ⁢ n = n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ 2 ⁢ n
12 eqid ⊢ n ∈ ℕ ⟼ 2 ⁢ n ⁢ n e n = n ∈ ℕ ⟼ 2 ⁢ n ⁢ n e n
13 eqid ⊢ n ∈ ℕ ⟼ 2 4 ⁢ n ⁢ n ! 4 2 ⁢ n ! 2 2 ⁢ n + 1 = n ∈ ℕ ⟼ 2 4 ⁢ n ⁢ n ! 4 2 ⁢ n ! 2 2 ⁢ n + 1
14 eqid ⊢ n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ n 4 n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ 2 ⁢ n ⁡ n 2 = n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ n 4 n ∈ ℕ ⟼ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⁡ 2 ⁢ n ⁡ n 2
15 eqid ⊢ n ∈ ℕ ⟼ n 2 n ⁢ 2 ⁢ n + 1 = n ∈ ℕ ⟼ n 2 n ⁢ 2 ⁢ n + 1
16 simpl ⊢ c ∈ ℝ + ∧ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c → c ∈ ℝ +
17 simpr ⊢ c ∈ ℝ + ∧ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c → n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c
18 10 1 2 11 12 13 14 15 16 17 stirlinglem15 ⊢ c ∈ ℝ + ∧ n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c → n ∈ ℕ ⟼ n ! S ⁡ n ⇝ 1
19 18 rexlimiva ⊢ ∃ c ∈ ℝ + n ∈ ℕ ⟼ n ! 2 ⁢ n ⁢ n e n ⇝ c → n ∈ ℕ ⟼ n ! S ⁡ n ⇝ 1
20 4 19 ax-mp ⊢ n ∈ ℕ ⟼ n ! S ⁡ n ⇝ 1