stirlinglem15

Description: The Stirling's formula is proven using a number of local definitions. The main theorem stirling will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem15.1	$⊢ Ⅎ n φ$
	stirlinglem15.2	$⊢ S = (n \in ℕ_{0} ⟼ \sqrt{2 π n} {(\frac{n}{e})}^{n})$
	stirlinglem15.3	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem15.4	$⊢ D = (n \in ℕ ⟼ A (2 n))$
	stirlinglem15.5	$⊢ E = (n \in ℕ ⟼ \sqrt{2 n} {(\frac{n}{e})}^{n})$
	stirlinglem15.6	$⊢ V = (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
	stirlinglem15.7	$⊢ F = (n \in ℕ ⟼ \frac{{A (n)}^{4}}{{D (n)}^{2}})$
	stirlinglem15.8	$⊢ H = (n \in ℕ ⟼ \frac{n^{2}}{n (2 n + 1)})$
	stirlinglem15.9	$⊢ φ \to C \in ℝ^{+}$
	stirlinglem15.10	$⊢ φ \to A ⇝ C$
Assertion	stirlinglem15	$⊢ φ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem15.1	$⊢ Ⅎ n φ$
2		stirlinglem15.2	$⊢ S = (n \in ℕ_{0} ⟼ \sqrt{2 π n} {(\frac{n}{e})}^{n})$
3		stirlinglem15.3	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
4		stirlinglem15.4	$⊢ D = (n \in ℕ ⟼ A (2 n))$
5		stirlinglem15.5	$⊢ E = (n \in ℕ ⟼ \sqrt{2 n} {(\frac{n}{e})}^{n})$
6		stirlinglem15.6	$⊢ V = (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
7		stirlinglem15.7	$⊢ F = (n \in ℕ ⟼ \frac{{A (n)}^{4}}{{D (n)}^{2}})$
8		stirlinglem15.8	$⊢ H = (n \in ℕ ⟼ \frac{n^{2}}{n (2 n + 1)})$
9		stirlinglem15.9	$⊢ φ \to C \in ℝ^{+}$
10		stirlinglem15.10	$⊢ φ \to A ⇝ C$
11		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
12	11	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
13		2cnd	$⊢ (φ \land n \in ℕ) \to 2 \in ℂ$
14		picn	$⊢ π \in ℂ$
15	14	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℂ$
16	13 15	mulcld	$⊢ (φ \land n \in ℕ) \to 2 π \in ℂ$
17		nncn	$⊢ n \in ℕ \to n \in ℂ$
18	17	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
19	16 18	mulcld	$⊢ (φ \land n \in ℕ) \to 2 π n \in ℂ$
20	19	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} \in ℂ$
21		ere	$⊢ e \in ℝ$
22	21	recni	$⊢ e \in ℂ$
23	22	a1i	$⊢ n \in ℕ \to e \in ℂ$
24		epos	$⊢ 0 < e$
25	21 24	gt0ne0ii	$⊢ e \neq 0$
26	25	a1i	$⊢ n \in ℕ \to e \neq 0$
27	17 23 26	divcld	$⊢ n \in ℕ \to \frac{n}{e} \in ℂ$
28	27 11	expcld	$⊢ n \in ℕ \to {(\frac{n}{e})}^{n} \in ℂ$
29	28	adantl	$⊢ (φ \land n \in ℕ) \to {(\frac{n}{e})}^{n} \in ℂ$
30	20 29	mulcld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} {(\frac{n}{e})}^{n} \in ℂ$
31	2	fvmpt2	$⊢ (n \in ℕ_{0} \land \sqrt{2 π n} {(\frac{n}{e})}^{n} \in ℂ) \to S (n) = \sqrt{2 π n} {(\frac{n}{e})}^{n}$
32	12 30 31	syl2anc	$⊢ (φ \land n \in ℕ) \to S (n) = \sqrt{2 π n} {(\frac{n}{e})}^{n}$
33	32	oveq2d	$⊢ (φ \land n \in ℕ) \to \frac{n!}{S (n)} = \frac{n!}{\sqrt{2 π n} {(\frac{n}{e})}^{n}}$
34	15	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \in ℂ$
35		2cnd	$⊢ n \in ℕ \to 2 \in ℂ$
36	35 17	mulcld	$⊢ n \in ℕ \to 2 n \in ℂ$
37	36	sqrtcld	$⊢ n \in ℕ \to \sqrt{2 n} \in ℂ$
38	37	adantl	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} \in ℂ$
39	34 38 29	mulassd	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}$
40		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{{A (n)}^{4}}{{D (n)}^{2}})$
41	7 40	nfcxfr	$⊢ \underline{Ⅎ} n F$
42		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{n^{2}}{n (2 n + 1)})$
43	8 42	nfcxfr	$⊢ \underline{Ⅎ} n H$
44		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1})$
45	6 44	nfcxfr	$⊢ \underline{Ⅎ} n V$
46		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
47		1zzd	$⊢ φ \to 1 \in ℤ$
48		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
49	3 48	nfcxfr	$⊢ \underline{Ⅎ} n A$
50		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ A (2 n))$
51	4 50	nfcxfr	$⊢ \underline{Ⅎ} n D$
52		faccl	$⊢ n \in ℕ_{0} \to n! \in ℕ$
53	11 52	syl	$⊢ n \in ℕ \to n! \in ℕ$
54	53	nnrpd	$⊢ n \in ℕ \to n! \in ℝ^{+}$
55		2rp	$⊢ 2 \in ℝ^{+}$
56	55	a1i	$⊢ n \in ℕ \to 2 \in ℝ^{+}$
57		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
58	56 57	rpmulcld	$⊢ n \in ℕ \to 2 n \in ℝ^{+}$
59	58	rpsqrtcld	$⊢ n \in ℕ \to \sqrt{2 n} \in ℝ^{+}$
60		epr	$⊢ e \in ℝ^{+}$
61	60	a1i	$⊢ n \in ℕ \to e \in ℝ^{+}$
62	57 61	rpdivcld	$⊢ n \in ℕ \to \frac{n}{e} \in ℝ^{+}$
63		nnz	$⊢ n \in ℕ \to n \in ℤ$
64	62 63	rpexpcld	$⊢ n \in ℕ \to {(\frac{n}{e})}^{n} \in ℝ^{+}$
65	59 64	rpmulcld	$⊢ n \in ℕ \to \sqrt{2 n} {(\frac{n}{e})}^{n} \in ℝ^{+}$
66	54 65	rpdivcld	$⊢ n \in ℕ \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℝ^{+}$
67	3 66	fmpti	$⊢ A : ℕ ⟶ ℝ^{+}$
68	67	a1i	$⊢ φ \to A : ℕ ⟶ ℝ^{+}$
69		eqid	$⊢ (n \in ℕ ⟼ {A (n)}^{4}) = (n \in ℕ ⟼ {A (n)}^{4})$
70		eqid	$⊢ (n \in ℕ ⟼ {D (n)}^{2}) = (n \in ℕ ⟼ {D (n)}^{2})$
71	67	a1i	$⊢ n \in ℕ \to A : ℕ ⟶ ℝ^{+}$
72		2nn	$⊢ 2 \in ℕ$
73	72	a1i	$⊢ n \in ℕ \to 2 \in ℕ$
74		id	$⊢ n \in ℕ \to n \in ℕ$
75	73 74	nnmulcld	$⊢ n \in ℕ \to 2 n \in ℕ$
76	71 75	ffvelcdmd	$⊢ n \in ℕ \to A (2 n) \in ℝ^{+}$
77	4	fvmpt2	$⊢ (n \in ℕ \land A (2 n) \in ℝ^{+}) \to D (n) = A (2 n)$
78	76 77	mpdan	$⊢ n \in ℕ \to D (n) = A (2 n)$
79	78 76	eqeltrd	$⊢ n \in ℕ \to D (n) \in ℝ^{+}$
80	79	adantl	$⊢ (φ \land n \in ℕ) \to D (n) \in ℝ^{+}$
81	1 49 51 4 68 7 69 70 80 9 10	stirlinglem8	$⊢ φ \to F ⇝ C^{2}$
82		nnex	$⊢ ℕ \in V$
83	82	mptex	$⊢ (n \in ℕ ⟼ \frac{\frac{2^{4 n} {n!}^{4}}{{2 n!}^{2}}}{2 n + 1}) \in V$
84	6 83	eqeltri	$⊢ V \in V$
85	84	a1i	$⊢ φ \to V \in V$
86		eqid	$⊢ (n \in ℕ ⟼ 1 - (\frac{1}{2 n + 1})) = (n \in ℕ ⟼ 1 - (\frac{1}{2 n + 1}))$
87		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{2 n + 1}) = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
88		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n}) = (n \in ℕ ⟼ \frac{1}{n})$
89	8 86 87 88	stirlinglem1	$⊢ H ⇝ (\frac{1}{2})$
90	89	a1i	$⊢ φ \to H ⇝ (\frac{1}{2})$
91	53	nncnd	$⊢ n \in ℕ \to n! \in ℂ$
92	37 28	mulcld	$⊢ n \in ℕ \to \sqrt{2 n} {(\frac{n}{e})}^{n} \in ℂ$
93	58	sqrtgt0d	$⊢ n \in ℕ \to 0 < \sqrt{2 n}$
94	93	gt0ne0d	$⊢ n \in ℕ \to \sqrt{2 n} \neq 0$
95		nnne0	$⊢ n \in ℕ \to n \neq 0$
96	17 23 95 26	divne0d	$⊢ n \in ℕ \to \frac{n}{e} \neq 0$
97	27 96 63	expne0d	$⊢ n \in ℕ \to {(\frac{n}{e})}^{n} \neq 0$
98	37 28 94 97	mulne0d	$⊢ n \in ℕ \to \sqrt{2 n} {(\frac{n}{e})}^{n} \neq 0$
99	91 92 98	divcld	$⊢ n \in ℕ \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ$
100	3	fvmpt2	$⊢ (n \in ℕ \land \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ) \to A (n) = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}$
101	99 100	mpdan	$⊢ n \in ℕ \to A (n) = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}$
102	101 99	eqeltrd	$⊢ n \in ℕ \to A (n) \in ℂ$
103		4nn0	$⊢ 4 \in ℕ_{0}$
104	103	a1i	$⊢ n \in ℕ \to 4 \in ℕ_{0}$
105	102 104	expcld	$⊢ n \in ℕ \to {A (n)}^{4} \in ℂ$
106	79	rpcnd	$⊢ n \in ℕ \to D (n) \in ℂ$
107	106	sqcld	$⊢ n \in ℕ \to {D (n)}^{2} \in ℂ$
108	79	rpne0d	$⊢ n \in ℕ \to D (n) \neq 0$
109		2z	$⊢ 2 \in ℤ$
110	109	a1i	$⊢ n \in ℕ \to 2 \in ℤ$
111	106 108 110	expne0d	$⊢ n \in ℕ \to {D (n)}^{2} \neq 0$
112	105 107 111	divcld	$⊢ n \in ℕ \to \frac{{A (n)}^{4}}{{D (n)}^{2}} \in ℂ$
113	7	fvmpt2	$⊢ (n \in ℕ \land \frac{{A (n)}^{4}}{{D (n)}^{2}} \in ℂ) \to F (n) = \frac{{A (n)}^{4}}{{D (n)}^{2}}$
114	112 113	mpdan	$⊢ n \in ℕ \to F (n) = \frac{{A (n)}^{4}}{{D (n)}^{2}}$
115	114 112	eqeltrd	$⊢ n \in ℕ \to F (n) \in ℂ$
116	115	adantl	$⊢ (φ \land n \in ℕ) \to F (n) \in ℂ$
117	17	sqcld	$⊢ n \in ℕ \to n^{2} \in ℂ$
118		1cnd	$⊢ n \in ℕ \to 1 \in ℂ$
119	36 118	addcld	$⊢ n \in ℕ \to 2 n + 1 \in ℂ$
120	17 119	mulcld	$⊢ n \in ℕ \to n (2 n + 1) \in ℂ$
121	75	nnred	$⊢ n \in ℕ \to 2 n \in ℝ$
122		1red	$⊢ n \in ℕ \to 1 \in ℝ$
123	75	nngt0d	$⊢ n \in ℕ \to 0 < 2 n$
124		0lt1	$⊢ 0 < 1$
125	124	a1i	$⊢ n \in ℕ \to 0 < 1$
126	121 122 123 125	addgt0d	$⊢ n \in ℕ \to 0 < 2 n + 1$
127	126	gt0ne0d	$⊢ n \in ℕ \to 2 n + 1 \neq 0$
128	17 119 95 127	mulne0d	$⊢ n \in ℕ \to n (2 n + 1) \neq 0$
129	117 120 128	divcld	$⊢ n \in ℕ \to \frac{n^{2}}{n (2 n + 1)} \in ℂ$
130	8	fvmpt2	$⊢ (n \in ℕ \land \frac{n^{2}}{n (2 n + 1)} \in ℂ) \to H (n) = \frac{n^{2}}{n (2 n + 1)}$
131	129 130	mpdan	$⊢ n \in ℕ \to H (n) = \frac{n^{2}}{n (2 n + 1)}$
132	131 129	eqeltrd	$⊢ n \in ℕ \to H (n) \in ℂ$
133	132	adantl	$⊢ (φ \land n \in ℕ) \to H (n) \in ℂ$
134	112 129	mulcld	$⊢ n \in ℕ \to (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)}) \in ℂ$
135	3 4 5 6	stirlinglem3	$⊢ V = (n \in ℕ ⟼ (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)}))$
136	135	fvmpt2	$⊢ (n \in ℕ \land (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)}) \in ℂ) \to V (n) = (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)})$
137	134 136	mpdan	$⊢ n \in ℕ \to V (n) = (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)})$
138	114 131	oveq12d	$⊢ n \in ℕ \to F (n) H (n) = (\frac{{A (n)}^{4}}{{D (n)}^{2}}) (\frac{n^{2}}{n (2 n + 1)})$
139	137 138	eqtr4d	$⊢ n \in ℕ \to V (n) = F (n) H (n)$
140	139	adantl	$⊢ (φ \land n \in ℕ) \to V (n) = F (n) H (n)$
141	1 41 43 45 46 47 81 85 90 116 133 140	climmulf	$⊢ φ \to V ⇝ C^{2} (\frac{1}{2})$
142	6	wallispi2	$⊢ V ⇝ (\frac{π}{2})$
143		climuni	$⊢ (V ⇝ C^{2} (\frac{1}{2}) \land V ⇝ (\frac{π}{2})) \to C^{2} (\frac{1}{2}) = \frac{π}{2}$
144	141 142 143	sylancl	$⊢ φ \to C^{2} (\frac{1}{2}) = \frac{π}{2}$
145	144	oveq1d	$⊢ φ \to \frac{C^{2} (\frac{1}{2})}{\frac{1}{2}} = \frac{\frac{π}{2}}{\frac{1}{2}}$
146	9	rpcnd	$⊢ φ \to C \in ℂ$
147	146	sqcld	$⊢ φ \to C^{2} \in ℂ$
148		1cnd	$⊢ φ \to 1 \in ℂ$
149	148	halfcld	$⊢ φ \to \frac{1}{2} \in ℂ$
150		2cnd	$⊢ φ \to 2 \in ℂ$
151		2pos	$⊢ 0 < 2$
152	151	a1i	$⊢ φ \to 0 < 2$
153	152	gt0ne0d	$⊢ φ \to 2 \neq 0$
154	150 153	recne0d	$⊢ φ \to \frac{1}{2} \neq 0$
155	147 149 154	divcan4d	$⊢ φ \to \frac{C^{2} (\frac{1}{2})}{\frac{1}{2}} = C^{2}$
156	14	a1i	$⊢ φ \to π \in ℂ$
157	124	a1i	$⊢ φ \to 0 < 1$
158	157	gt0ne0d	$⊢ φ \to 1 \neq 0$
159	156 148 150 158 153	divcan7d	$⊢ φ \to \frac{\frac{π}{2}}{\frac{1}{2}} = \frac{π}{1}$
160	156	div1d	$⊢ φ \to \frac{π}{1} = π$
161	159 160	eqtrd	$⊢ φ \to \frac{\frac{π}{2}}{\frac{1}{2}} = π$
162	145 155 161	3eqtr3d	$⊢ φ \to C^{2} = π$
163	162	fveq2d	$⊢ φ \to \sqrt{C^{2}} = \sqrt{π}$
164	9	rprege0d	$⊢ φ \to (C \in ℝ \land 0 \leq C)$
165		sqrtsq	$⊢ (C \in ℝ \land 0 \leq C) \to \sqrt{C^{2}} = C$
166	164 165	syl	$⊢ φ \to \sqrt{C^{2}} = C$
167	163 166	eqtr3d	$⊢ φ \to \sqrt{π} = C$
168	167	adantr	$⊢ (φ \land n \in ℕ) \to \sqrt{π} = C$
169	168	oveq1d	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n} = C \sqrt{2 n} {(\frac{n}{e})}^{n}$
170	146	adantr	$⊢ (φ \land n \in ℕ) \to C \in ℂ$
171	92	adantl	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} {(\frac{n}{e})}^{n} \in ℂ$
172	170 171	mulcomd	$⊢ (φ \land n \in ℕ) \to C \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 n} {(\frac{n}{e})}^{n} C$
173	39 169 172	3eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 n} {(\frac{n}{e})}^{n} C$
174	173	oveq2d	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}} = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n} C}$
175		2re	$⊢ 2 \in ℝ$
176	175	a1i	$⊢ (φ \land n \in ℕ) \to 2 \in ℝ$
177		pire	$⊢ π \in ℝ$
178	177	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
179	176 178	remulcld	$⊢ (φ \land n \in ℕ) \to 2 π \in ℝ$
180		0le2	$⊢ 0 \leq 2$
181	180	a1i	$⊢ (φ \land n \in ℕ) \to 0 \leq 2$
182		pige0	$⊢ 0 \leq π$
183	182	a1i	$⊢ (φ \land n \in ℕ) \to 0 \leq π$
184	176 178 181 183	mulge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq 2 π$
185	12	nn0red	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
186	12	nn0ge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq n$
187	179 184 185 186	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} = \sqrt{2 π} \sqrt{n}$
188	176 181 178 183	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} = \sqrt{2} \sqrt{π}$
189	188	oveq1d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} \sqrt{n} = \sqrt{2} \sqrt{π} \sqrt{n}$
190	13	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \in ℂ$
191	18	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{n} \in ℂ$
192	190 34 191	mulassd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{2} \sqrt{π} \sqrt{n}$
193	190 34 191	mul12d	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{π} \sqrt{2} \sqrt{n}$
194	176 181 185 186	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} = \sqrt{2} \sqrt{n}$
195	194	eqcomd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{n} = \sqrt{2 n}$
196	195	oveq2d	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \sqrt{2} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
197	193 196	eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
198	189 192 197	3eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
199	187 198	eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} = \sqrt{π} \sqrt{2 n}$
200	199	oveq1d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} {(\frac{n}{e})}^{n} = \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}$
201	200	oveq2d	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{2 π n} {(\frac{n}{e})}^{n}} = \frac{n!}{\sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}}$
202	91	adantl	$⊢ (φ \land n \in ℕ) \to n! \in ℂ$
203	94	adantl	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} \neq 0$
204	22	a1i	$⊢ (φ \land n \in ℕ) \to e \in ℂ$
205	25	a1i	$⊢ (φ \land n \in ℕ) \to e \neq 0$
206	18 204 205	divcld	$⊢ (φ \land n \in ℕ) \to \frac{n}{e} \in ℂ$
207	95	adantl	$⊢ (φ \land n \in ℕ) \to n \neq 0$
208	18 204 207 205	divne0d	$⊢ (φ \land n \in ℕ) \to \frac{n}{e} \neq 0$
209	63	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℤ$
210	206 208 209	expne0d	$⊢ (φ \land n \in ℕ) \to {(\frac{n}{e})}^{n} \neq 0$
211	38 29 203 210	mulne0d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} {(\frac{n}{e})}^{n} \neq 0$
212	9	rpne0d	$⊢ φ \to C \neq 0$
213	212	adantr	$⊢ (φ \land n \in ℕ) \to C \neq 0$
214	202 171 170 211 213	divdiv1d	$⊢ (φ \land n \in ℕ) \to \frac{\frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}}{C} = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n} C}$
215	174 201 214	3eqtr4d	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{2 π n} {(\frac{n}{e})}^{n}} = \frac{\frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}}{C}$
216	99	ancli	$⊢ n \in ℕ \to (n \in ℕ \land \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ)$
217	216	adantl	$⊢ (φ \land n \in ℕ) \to (n \in ℕ \land \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ)$
218	217 100	syl	$⊢ (φ \land n \in ℕ) \to A (n) = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}$
219	218	eqcomd	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = A (n)$
220	219	oveq1d	$⊢ (φ \land n \in ℕ) \to \frac{\frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}}{C} = \frac{A (n)}{C}$
221	33 215 220	3eqtrd	$⊢ (φ \land n \in ℕ) \to \frac{n!}{S (n)} = \frac{A (n)}{C}$
222	1 221	mpteq2da	$⊢ φ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) = (n \in ℕ ⟼ \frac{A (n)}{C})$
223	102	adantl	$⊢ (φ \land n \in ℕ) \to A (n) \in ℂ$
224	223 170 213	divrec2d	$⊢ (φ \land n \in ℕ) \to \frac{A (n)}{C} = (\frac{1}{C}) A (n)$
225	1 224	mpteq2da	$⊢ φ \to (n \in ℕ ⟼ \frac{A (n)}{C}) = (n \in ℕ ⟼ (\frac{1}{C}) A (n))$
226	146 212	reccld	$⊢ φ \to \frac{1}{C} \in ℂ$
227	82	mptex	$⊢ (n \in ℕ ⟼ (\frac{1}{C}) A (n)) \in V$
228	227	a1i	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) \in V$
229	3	a1i	$⊢ k \in ℕ \to A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
230		simpr	$⊢ (k \in ℕ \land n = k) \to n = k$
231	230	fveq2d	$⊢ (k \in ℕ \land n = k) \to n! = k!$
232	230	oveq2d	$⊢ (k \in ℕ \land n = k) \to 2 n = 2 k$
233	232	fveq2d	$⊢ (k \in ℕ \land n = k) \to \sqrt{2 n} = \sqrt{2 k}$
234	230	oveq1d	$⊢ (k \in ℕ \land n = k) \to \frac{n}{e} = \frac{k}{e}$
235	234 230	oveq12d	$⊢ (k \in ℕ \land n = k) \to {(\frac{n}{e})}^{n} = {(\frac{k}{e})}^{k}$
236	233 235	oveq12d	$⊢ (k \in ℕ \land n = k) \to \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 k} {(\frac{k}{e})}^{k}$
237	231 236	oveq12d	$⊢ (k \in ℕ \land n = k) \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}}$
238		id	$⊢ k \in ℕ \to k \in ℕ$
239		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
240		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
241		nncn	$⊢ k! \in ℕ \to k! \in ℂ$
242	239 240 241	3syl	$⊢ k \in ℕ \to k! \in ℂ$
243		2cnd	$⊢ k \in ℕ \to 2 \in ℂ$
244		nncn	$⊢ k \in ℕ \to k \in ℂ$
245	243 244	mulcld	$⊢ k \in ℕ \to 2 k \in ℂ$
246	245	sqrtcld	$⊢ k \in ℕ \to \sqrt{2 k} \in ℂ$
247	22	a1i	$⊢ k \in ℕ \to e \in ℂ$
248	25	a1i	$⊢ k \in ℕ \to e \neq 0$
249	244 247 248	divcld	$⊢ k \in ℕ \to \frac{k}{e} \in ℂ$
250	249 239	expcld	$⊢ k \in ℕ \to {(\frac{k}{e})}^{k} \in ℂ$
251	246 250	mulcld	$⊢ k \in ℕ \to \sqrt{2 k} {(\frac{k}{e})}^{k} \in ℂ$
252	55	a1i	$⊢ k \in ℕ \to 2 \in ℝ^{+}$
253		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
254	252 253	rpmulcld	$⊢ k \in ℕ \to 2 k \in ℝ^{+}$
255	254	sqrtgt0d	$⊢ k \in ℕ \to 0 < \sqrt{2 k}$
256	255	gt0ne0d	$⊢ k \in ℕ \to \sqrt{2 k} \neq 0$
257		nnne0	$⊢ k \in ℕ \to k \neq 0$
258	244 247 257 248	divne0d	$⊢ k \in ℕ \to \frac{k}{e} \neq 0$
259		nnz	$⊢ k \in ℕ \to k \in ℤ$
260	249 258 259	expne0d	$⊢ k \in ℕ \to {(\frac{k}{e})}^{k} \neq 0$
261	246 250 256 260	mulne0d	$⊢ k \in ℕ \to \sqrt{2 k} {(\frac{k}{e})}^{k} \neq 0$
262	242 251 261	divcld	$⊢ k \in ℕ \to \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}} \in ℂ$
263	229 237 238 262	fvmptd	$⊢ k \in ℕ \to A (k) = \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}}$
264	263 262	eqeltrd	$⊢ k \in ℕ \to A (k) \in ℂ$
265	264	adantl	$⊢ (φ \land k \in ℕ) \to A (k) \in ℂ$
266		nfcv	$⊢ \underline{Ⅎ} k (\frac{1}{C}) A (n)$
267		nfcv	$⊢ \underline{Ⅎ} n 1$
268		nfcv	$⊢ \underline{Ⅎ} n \div$
269		nfcv	$⊢ \underline{Ⅎ} n C$
270	267 268 269	nfov	$⊢ \underline{Ⅎ} n (\frac{1}{C})$
271		nfcv	$⊢ \underline{Ⅎ} n \times$
272		nfcv	$⊢ \underline{Ⅎ} n k$
273	49 272	nffv	$⊢ \underline{Ⅎ} n A (k)$
274	270 271 273	nfov	$⊢ \underline{Ⅎ} n (\frac{1}{C}) A (k)$
275		fveq2	$⊢ n = k \to A (n) = A (k)$
276	275	oveq2d	$⊢ n = k \to (\frac{1}{C}) A (n) = (\frac{1}{C}) A (k)$
277	266 274 276	cbvmpt	$⊢ (n \in ℕ ⟼ (\frac{1}{C}) A (n)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
278	277	a1i	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
279	278	fveq1d	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) (k) = (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k)$
280		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
281	146	adantr	$⊢ (φ \land k \in ℕ) \to C \in ℂ$
282	212	adantr	$⊢ (φ \land k \in ℕ) \to C \neq 0$
283	281 282	reccld	$⊢ (φ \land k \in ℕ) \to \frac{1}{C} \in ℂ$
284	283 265	mulcld	$⊢ (φ \land k \in ℕ) \to (\frac{1}{C}) A (k) \in ℂ$
285		eqid	$⊢ (k \in ℕ ⟼ (\frac{1}{C}) A (k)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
286	285	fvmpt2	$⊢ (k \in ℕ \land (\frac{1}{C}) A (k) \in ℂ) \to (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k) = (\frac{1}{C}) A (k)$
287	280 284 286	syl2anc	$⊢ (φ \land k \in ℕ) \to (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k) = (\frac{1}{C}) A (k)$
288	279 287	eqtrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) (k) = (\frac{1}{C}) A (k)$
289	46 47 10 226 228 265 288	climmulc2	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) ⇝ (\frac{1}{C}) C$
290	146 212	recid2d	$⊢ φ \to (\frac{1}{C}) C = 1$
291	289 290	breqtrd	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) ⇝ 1$
292	225 291	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ \frac{A (n)}{C}) ⇝ 1$
293	222 292	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1$

Metamath Proof Explorer

Theorem stirlinglem15

Proof