# Metamath Proof Explorer

## Theorem stirlingr

Description: Stirling's approximation formula for n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling is proven for convergence in the topology of complex numbers. The variable R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlingr.1 ${⊢}{S}=\left({n}\in {ℕ}_{0}⟼\sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\right)$
stirlingr.2
Assertion stirlingr ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right){R}1$

### Proof

Step Hyp Ref Expression
1 stirlingr.1 ${⊢}{S}=\left({n}\in {ℕ}_{0}⟼\sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\right)$
2 stirlingr.2
3 1 stirling ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right)⇝1$
4 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
5 1zzd ${⊢}\top \to 1\in ℤ$
6 eqid ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right)=\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right)$
7 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
8 faccl ${⊢}{n}\in {ℕ}_{0}\to {n}!\in ℕ$
9 nnre ${⊢}{n}!\in ℕ\to {n}!\in ℝ$
10 7 8 9 3syl ${⊢}{n}\in ℕ\to {n}!\in ℝ$
11 2re ${⊢}2\in ℝ$
12 11 a1i ${⊢}{n}\in ℕ\to 2\in ℝ$
13 pire ${⊢}\mathrm{\pi }\in ℝ$
14 13 a1i ${⊢}{n}\in ℕ\to \mathrm{\pi }\in ℝ$
15 12 14 remulcld ${⊢}{n}\in ℕ\to 2\mathrm{\pi }\in ℝ$
16 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
17 15 16 remulcld ${⊢}{n}\in ℕ\to 2\mathrm{\pi }{n}\in ℝ$
18 0re ${⊢}0\in ℝ$
19 18 a1i ${⊢}{n}\in ℕ\to 0\in ℝ$
20 2pos ${⊢}0<2$
21 20 a1i ${⊢}{n}\in ℕ\to 0<2$
22 19 12 21 ltled ${⊢}{n}\in ℕ\to 0\le 2$
23 pipos ${⊢}0<\mathrm{\pi }$
24 18 13 23 ltleii ${⊢}0\le \mathrm{\pi }$
25 24 a1i ${⊢}{n}\in ℕ\to 0\le \mathrm{\pi }$
26 12 14 22 25 mulge0d ${⊢}{n}\in ℕ\to 0\le 2\mathrm{\pi }$
27 7 nn0ge0d ${⊢}{n}\in ℕ\to 0\le {n}$
28 15 16 26 27 mulge0d ${⊢}{n}\in ℕ\to 0\le 2\mathrm{\pi }{n}$
29 17 28 resqrtcld ${⊢}{n}\in ℕ\to \sqrt{2\mathrm{\pi }{n}}\in ℝ$
30 ere ${⊢}\mathrm{e}\in ℝ$
31 30 a1i ${⊢}{n}\in ℕ\to \mathrm{e}\in ℝ$
32 epos ${⊢}0<\mathrm{e}$
33 18 32 gtneii ${⊢}\mathrm{e}\ne 0$
34 33 a1i ${⊢}{n}\in ℕ\to \mathrm{e}\ne 0$
35 16 31 34 redivcld ${⊢}{n}\in ℕ\to \frac{{n}}{\mathrm{e}}\in ℝ$
36 35 7 reexpcld ${⊢}{n}\in ℕ\to {\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in ℝ$
37 29 36 remulcld ${⊢}{n}\in ℕ\to \sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in ℝ$
38 1 fvmpt2 ${⊢}\left({n}\in {ℕ}_{0}\wedge \sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in ℝ\right)\to {S}\left({n}\right)=\sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}$
39 7 37 38 syl2anc ${⊢}{n}\in ℕ\to {S}\left({n}\right)=\sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}$
40 2rp ${⊢}2\in {ℝ}^{+}$
41 40 a1i ${⊢}{n}\in ℕ\to 2\in {ℝ}^{+}$
42 pirp ${⊢}\mathrm{\pi }\in {ℝ}^{+}$
43 42 a1i ${⊢}{n}\in ℕ\to \mathrm{\pi }\in {ℝ}^{+}$
44 41 43 rpmulcld ${⊢}{n}\in ℕ\to 2\mathrm{\pi }\in {ℝ}^{+}$
45 nnrp ${⊢}{n}\in ℕ\to {n}\in {ℝ}^{+}$
46 44 45 rpmulcld ${⊢}{n}\in ℕ\to 2\mathrm{\pi }{n}\in {ℝ}^{+}$
47 46 rpsqrtcld ${⊢}{n}\in ℕ\to \sqrt{2\mathrm{\pi }{n}}\in {ℝ}^{+}$
48 epr ${⊢}\mathrm{e}\in {ℝ}^{+}$
49 48 a1i ${⊢}{n}\in ℕ\to \mathrm{e}\in {ℝ}^{+}$
50 45 49 rpdivcld ${⊢}{n}\in ℕ\to \frac{{n}}{\mathrm{e}}\in {ℝ}^{+}$
51 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
52 50 51 rpexpcld ${⊢}{n}\in ℕ\to {\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in {ℝ}^{+}$
53 47 52 rpmulcld ${⊢}{n}\in ℕ\to \sqrt{2\mathrm{\pi }{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in {ℝ}^{+}$
54 39 53 eqeltrd ${⊢}{n}\in ℕ\to {S}\left({n}\right)\in {ℝ}^{+}$
55 10 54 rerpdivcld ${⊢}{n}\in ℕ\to \frac{{n}!}{{S}\left({n}\right)}\in ℝ$
56 6 55 fmpti ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right):ℕ⟶ℝ$
57 56 a1i ${⊢}\top \to \left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right):ℕ⟶ℝ$
58 2 4 5 57 climreeq ${⊢}\top \to \left(\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right){R}1↔\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right)⇝1\right)$
59 58 mptru ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right){R}1↔\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right)⇝1$
60 3 59 mpbir ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{{S}\left({n}\right)}\right){R}1$