Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem3 Structured version   Unicode version

Theorem stirlinglem3 27801
 Description: Long but simple algebraic transformations are applied to show that , the Wallis formula for π , can be expressed in terms of , the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the , in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem3.1
stirlinglem3.2
stirlinglem3.3
stirlinglem3.4
Assertion
Ref Expression
stirlinglem3

Proof of Theorem stirlinglem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 stirlinglem3.4 . 2
2 nnnn0 10228 . . . . . . . . . . . . 13
3 faccl 11576 . . . . . . . . . . . . 13
4 nncn 10008 . . . . . . . . . . . . 13
52, 3, 43syl 19 . . . . . . . . . . . 12
6 2cn 10070 . . . . . . . . . . . . . . . 16
76a1i 11 . . . . . . . . . . . . . . 15
8 nncn 10008 . . . . . . . . . . . . . . 15
97, 8mulcld 9108 . . . . . . . . . . . . . 14
109sqrcld 12239 . . . . . . . . . . . . 13
11 ere 12691 . . . . . . . . . . . . . . . . 17
1211recni 9102 . . . . . . . . . . . . . . . 16
1312a1i 11 . . . . . . . . . . . . . . 15
14 epos 12806 . . . . . . . . . . . . . . . . 17
1511, 14gt0ne0ii 9563 . . . . . . . . . . . . . . . 16
1615a1i 11 . . . . . . . . . . . . . . 15
178, 13, 16divcld 9790 . . . . . . . . . . . . . 14
1817, 2expcld 11523 . . . . . . . . . . . . 13
1910, 18mulcld 9108 . . . . . . . . . . . 12
20 2rp 10617 . . . . . . . . . . . . . . . . 17
2120a1i 11 . . . . . . . . . . . . . . . 16
22 nnrp 10621 . . . . . . . . . . . . . . . 16
2321, 22rpmulcld 10664 . . . . . . . . . . . . . . 15
2423sqrgt0d 12215 . . . . . . . . . . . . . 14
2524gt0ne0d 9591 . . . . . . . . . . . . 13
26 nnne0 10032 . . . . . . . . . . . . . . 15
278, 13, 26, 16divne0d 9806 . . . . . . . . . . . . . 14
28 nnz 10303 . . . . . . . . . . . . . 14
2917, 27, 28expne0d 11529 . . . . . . . . . . . . 13
3010, 18, 25, 29mulne0d 9674 . . . . . . . . . . . 12
315, 19, 30divcld 9790 . . . . . . . . . . 11
32 stirlinglem3.1 . . . . . . . . . . . 12
3332fvmpt2 5812 . . . . . . . . . . 11
3431, 33mpdan 650 . . . . . . . . . 10
3534oveq1d 6096 . . . . . . . . 9
36 stirlinglem3.3 . . . . . . . . . . . 12
3736fvmpt2 5812 . . . . . . . . . . 11
3819, 37mpdan 650 . . . . . . . . . 10
3938oveq1d 6096 . . . . . . . . 9
4035, 39oveq12d 6099 . . . . . . . 8
41 4nn0 10240 . . . . . . . . . . 11
4241a1i 11 . . . . . . . . . 10
435, 19, 30, 42expdivd 11537 . . . . . . . . 9
4443oveq1d 6096 . . . . . . . 8
455, 42expcld 11523 . . . . . . . . 9
4619, 42expcld 11523 . . . . . . . . 9
4742nn0zd 10373 . . . . . . . . . 10
4819, 30, 47expne0d 11529 . . . . . . . . 9
4945, 46, 48divcan1d 9791 . . . . . . . 8
5040, 44, 493eqtrd 2472 . . . . . . 7
5150eqcomd 2441 . . . . . 6
5251oveq2d 6097 . . . . 5
53 2nn0 10238 . . . . . . . . . . . . 13
5453a1i 11 . . . . . . . . . . . 12
5554, 2nn0mulcld 10279 . . . . . . . . . . 11
56 faccl 11576 . . . . . . . . . . 11
57 nncn 10008 . . . . . . . . . . 11
5855, 56, 573syl 19 . . . . . . . . . 10
5958sqcld 11521 . . . . . . . . 9
607, 9mulcld 9108 . . . . . . . . . . . 12
6160sqrcld 12239 . . . . . . . . . . 11
629, 13, 16divcld 9790 . . . . . . . . . . . 12
6362, 55expcld 11523 . . . . . . . . . . 11
6461, 63mulcld 9108 . . . . . . . . . 10
6564sqcld 11521 . . . . . . . . 9
6621, 23rpmulcld 10664 . . . . . . . . . . . . 13
6766sqrgt0d 12215 . . . . . . . . . . . 12
6867gt0ne0d 9591 . . . . . . . . . . 11
6921rpne0d 10653 . . . . . . . . . . . . . 14
707, 8, 69, 26mulne0d 9674 . . . . . . . . . . . . 13
719, 13, 70, 16divne0d 9806 . . . . . . . . . . . 12
72 2z 10312 . . . . . . . . . . . . . 14
7372a1i 11 . . . . . . . . . . . . 13
7473, 28zmulcld 10381 . . . . . . . . . . . 12
7562, 71, 74expne0d 11529 . . . . . . . . . . 11
7661, 63, 68, 75mulne0d 9674 . . . . . . . . . 10
7764, 76, 73expne0d 11529 . . . . . . . . 9
7859, 65, 77divcan1d 9791 . . . . . . . 8
7958, 64, 76, 54expdivd 11537 . . . . . . . . . 10
8079eqcomd 2441 . . . . . . . . 9
8180oveq1d 6096 . . . . . . . 8
8278, 81eqtr3d 2470 . . . . . . 7
83 fveq2 5728 . . . . . . . . . . . . . . 15
84 oveq2 6089 . . . . . . . . . . . . . . . . 17
8584fveq2d 5732 . . . . . . . . . . . . . . . 16
86 oveq1 6088 . . . . . . . . . . . . . . . . 17
87 id 20 . . . . . . . . . . . . . . . . 17
8886, 87oveq12d 6099 . . . . . . . . . . . . . . . 16
8985, 88oveq12d 6099 . . . . . . . . . . . . . . 15
9083, 89oveq12d 6099 . . . . . . . . . . . . . 14
9190cbvmptv 4300 . . . . . . . . . . . . 13
9232, 91eqtri 2456 . . . . . . . . . . . 12
9392a1i 11 . . . . . . . . . . 11
94 fveq2 5728 . . . . . . . . . . . . 13
95 oveq2 6089 . . . . . . . . . . . . . . 15
9695fveq2d 5732 . . . . . . . . . . . . . 14
97 oveq1 6088 . . . . . . . . . . . . . . 15
98 id 20 . . . . . . . . . . . . . . 15
9997, 98oveq12d 6099 . . . . . . . . . . . . . 14
10096, 99oveq12d 6099 . . . . . . . . . . . . 13
10194, 100oveq12d 6099 . . . . . . . . . . . 12
102101adantl 453 . . . . . . . . . . 11
103 2nn 10133 . . . . . . . . . . . . 13
104103a1i 11 . . . . . . . . . . . 12
105 id 20 . . . . . . . . . . . 12
106104, 105nnmulcld 10047 . . . . . . . . . . 11
10758, 64, 76divcld 9790 . . . . . . . . . . 11
10893, 102, 106, 107fvmptd 5810 . . . . . . . . . 10
109108oveq1d 6096 . . . . . . . . 9
110109eqcomd 2441 . . . . . . . 8
111110oveq1d 6096 . . . . . . 7
112 eqidd 2437 . . . . . . . . . . 11
113100adantl 453 . . . . . . . . . . 11
114112, 113, 106, 64fvmptd 5810 . . . . . . . . . 10
115114oveq1d 6096 . . . . . . . . 9
116115eqcomd 2441 . . . . . . . 8
117116oveq2d 6097 . . . . . . 7
11882, 111, 1173eqtrd 2472 . . . . . 6
11989cbvmptv 4300 . . . . . . . . . . 11
120119a1i 11 . . . . . . . . . 10
121120fveq1d 5730 . . . . . . . . 9
122121eqcomd 2441 . . . . . . . 8
123122oveq1d 6096 . . . . . . 7
124123oveq2d 6097 . . . . . 6
125108, 107eqeltrd 2510 . . . . . . . . . 10
126 stirlinglem3.2 . . . . . . . . . . 11
127126fvmpt2 5812 . . . . . . . . . 10
128125, 127mpdan 650 . . . . . . . . 9
129128eqcomd 2441 . . . . . . . 8
130129oveq1d 6096 . . . . . . 7
13136a1i 11 . . . . . . . . . 10
132131fveq1d 5730 . . . . . . . . 9
133132eqcomd 2441 . . . . . . . 8
134133oveq1d 6096 . . . . . . 7
135130, 134oveq12d 6099 . . . . . 6
136118, 124, 1353eqtrd 2472 . . . . 5
13752, 136oveq12d 6099 . . . 4
138137oveq1d 6096 . . 3
139138mpteq2ia 4291 . 2
14042, 2nn0mulcld 10279 . . . . . . . 8
1417, 140expcld 11523 . . . . . . 7
14250, 45eqeltrd 2510 . . . . . . 7
143141, 142mulcomd 9109 . . . . . 6
144143oveq1d 6096 . . . . 5
145144oveq1d 6096 . . . 4
146128, 125eqeltrd 2510 . . . . . . . 8
147146sqcld 11521 . . . . . . 7
148131, 120eqtrd 2468 . . . . . . . . . 10
149148, 113, 106, 64fvmptd 5810 . . . . . . . . 9
150149, 64eqeltrd 2510 . . . . . . . 8
151150sqcld 11521 . . . . . . 7
152 nnne0 10032 . . . . . . . . . . . 12
15355, 56, 1523syl 19 . . . . . . . . . . 11
15458, 64, 153, 76divne0d 9806 . . . . . . . . . 10
155108, 154eqnetrd 2619 . . . . . . . . 9
156128, 155eqnetrd 2619 . . . . . . . 8
157146, 156, 73expne0d 11529 . . . . . . 7
158149, 76eqnetrd 2619 . . . . . . . 8
159150, 158, 73expne0d 11529 . . . . . . 7
160142, 147, 141, 151, 157, 159divmuldivd 9831 . . . . . 6
161160eqcomd 2441 . . . . 5
162161oveq1d 6096 . . . 4
16334, 31eqeltrd 2510 . . . . . . . . 9
164163, 42expcld 11523 . . . . . . . 8
16539, 46eqeltrd 2510 . . . . . . . 8
166164, 165, 147, 157div23d 9827 . . . . . . 7
167166oveq1d 6096 . . . . . 6
168167oveq1d 6096 . . . . 5
169164, 147, 157divcld 9790 . . . . . . 7
170141, 151, 159divcld 9790 . . . . . . 7
171169, 165, 170mulassd 9111 . . . . . 6
172171oveq1d 6096 . . . . 5
173165, 170mulcld 9108 . . . . . . 7
174 ax-1cn 9048 . . . . . . . . 9
175174a1i 11 . . . . . . . 8
1769, 175addcld 9107 . . . . . . 7
177 0re 9091 . . . . . . . . . 10
178177a1i 11 . . . . . . . . 9
179106nnred 10015 . . . . . . . . 9
180 2re 10069 . . . . . . . . . . . 12
181180a1i 11 . . . . . . . . . . 11
182 nnre 10007 . . . . . . . . . . 11
183181, 182remulcld 9116 . . . . . . . . . 10
184 1re 9090 . . . . . . . . . . 11
185184a1i 11 . . . . . . . . . 10
186183, 185readdcld 9115 . . . . . . . . 9
187106nngt0d 10043 . . . . . . . . 9
188179ltp1d 9941 . . . . . . . . 9
189178, 179, 186, 187, 188lttrd 9231 . . . . . . . 8
190189gt0ne0d 9591 . . . . . . 7
191169, 173, 176, 190divassd 9825 . . . . . 6
192165, 141, 151, 159div12d 9826 . . . . . . . . . 10
19310, 18, 42mulexpd 11538 . . . . . . . . . . . . 13
19461, 63sqmuld 11535 . . . . . . . . . . . . 13
195193, 194oveq12d 6099 . . . . . . . . . . . 12
196149oveq1d 6096 . . . . . . . . . . . . 13
19739, 196oveq12d 6099 . . . . . . . . . . . 12
19810, 42expcld 11523 . . . . . . . . . . . . 13
19961sqcld 11521 . . . . . . . . . . . . 13
20018, 42expcld 11523 . . . . . . . . . . . . 13
20163sqcld 11521 . . . . . . . . . . . . 13
20261, 68, 73expne0d 11529 . . . . . . . . . . . . 13
20363, 75, 73expne0d 11529 . . . . . . . . . . . . 13
204198, 199, 200, 201, 202, 203divmuldivd 9831 . . . . . . . . . . . 12
205195, 197, 2043eqtr4d 2478 . . . . . . . . . . 11
206205oveq2d 6097 . . . . . . . . . 10
20766rprege0d 10655 . . . . . . . . . . . . . . . 16
208 resqrth 12061 . . . . . . . . . . . . . . . 16
209207, 208syl 16 . . . . . . . . . . . . . . 15
210209oveq2d 6097 . . . . . . . . . . . . . 14
211 2t2e4 10127 . . . . . . . . . . . . . . . . . . 19
212211eqcomi 2440 . . . . . . . . . . . . . . . . . 18
213212a1i 11 . . . . . . . . . . . . . . . . 17
214213oveq2d 6097 . . . . . . . . . . . . . . . 16
21510, 54, 54expmuld 11526 . . . . . . . . . . . . . . . 16
21623rprege0d 10655 . . . . . . . . . . . . . . . . . 18
217 resqrth 12061 . . . . . . . . . . . . . . . . . 18
218216, 217syl 16 . . . . . . . . . . . . . . . . 17
219218oveq1d 6096 . . . . . . . . . . . . . . . 16
220214, 215, 2193eqtrd 2472 . . . . . . . . . . . . . . 15
2217, 7, 8mulassd 9111 . . . . . . . . . . . . . . . 16
222211a1i 11 . . . . . . . . . . . . . . . . 17
223222oveq1d 6096 . . . . . . . . . . . . . . . 16
224221, 223eqtr3d 2470 . . . . . . . . . . . . . . 15
225220, 224oveq12d 6099 . . . . . . . . . . . . . 14
2267, 8sqmuld 11535 . . . . . . . . . . . . . . . . 17
227 sq2 11477 . . . . . . . . . . . . . . . . . . 19
228227a1i 11 . . . . . . . . . . . . . . . . . 18
229228oveq1d 6096 . . . . . . . . . . . . . . . . 17
230226, 229eqtrd 2468 . . . . . . . . . . . . . . . 16
231230oveq1d 6096 . . . . . . . . . . . . . . 15
232 4cn 10074 . . . . . . . . . . . . . . . . . . 19
233 4pos 10086 . . . . . . . . . . . . . . . . . . . 20
234177, 233gtneii 9185 . . . . . . . . . . . . . . . . . . 19
235232, 234dividi 9747 . . . . . . . . . . . . . . . . . 18
236235a1i 11 . . . . . . . . . . . . . . . . 17
2378sqvald 11520 . . . . . . . . . . . . . . . . . . 19
238237oveq1d 6096 . . . . . . . . . . . . . . . . . 18
2398, 8, 26divcan4d 9796 . . . . . . . . . . . . . . . . . 18
240238, 239eqtrd 2468 . . . . . . . . . . . . . . . . 17
241236, 240oveq12d 6099 . . . . . . . . . . . . . . . 16
24242nn0cnd 10276 . . . . . . . . . . . . . . . . 17
2438sqcld 11521 . . . . . . . . . . . . . . . . 17
244234a1i 11 . . . . . . . . . . . . . . . . 17
245242, 242, 243, 8, 244, 26divmuldivd 9831 . . . . . . . . . . . . . . . 16
2468mulid2d 9106 . . . . . . . . . . . . . . . 16
247241, 245, 2463eqtr3d 2476 . . . . . . . . . . . . . . 15
248231, 247eqtrd 2468 . . . . . . . . . . . . . 14
249210, 225, 2483eqtrd 2472 . . . . . . . . . . . . 13
2508, 242mulcomd 9109 . . . . . . . . . . . . . . . . 17
251250oveq2d 6097 . . . . . . . . . . . . . . . 16
25217, 42, 2expmuld 11526 . . . . . . . . . . . . . . . 16
2538, 13, 16, 140expdivd 11537 . . . . . . . . . . . . . . . 16
254251, 252, 2533eqtr3d 2476 . . . . . . . . . . . . . . 15
2557, 8, 7mul32d 9276 . . . . . . . . . . . . . . . . . 18
256255, 223eqtrd 2468 . . . . . . . . . . . . . . . . 17
257256oveq2d 6097 . . . . . . . . . . . . . . . 16
25862, 54, 55expmuld 11526 . . . . . . . . . . . . . . . 16
2599, 13, 16, 140expdivd 11537 . . . . . . . . . . . . . . . 16
260257, 258, 2593eqtr3d 2476 . . . . . . . . . . . . . . 15
261254, 260oveq12d 6099 . . . . . . . . . . . . . 14
262254, 200eqeltrrd 2511 . . . . . . . . . . . . . . 15
2639, 140expcld 11523 . . . . . . . . . . . . . . 15
26413, 140expcld 11523 . . . . . . . . . . . . . . 15
26547, 28zmulcld 10381 . . . . . . . . . . . . . . . 16
2669, 70, 265expne0d 11529 . . . . . . . . . . . . . . 15
26713, 16, 265expne0d 11529 . . . . . . . . . . . . . . 15
268262, 263, 264, 266, 267divdiv2d 9822 . . . . . . . . . . . . . 14
2698, 140expcld 11523 . . . . . . . . . . . . . . . . 17
270269, 264, 267divcan1d 9791 . . . . . . . . . . . . . . . 16
271270oveq1d 6096 . . . . . . . . . . . . . . 15
2727, 8, 140mulexpd 11538 . . . . . . . . . . . . . . . 16
273272oveq2d 6097 . . . . . . . . . . . . . . 15
274141, 269mulcomd 9109 . . . . . . . . . . . . . . . . 17
275274oveq2d 6097 . . . . . . . . . . . . . . . 16
2768, 26, 265expne0d 11529 . . . . . . . . . . . . . . . . 17
2777, 69, 265expne0d 11529 . . . . . . . . . . . . . . . . 17
278269, 269, 141, 276, 277divdiv1d 9821 . . . . . . . . . . . . . . . 16
279269, 276dividd 9788 . . . . . . . . . . . . . . . . 17
280279oveq1d 6096 . . . . . . . . . . . . . . . 16
281275, 278, 2803eqtr2d 2474 . . . . . . . . . . . . . . 15
282271, 273, 2813eqtrd 2472 . . . . . . . . . . . . . 14
283261, 268, 2823eqtrd 2472 . . . . . . . . . . . . 13
284249, 283oveq12d 6099 . . . . . . . . . . . 12
285284oveq2d 6097 . . . . . . . . . . 11
286141, 277reccld 9783 . . . . . . . . . . . 12
287141, 8, 286mul12d 9275 . . . . . . . . . . 11
2888mulid1d 9105 . . . . . . . . . . . 12
289141, 277recidd 9785 . . . . . . . . . . . . 13
290289oveq2d 6097 . . . . . . . . . . . 12
291288, 290, 2403eqtr4d 2478 . . . . . . . . . . 11
292285, 287, 2913eqtrd 2472 . . . . . . . . . 10
293192, 206, 2923eqtrd 2472 . . . . . . . . 9
294293oveq1d 6096 . . . . . . . 8
295243, 8, 176, 26, 190divdiv1d 9821 . . . . . . . 8
296294, 295eqtrd 2468 . . . . . . 7
297296oveq2d 6097 . . . . . 6
298191, 297eqtrd 2468 . . . . 5
299168, 172, 2983eqtrd 2472 . . . 4
300145, 162, 2993eqtrd 2472 . . 3
301300mpteq2ia 4291 . 2
3021, 139, 3013eqtri 2460 1
 Colors of variables: wff set class Syntax hints:   wa 359   wceq 1652   wcel 1725   wne 2599   class class class wbr 4212   cmpt 4266  cfv 5454  (class class class)co 6081  cc 8988  cr 8989  cc0 8990  c1 8991   caddc 8993   cmul 8995   cle 9121   cdiv 9677  cn 10000  c2 10049  c4 10051  cn0 10221  cz 10282  crp 10612  cexp 11382  cfa 11566  csqr 12038  ceu 12665 This theorem is referenced by:  stirlinglem15  27813 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-inf2 7596  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067  ax-pre-sup 9068  ax-addf 9069  ax-mulf 9070 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-oadd 6728  df-er 6905  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-oi 7479  df-card 7826  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-div 9678  df-nn 10001  df-2 10058  df-3 10059  df-4 10060  df-n0 10222  df-z 10283  df-uz 10489  df-q 10575  df-rp 10613  df-ico 10922  df-fz 11044  df-fzo 11136  df-fl 11202  df-seq 11324  df-exp 11383  df-fac 11567  df-bc 11594  df-hash 11619  df-shft 11882  df-cj 11904  df-re 11905  df-im 11906  df-sqr 12040  df-abs 12041  df-limsup 12265  df-clim 12282  df-rlim 12283  df-sum 12480  df-ef 12670  df-e 12671
 Copyright terms: Public domain W3C validator