# Metamath Proof Explorer

## Theorem stirlinglem14

Description: The sequence A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem14.1 ${⊢}{A}=\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)$
stirlinglem14.2 ${⊢}{B}=\left({n}\in ℕ⟼\mathrm{log}{A}\left({n}\right)\right)$
Assertion stirlinglem14 ${⊢}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}⇝{c}$

### Proof

Step Hyp Ref Expression
1 stirlinglem14.1 ${⊢}{A}=\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)$
2 stirlinglem14.2 ${⊢}{B}=\left({n}\in ℕ⟼\mathrm{log}{A}\left({n}\right)\right)$
3 1 2 stirlinglem13 ${⊢}\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{B}⇝{d}$
4 simpl ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {d}\in ℝ$
5 4 rpefcld ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {\mathrm{e}}^{{d}}\in {ℝ}^{+}$
6 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
7 1zzd ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to 1\in ℤ$
8 efcn ${⊢}\mathrm{exp}:ℂ\underset{cn}{⟶}ℂ$
9 8 a1i ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to \mathrm{exp}:ℂ\underset{cn}{⟶}ℂ$
10 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
11 faccl ${⊢}{n}\in {ℕ}_{0}\to {n}!\in ℕ$
12 nncn ${⊢}{n}!\in ℕ\to {n}!\in ℂ$
13 10 11 12 3syl ${⊢}{n}\in ℕ\to {n}!\in ℂ$
14 2cnd ${⊢}{n}\in ℕ\to 2\in ℂ$
15 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
16 14 15 mulcld ${⊢}{n}\in ℕ\to 2{n}\in ℂ$
17 16 sqrtcld ${⊢}{n}\in ℕ\to \sqrt{2{n}}\in ℂ$
18 epr ${⊢}\mathrm{e}\in {ℝ}^{+}$
19 rpcn ${⊢}\mathrm{e}\in {ℝ}^{+}\to \mathrm{e}\in ℂ$
20 18 19 ax-mp ${⊢}\mathrm{e}\in ℂ$
21 20 a1i ${⊢}{n}\in ℕ\to \mathrm{e}\in ℂ$
22 0re ${⊢}0\in ℝ$
23 epos ${⊢}0<\mathrm{e}$
24 22 23 gtneii ${⊢}\mathrm{e}\ne 0$
25 24 a1i ${⊢}{n}\in ℕ\to \mathrm{e}\ne 0$
26 15 21 25 divcld ${⊢}{n}\in ℕ\to \frac{{n}}{\mathrm{e}}\in ℂ$
27 26 10 expcld ${⊢}{n}\in ℕ\to {\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in ℂ$
28 17 27 mulcld ${⊢}{n}\in ℕ\to \sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\in ℂ$
29 2rp ${⊢}2\in {ℝ}^{+}$
30 29 a1i ${⊢}{n}\in ℕ\to 2\in {ℝ}^{+}$
31 nnrp ${⊢}{n}\in ℕ\to {n}\in {ℝ}^{+}$
32 30 31 rpmulcld ${⊢}{n}\in ℕ\to 2{n}\in {ℝ}^{+}$
33 32 sqrtgt0d ${⊢}{n}\in ℕ\to 0<\sqrt{2{n}}$
34 33 gt0ne0d ${⊢}{n}\in ℕ\to \sqrt{2{n}}\ne 0$
35 nnne0 ${⊢}{n}\in ℕ\to {n}\ne 0$
36 15 21 35 25 divne0d ${⊢}{n}\in ℕ\to \frac{{n}}{\mathrm{e}}\ne 0$
37 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
38 26 36 37 expne0d ${⊢}{n}\in ℕ\to {\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\ne 0$
39 17 27 34 38 mulne0d ${⊢}{n}\in ℕ\to \sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}\ne 0$
40 13 28 39 divcld ${⊢}{n}\in ℕ\to \frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\in ℂ$
41 1 fvmpt2 ${⊢}\left({n}\in ℕ\wedge \frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\in ℂ\right)\to {A}\left({n}\right)=\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}$
42 40 41 mpdan ${⊢}{n}\in ℕ\to {A}\left({n}\right)=\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}$
43 42 40 eqeltrd ${⊢}{n}\in ℕ\to {A}\left({n}\right)\in ℂ$
44 nnne0 ${⊢}{n}!\in ℕ\to {n}!\ne 0$
45 10 11 44 3syl ${⊢}{n}\in ℕ\to {n}!\ne 0$
46 13 28 45 39 divne0d ${⊢}{n}\in ℕ\to \frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\ne 0$
47 42 46 eqnetrd ${⊢}{n}\in ℕ\to {A}\left({n}\right)\ne 0$
48 43 47 logcld ${⊢}{n}\in ℕ\to \mathrm{log}{A}\left({n}\right)\in ℂ$
49 2 48 fmpti ${⊢}{B}:ℕ⟶ℂ$
50 49 a1i ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {B}:ℕ⟶ℂ$
51 simpr ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {B}⇝{d}$
52 4 recnd ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {d}\in ℂ$
53 6 7 9 50 51 52 climcncf ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to \left(\mathrm{exp}\circ {B}\right)⇝{\mathrm{e}}^{{d}}$
54 8 elexi ${⊢}\mathrm{exp}\in \mathrm{V}$
55 nnex ${⊢}ℕ\in \mathrm{V}$
56 55 mptex ${⊢}\left({n}\in ℕ⟼\mathrm{log}{A}\left({n}\right)\right)\in \mathrm{V}$
57 2 56 eqeltri ${⊢}{B}\in \mathrm{V}$
58 54 57 coex ${⊢}\mathrm{exp}\circ {B}\in \mathrm{V}$
59 58 a1i ${⊢}\top \to \mathrm{exp}\circ {B}\in \mathrm{V}$
60 55 mptex ${⊢}\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)\in \mathrm{V}$
61 1 60 eqeltri ${⊢}{A}\in \mathrm{V}$
62 61 a1i ${⊢}\top \to {A}\in \mathrm{V}$
63 1zzd ${⊢}\top \to 1\in ℤ$
64 2 funmpt2 ${⊢}\mathrm{Fun}{B}$
65 id ${⊢}{k}\in ℕ\to {k}\in ℕ$
66 rabid2 ${⊢}ℕ=\left\{{n}\in ℕ|\mathrm{log}{A}\left({n}\right)\in \mathrm{V}\right\}↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\mathrm{log}{A}\left({n}\right)\in \mathrm{V}$
67 1 stirlinglem2 ${⊢}{n}\in ℕ\to {A}\left({n}\right)\in {ℝ}^{+}$
68 relogcl ${⊢}{A}\left({n}\right)\in {ℝ}^{+}\to \mathrm{log}{A}\left({n}\right)\in ℝ$
69 elex ${⊢}\mathrm{log}{A}\left({n}\right)\in ℝ\to \mathrm{log}{A}\left({n}\right)\in \mathrm{V}$
70 67 68 69 3syl ${⊢}{n}\in ℕ\to \mathrm{log}{A}\left({n}\right)\in \mathrm{V}$
71 66 70 mprgbir ${⊢}ℕ=\left\{{n}\in ℕ|\mathrm{log}{A}\left({n}\right)\in \mathrm{V}\right\}$
72 2 dmmpt ${⊢}\mathrm{dom}{B}=\left\{{n}\in ℕ|\mathrm{log}{A}\left({n}\right)\in \mathrm{V}\right\}$
73 71 72 eqtr4i ${⊢}ℕ=\mathrm{dom}{B}$
74 65 73 eleqtrdi ${⊢}{k}\in ℕ\to {k}\in \mathrm{dom}{B}$
75 fvco ${⊢}\left(\mathrm{Fun}{B}\wedge {k}\in \mathrm{dom}{B}\right)\to \left(\mathrm{exp}\circ {B}\right)\left({k}\right)={\mathrm{e}}^{{B}\left({k}\right)}$
76 64 74 75 sylancr ${⊢}{k}\in ℕ\to \left(\mathrm{exp}\circ {B}\right)\left({k}\right)={\mathrm{e}}^{{B}\left({k}\right)}$
77 1 a1i ${⊢}{k}\in ℕ\to {A}=\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)$
78 simpr ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to {n}={k}$
79 78 fveq2d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to {n}!={k}!$
80 78 oveq2d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to 2{n}=2{k}$
81 80 fveq2d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to \sqrt{2{n}}=\sqrt{2{k}}$
82 78 oveq1d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to \frac{{n}}{\mathrm{e}}=\frac{{k}}{\mathrm{e}}$
83 82 78 oveq12d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to {\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}={\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}$
84 81 83 oveq12d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to \sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}=\sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}$
85 79 84 oveq12d ${⊢}\left({k}\in ℕ\wedge {n}={k}\right)\to \frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}=\frac{{k}!}{\sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}}$
86 nnnn0 ${⊢}{k}\in ℕ\to {k}\in {ℕ}_{0}$
87 faccl ${⊢}{k}\in {ℕ}_{0}\to {k}!\in ℕ$
88 nncn ${⊢}{k}!\in ℕ\to {k}!\in ℂ$
89 86 87 88 3syl ${⊢}{k}\in ℕ\to {k}!\in ℂ$
90 2cnd ${⊢}{k}\in ℕ\to 2\in ℂ$
91 nncn ${⊢}{k}\in ℕ\to {k}\in ℂ$
92 90 91 mulcld ${⊢}{k}\in ℕ\to 2{k}\in ℂ$
93 92 sqrtcld ${⊢}{k}\in ℕ\to \sqrt{2{k}}\in ℂ$
94 20 a1i ${⊢}{k}\in ℕ\to \mathrm{e}\in ℂ$
95 24 a1i ${⊢}{k}\in ℕ\to \mathrm{e}\ne 0$
96 91 94 95 divcld ${⊢}{k}\in ℕ\to \frac{{k}}{\mathrm{e}}\in ℂ$
97 96 86 expcld ${⊢}{k}\in ℕ\to {\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}\in ℂ$
98 93 97 mulcld ${⊢}{k}\in ℕ\to \sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}\in ℂ$
99 29 a1i ${⊢}{k}\in ℕ\to 2\in {ℝ}^{+}$
100 nnrp ${⊢}{k}\in ℕ\to {k}\in {ℝ}^{+}$
101 99 100 rpmulcld ${⊢}{k}\in ℕ\to 2{k}\in {ℝ}^{+}$
102 101 sqrtgt0d ${⊢}{k}\in ℕ\to 0<\sqrt{2{k}}$
103 102 gt0ne0d ${⊢}{k}\in ℕ\to \sqrt{2{k}}\ne 0$
104 nnne0 ${⊢}{k}\in ℕ\to {k}\ne 0$
105 91 94 104 95 divne0d ${⊢}{k}\in ℕ\to \frac{{k}}{\mathrm{e}}\ne 0$
106 nnz ${⊢}{k}\in ℕ\to {k}\in ℤ$
107 96 105 106 expne0d ${⊢}{k}\in ℕ\to {\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}\ne 0$
108 93 97 103 107 mulne0d ${⊢}{k}\in ℕ\to \sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}\ne 0$
109 89 98 108 divcld ${⊢}{k}\in ℕ\to \frac{{k}!}{\sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}}\in ℂ$
110 77 85 65 109 fvmptd ${⊢}{k}\in ℕ\to {A}\left({k}\right)=\frac{{k}!}{\sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}}$
111 110 109 eqeltrd ${⊢}{k}\in ℕ\to {A}\left({k}\right)\in ℂ$
112 nnne0 ${⊢}{k}!\in ℕ\to {k}!\ne 0$
113 86 87 112 3syl ${⊢}{k}\in ℕ\to {k}!\ne 0$
114 89 98 113 108 divne0d ${⊢}{k}\in ℕ\to \frac{{k}!}{\sqrt{2{k}}{\left(\frac{{k}}{\mathrm{e}}\right)}^{{k}}}\ne 0$
115 110 114 eqnetrd ${⊢}{k}\in ℕ\to {A}\left({k}\right)\ne 0$
116 111 115 logcld ${⊢}{k}\in ℕ\to \mathrm{log}{A}\left({k}\right)\in ℂ$
117 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{k}$
118 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}log$
119 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)$
120 1 119 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
121 120 117 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)$
122 118 121 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{log}{A}\left({k}\right)$
123 2fveq3 ${⊢}{n}={k}\to \mathrm{log}{A}\left({n}\right)=\mathrm{log}{A}\left({k}\right)$
124 117 122 123 2 fvmptf ${⊢}\left({k}\in ℕ\wedge \mathrm{log}{A}\left({k}\right)\in ℂ\right)\to {B}\left({k}\right)=\mathrm{log}{A}\left({k}\right)$
125 116 124 mpdan ${⊢}{k}\in ℕ\to {B}\left({k}\right)=\mathrm{log}{A}\left({k}\right)$
126 125 fveq2d ${⊢}{k}\in ℕ\to {\mathrm{e}}^{{B}\left({k}\right)}={\mathrm{e}}^{\mathrm{log}{A}\left({k}\right)}$
127 eflog ${⊢}\left({A}\left({k}\right)\in ℂ\wedge {A}\left({k}\right)\ne 0\right)\to {\mathrm{e}}^{\mathrm{log}{A}\left({k}\right)}={A}\left({k}\right)$
128 111 115 127 syl2anc ${⊢}{k}\in ℕ\to {\mathrm{e}}^{\mathrm{log}{A}\left({k}\right)}={A}\left({k}\right)$
129 76 126 128 3eqtrd ${⊢}{k}\in ℕ\to \left(\mathrm{exp}\circ {B}\right)\left({k}\right)={A}\left({k}\right)$
130 129 adantl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left(\mathrm{exp}\circ {B}\right)\left({k}\right)={A}\left({k}\right)$
131 6 59 62 63 130 climeq ${⊢}\top \to \left(\left(\mathrm{exp}\circ {B}\right)⇝{\mathrm{e}}^{{d}}↔{A}⇝{\mathrm{e}}^{{d}}\right)$
132 131 mptru ${⊢}\left(\mathrm{exp}\circ {B}\right)⇝{\mathrm{e}}^{{d}}↔{A}⇝{\mathrm{e}}^{{d}}$
133 53 132 sylib ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to {A}⇝{\mathrm{e}}^{{d}}$
134 breq2 ${⊢}{c}={\mathrm{e}}^{{d}}\to \left({A}⇝{c}↔{A}⇝{\mathrm{e}}^{{d}}\right)$
135 134 rspcev ${⊢}\left({\mathrm{e}}^{{d}}\in {ℝ}^{+}\wedge {A}⇝{\mathrm{e}}^{{d}}\right)\to \exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}⇝{c}$
136 5 133 135 syl2anc ${⊢}\left({d}\in ℝ\wedge {B}⇝{d}\right)\to \exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}⇝{c}$
137 136 rexlimiva ${⊢}\exists {d}\in ℝ\phantom{\rule{.4em}{0ex}}{B}⇝{d}\to \exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}⇝{c}$
138 3 137 ax-mp ${⊢}\exists {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}⇝{c}$