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	ffvelrnd	$⊢ 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		0re	$⊢ 0 \in ℝ$
183		pipos	$⊢ 0 < π$
184	182 177 183	ltleii	$⊢ 0 \leq π$
185	184	a1i	$⊢ (φ \land n \in ℕ) \to 0 \leq π$
186	176 178 181 185	mulge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq 2 π$
187	12	nn0red	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
188	12	nn0ge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq n$
189	179 186 187 188	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} = \sqrt{2 π} \sqrt{n}$
190	176 181 178 185	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} = \sqrt{2} \sqrt{π}$
191	190	oveq1d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} \sqrt{n} = \sqrt{2} \sqrt{π} \sqrt{n}$
192	13	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \in ℂ$
193	18	sqrtcld	$⊢ (φ \land n \in ℕ) \to \sqrt{n} \in ℂ$
194	192 34 193	mulassd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{2} \sqrt{π} \sqrt{n}$
195	192 34 193	mul12d	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{π} \sqrt{2} \sqrt{n}$
196	176 181 187 188	sqrtmuld	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} = \sqrt{2} \sqrt{n}$
197	196	eqcomd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{n} = \sqrt{2 n}$
198	197	oveq2d	$⊢ (φ \land n \in ℕ) \to \sqrt{π} \sqrt{2} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
199	195 198	eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2} \sqrt{π} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
200	191 194 199	3eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π} \sqrt{n} = \sqrt{π} \sqrt{2 n}$
201	189 200	eqtrd	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} = \sqrt{π} \sqrt{2 n}$
202	201	oveq1d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 π n} {(\frac{n}{e})}^{n} = \sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}$
203	202	oveq2d	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{2 π n} {(\frac{n}{e})}^{n}} = \frac{n!}{\sqrt{π} \sqrt{2 n} {(\frac{n}{e})}^{n}}$
204	91	adantl	$⊢ (φ \land n \in ℕ) \to n! \in ℂ$
205	94	adantl	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} \neq 0$
206	22	a1i	$⊢ (φ \land n \in ℕ) \to e \in ℂ$
207	25	a1i	$⊢ (φ \land n \in ℕ) \to e \neq 0$
208	18 206 207	divcld	$⊢ (φ \land n \in ℕ) \to \frac{n}{e} \in ℂ$
209	95	adantl	$⊢ (φ \land n \in ℕ) \to n \neq 0$
210	18 206 209 207	divne0d	$⊢ (φ \land n \in ℕ) \to \frac{n}{e} \neq 0$
211	63	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℤ$
212	208 210 211	expne0d	$⊢ (φ \land n \in ℕ) \to {(\frac{n}{e})}^{n} \neq 0$
213	38 29 205 212	mulne0d	$⊢ (φ \land n \in ℕ) \to \sqrt{2 n} {(\frac{n}{e})}^{n} \neq 0$
214	9	rpne0d	$⊢ φ \to C \neq 0$
215	214	adantr	$⊢ (φ \land n \in ℕ) \to C \neq 0$
216	204 171 170 213 215	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}$
217	174 203 216	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}$
218	99	ancli	$⊢ n \in ℕ \to (n \in ℕ \land \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ)$
219	218	adantl	$⊢ (φ \land n \in ℕ) \to (n \in ℕ \land \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} \in ℂ)$
220	219 100	syl	$⊢ (φ \land n \in ℕ) \to A (n) = \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}$
221	220	eqcomd	$⊢ (φ \land n \in ℕ) \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = A (n)$
222	221	oveq1d	$⊢ (φ \land n \in ℕ) \to \frac{\frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}}{C} = \frac{A (n)}{C}$
223	33 217 222	3eqtrd	$⊢ (φ \land n \in ℕ) \to \frac{n!}{S (n)} = \frac{A (n)}{C}$
224	1 223	mpteq2da	$⊢ φ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) = (n \in ℕ ⟼ \frac{A (n)}{C})$
225	102	adantl	$⊢ (φ \land n \in ℕ) \to A (n) \in ℂ$
226	225 170 215	divrec2d	$⊢ (φ \land n \in ℕ) \to \frac{A (n)}{C} = (\frac{1}{C}) A (n)$
227	1 226	mpteq2da	$⊢ φ \to (n \in ℕ ⟼ \frac{A (n)}{C}) = (n \in ℕ ⟼ (\frac{1}{C}) A (n))$
228	146 214	reccld	$⊢ φ \to \frac{1}{C} \in ℂ$
229	82	mptex	$⊢ (n \in ℕ ⟼ (\frac{1}{C}) A (n)) \in V$
230	229	a1i	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) \in V$
231	3	a1i	$⊢ k \in ℕ \to A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
232		simpr	$⊢ (k \in ℕ \land n = k) \to n = k$
233	232	fveq2d	$⊢ (k \in ℕ \land n = k) \to n! = k!$
234	232	oveq2d	$⊢ (k \in ℕ \land n = k) \to 2 n = 2 k$
235	234	fveq2d	$⊢ (k \in ℕ \land n = k) \to \sqrt{2 n} = \sqrt{2 k}$
236	232	oveq1d	$⊢ (k \in ℕ \land n = k) \to \frac{n}{e} = \frac{k}{e}$
237	236 232	oveq12d	$⊢ (k \in ℕ \land n = k) \to {(\frac{n}{e})}^{n} = {(\frac{k}{e})}^{k}$
238	235 237	oveq12d	$⊢ (k \in ℕ \land n = k) \to \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 k} {(\frac{k}{e})}^{k}$
239	233 238	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}}$
240		id	$⊢ k \in ℕ \to k \in ℕ$
241		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
242		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
243		nncn	$⊢ k! \in ℕ \to k! \in ℂ$
244	241 242 243	3syl	$⊢ k \in ℕ \to k! \in ℂ$
245		2cnd	$⊢ k \in ℕ \to 2 \in ℂ$
246		nncn	$⊢ k \in ℕ \to k \in ℂ$
247	245 246	mulcld	$⊢ k \in ℕ \to 2 k \in ℂ$
248	247	sqrtcld	$⊢ k \in ℕ \to \sqrt{2 k} \in ℂ$
249	22	a1i	$⊢ k \in ℕ \to e \in ℂ$
250	25	a1i	$⊢ k \in ℕ \to e \neq 0$
251	246 249 250	divcld	$⊢ k \in ℕ \to \frac{k}{e} \in ℂ$
252	251 241	expcld	$⊢ k \in ℕ \to {(\frac{k}{e})}^{k} \in ℂ$
253	248 252	mulcld	$⊢ k \in ℕ \to \sqrt{2 k} {(\frac{k}{e})}^{k} \in ℂ$
254	55	a1i	$⊢ k \in ℕ \to 2 \in ℝ^{+}$
255		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
256	254 255	rpmulcld	$⊢ k \in ℕ \to 2 k \in ℝ^{+}$
257	256	sqrtgt0d	$⊢ k \in ℕ \to 0 < \sqrt{2 k}$
258	257	gt0ne0d	$⊢ k \in ℕ \to \sqrt{2 k} \neq 0$
259		nnne0	$⊢ k \in ℕ \to k \neq 0$
260	246 249 259 250	divne0d	$⊢ k \in ℕ \to \frac{k}{e} \neq 0$
261		nnz	$⊢ k \in ℕ \to k \in ℤ$
262	251 260 261	expne0d	$⊢ k \in ℕ \to {(\frac{k}{e})}^{k} \neq 0$
263	248 252 258 262	mulne0d	$⊢ k \in ℕ \to \sqrt{2 k} {(\frac{k}{e})}^{k} \neq 0$
264	244 253 263	divcld	$⊢ k \in ℕ \to \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}} \in ℂ$
265	231 239 240 264	fvmptd	$⊢ k \in ℕ \to A (k) = \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}}$
266	265 264	eqeltrd	$⊢ k \in ℕ \to A (k) \in ℂ$
267	266	adantl	$⊢ (φ \land k \in ℕ) \to A (k) \in ℂ$
268		nfcv	$⊢ \underline{Ⅎ} k (\frac{1}{C}) A (n)$
269		nfcv	$⊢ \underline{Ⅎ} n 1$
270		nfcv	$⊢ \underline{Ⅎ} n \div$
271		nfcv	$⊢ \underline{Ⅎ} n C$
272	269 270 271	nfov	$⊢ \underline{Ⅎ} n (\frac{1}{C})$
273		nfcv	$⊢ \underline{Ⅎ} n \times$
274		nfcv	$⊢ \underline{Ⅎ} n k$
275	49 274	nffv	$⊢ \underline{Ⅎ} n A (k)$
276	272 273 275	nfov	$⊢ \underline{Ⅎ} n (\frac{1}{C}) A (k)$
277		fveq2	$⊢ n = k \to A (n) = A (k)$
278	277	oveq2d	$⊢ n = k \to (\frac{1}{C}) A (n) = (\frac{1}{C}) A (k)$
279	268 276 278	cbvmpt	$⊢ (n \in ℕ ⟼ (\frac{1}{C}) A (n)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
280	279	a1i	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
281	280	fveq1d	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) (k) = (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k)$
282		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
283	146	adantr	$⊢ (φ \land k \in ℕ) \to C \in ℂ$
284	214	adantr	$⊢ (φ \land k \in ℕ) \to C \neq 0$
285	283 284	reccld	$⊢ (φ \land k \in ℕ) \to \frac{1}{C} \in ℂ$
286	285 267	mulcld	$⊢ (φ \land k \in ℕ) \to (\frac{1}{C}) A (k) \in ℂ$
287		eqid	$⊢ (k \in ℕ ⟼ (\frac{1}{C}) A (k)) = (k \in ℕ ⟼ (\frac{1}{C}) A (k))$
288	287	fvmpt2	$⊢ (k \in ℕ \land (\frac{1}{C}) A (k) \in ℂ) \to (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k) = (\frac{1}{C}) A (k)$
289	282 286 288	syl2anc	$⊢ (φ \land k \in ℕ) \to (k \in ℕ ⟼ (\frac{1}{C}) A (k)) (k) = (\frac{1}{C}) A (k)$
290	281 289	eqtrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) (k) = (\frac{1}{C}) A (k)$
291	46 47 10 228 230 267 290	climmulc2	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) ⇝ (\frac{1}{C}) C$
292	146 214	recid2d	$⊢ φ \to (\frac{1}{C}) C = 1$
293	291 292	breqtrd	$⊢ φ \to (n \in ℕ ⟼ (\frac{1}{C}) A (n)) ⇝ 1$
294	227 293	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ \frac{A (n)}{C}) ⇝ 1$
295	224 294	eqbrtrd	$⊢ φ \to (n \in ℕ ⟼ \frac{n!}{S (n)}) ⇝ 1$

Metamath Proof Explorer

Theorem stirlinglem15

Proof