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

Theorem stirlinglem3 31376
 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 10798 . . . . . . . . . . . . 13
3 faccl 12325 . . . . . . . . . . . . 13
4 nncn 10540 . . . . . . . . . . . . 13
52, 3, 43syl 20 . . . . . . . . . . . 12
6 2cnd 10604 . . . . . . . . . . . . . . 15
7 nncn 10540 . . . . . . . . . . . . . . 15
86, 7mulcld 9612 . . . . . . . . . . . . . 14
98sqrtcld 13224 . . . . . . . . . . . . 13
10 ere 13679 . . . . . . . . . . . . . . . . 17
1110recni 9604 . . . . . . . . . . . . . . . 16
1211a1i 11 . . . . . . . . . . . . . . 15
13 epos 13794 . . . . . . . . . . . . . . . . 17
1410, 13gt0ne0ii 10085 . . . . . . . . . . . . . . . 16
1514a1i 11 . . . . . . . . . . . . . . 15
167, 12, 15divcld 10316 . . . . . . . . . . . . . 14
1716, 2expcld 12272 . . . . . . . . . . . . 13
189, 17mulcld 9612 . . . . . . . . . . . 12
19 2rp 11221 . . . . . . . . . . . . . . . . 17
2019a1i 11 . . . . . . . . . . . . . . . 16
21 nnrp 11225 . . . . . . . . . . . . . . . 16
2220, 21rpmulcld 11268 . . . . . . . . . . . . . . 15
2322sqrtgt0d 13200 . . . . . . . . . . . . . 14
2423gt0ne0d 10113 . . . . . . . . . . . . 13
25 nnne0 10564 . . . . . . . . . . . . . . 15
267, 12, 25, 15divne0d 10332 . . . . . . . . . . . . . 14
27 nnz 10882 . . . . . . . . . . . . . 14
2816, 26, 27expne0d 12278 . . . . . . . . . . . . 13
299, 17, 24, 28mulne0d 10197 . . . . . . . . . . . 12
305, 18, 29divcld 10316 . . . . . . . . . . 11
31 stirlinglem3.1 . . . . . . . . . . . 12
3231fvmpt2 5955 . . . . . . . . . . 11
3330, 32mpdan 668 . . . . . . . . . 10
3433oveq1d 6297 . . . . . . . . 9
35 stirlinglem3.3 . . . . . . . . . . . 12
3635fvmpt2 5955 . . . . . . . . . . 11
3718, 36mpdan 668 . . . . . . . . . 10
3837oveq1d 6297 . . . . . . . . 9
3934, 38oveq12d 6300 . . . . . . . 8
40 4nn0 10810 . . . . . . . . . . 11
4140a1i 11 . . . . . . . . . 10
425, 18, 29, 41expdivd 12286 . . . . . . . . 9
4342oveq1d 6297 . . . . . . . 8
445, 41expcld 12272 . . . . . . . . 9
4518, 41expcld 12272 . . . . . . . . 9
4641nn0zd 10960 . . . . . . . . . 10
4718, 29, 46expne0d 12278 . . . . . . . . 9
4844, 45, 47divcan1d 10317 . . . . . . . 8
4939, 43, 483eqtrd 2512 . . . . . . 7
5049eqcomd 2475 . . . . . 6
5150oveq2d 6298 . . . . 5
52 2nn0 10808 . . . . . . . . . . . . 13
5352a1i 11 . . . . . . . . . . . 12
5453, 2nn0mulcld 10853 . . . . . . . . . . 11
55 faccl 12325 . . . . . . . . . . 11
56 nncn 10540 . . . . . . . . . . 11
5754, 55, 563syl 20 . . . . . . . . . 10
5857sqcld 12270 . . . . . . . . 9
596, 8mulcld 9612 . . . . . . . . . . . 12
6059sqrtcld 13224 . . . . . . . . . . 11
618, 12, 15divcld 10316 . . . . . . . . . . . 12
6261, 54expcld 12272 . . . . . . . . . . 11
6360, 62mulcld 9612 . . . . . . . . . 10
6463sqcld 12270 . . . . . . . . 9
6520, 22rpmulcld 11268 . . . . . . . . . . . . 13
6665sqrtgt0d 13200 . . . . . . . . . . . 12
6766gt0ne0d 10113 . . . . . . . . . . 11
6820rpne0d 11257 . . . . . . . . . . . . . 14
696, 7, 68, 25mulne0d 10197 . . . . . . . . . . . . 13
708, 12, 69, 15divne0d 10332 . . . . . . . . . . . 12
71 2z 10892 . . . . . . . . . . . . . 14
7271a1i 11 . . . . . . . . . . . . 13
7372, 27zmulcld 10968 . . . . . . . . . . . 12
7461, 70, 73expne0d 12278 . . . . . . . . . . 11
7560, 62, 67, 74mulne0d 10197 . . . . . . . . . 10
7663, 75, 72expne0d 12278 . . . . . . . . 9
7758, 64, 76divcan1d 10317 . . . . . . . 8
7857, 63, 75, 53expdivd 12286 . . . . . . . . . 10
7978eqcomd 2475 . . . . . . . . 9
8079oveq1d 6297 . . . . . . . 8
8177, 80eqtr3d 2510 . . . . . . 7
82 fveq2 5864 . . . . . . . . . . . . . . 15
83 oveq2 6290 . . . . . . . . . . . . . . . . 17
8483fveq2d 5868 . . . . . . . . . . . . . . . 16
85 oveq1 6289 . . . . . . . . . . . . . . . . 17
86 id 22 . . . . . . . . . . . . . . . . 17
8785, 86oveq12d 6300 . . . . . . . . . . . . . . . 16
8884, 87oveq12d 6300 . . . . . . . . . . . . . . 15
8982, 88oveq12d 6300 . . . . . . . . . . . . . 14
9089cbvmptv 4538 . . . . . . . . . . . . 13
9131, 90eqtri 2496 . . . . . . . . . . . 12
9291a1i 11 . . . . . . . . . . 11
93 fveq2 5864 . . . . . . . . . . . . 13
94 oveq2 6290 . . . . . . . . . . . . . . 15
9594fveq2d 5868 . . . . . . . . . . . . . 14
96 oveq1 6289 . . . . . . . . . . . . . . 15
97 id 22 . . . . . . . . . . . . . . 15
9896, 97oveq12d 6300 . . . . . . . . . . . . . 14
9995, 98oveq12d 6300 . . . . . . . . . . . . 13
10093, 99oveq12d 6300 . . . . . . . . . . . 12
101100adantl 466 . . . . . . . . . . 11
102 2nn 10689 . . . . . . . . . . . . 13
103102a1i 11 . . . . . . . . . . . 12
104 id 22 . . . . . . . . . . . 12
105103, 104nnmulcld 10579 . . . . . . . . . . 11
10657, 63, 75divcld 10316 . . . . . . . . . . 11
10792, 101, 105, 106fvmptd 5953 . . . . . . . . . 10
108107oveq1d 6297 . . . . . . . . 9
109108eqcomd 2475 . . . . . . . 8
110109oveq1d 6297 . . . . . . 7
111 eqidd 2468 . . . . . . . . . . 11
11299adantl 466 . . . . . . . . . . 11
113111, 112, 105, 63fvmptd 5953 . . . . . . . . . 10
114113oveq1d 6297 . . . . . . . . 9
115114eqcomd 2475 . . . . . . . 8
116115oveq2d 6298 . . . . . . 7
11781, 110, 1163eqtrd 2512 . . . . . 6
11888cbvmptv 4538 . . . . . . . . . . 11
119118a1i 11 . . . . . . . . . 10
120119fveq1d 5866 . . . . . . . . 9
121120eqcomd 2475 . . . . . . . 8
122121oveq1d 6297 . . . . . . 7
123122oveq2d 6298 . . . . . 6
124107, 106eqeltrd 2555 . . . . . . . . . 10
125 stirlinglem3.2 . . . . . . . . . . 11
126125fvmpt2 5955 . . . . . . . . . 10
127124, 126mpdan 668 . . . . . . . . 9
128127eqcomd 2475 . . . . . . . 8
129128oveq1d 6297 . . . . . . 7
13035a1i 11 . . . . . . . . . 10
131130fveq1d 5866 . . . . . . . . 9
132131eqcomd 2475 . . . . . . . 8
133132oveq1d 6297 . . . . . . 7
134129, 133oveq12d 6300 . . . . . 6
135117, 123, 1343eqtrd 2512 . . . . 5
13651, 135oveq12d 6300 . . . 4
137136oveq1d 6297 . . 3
138137mpteq2ia 4529 . 2
13941, 2nn0mulcld 10853 . . . . . . . 8
1406, 139expcld 12272 . . . . . . 7
14149, 44eqeltrd 2555 . . . . . . 7
142140, 141mulcomd 9613 . . . . . 6
143142oveq1d 6297 . . . . 5
144143oveq1d 6297 . . . 4
145127, 124eqeltrd 2555 . . . . . . . 8
146145sqcld 12270 . . . . . . 7
147130, 119eqtrd 2508 . . . . . . . . . 10
148147, 112, 105, 63fvmptd 5953 . . . . . . . . 9
149148, 63eqeltrd 2555 . . . . . . . 8
150149sqcld 12270 . . . . . . 7
151 nnne0 10564 . . . . . . . . . . . 12
15254, 55, 1513syl 20 . . . . . . . . . . 11
15357, 63, 152, 75divne0d 10332 . . . . . . . . . 10
154107, 153eqnetrd 2760 . . . . . . . . 9
155127, 154eqnetrd 2760 . . . . . . . 8
156145, 155, 72expne0d 12278 . . . . . . 7
157148, 75eqnetrd 2760 . . . . . . . 8
158149, 157, 72expne0d 12278 . . . . . . 7
159141, 146, 140, 150, 156, 158divmuldivd 10357 . . . . . 6
160159eqcomd 2475 . . . . 5
161160oveq1d 6297 . . . 4
16233, 30eqeltrd 2555 . . . . . . . . 9
163162, 41expcld 12272 . . . . . . . 8
16438, 45eqeltrd 2555 . . . . . . . 8
165163, 164, 146, 156div23d 10353 . . . . . . 7
166165oveq1d 6297 . . . . . 6
167166oveq1d 6297 . . . . 5
168163, 146, 156divcld 10316 . . . . . . 7
169140, 150, 158divcld 10316 . . . . . . 7
170168, 164, 169mulassd 9615 . . . . . 6
171170oveq1d 6297 . . . . 5
172164, 169mulcld 9612 . . . . . . 7
173 ax-1cn 9546 . . . . . . . . 9
174173a1i 11 . . . . . . . 8
1758, 174addcld 9611 . . . . . . 7
176 0re 9592 . . . . . . . . . 10
177176a1i 11 . . . . . . . . 9
178105nnred 10547 . . . . . . . . 9
179 2re 10601 . . . . . . . . . . . 12
180179a1i 11 . . . . . . . . . . 11
181 nnre 10539 . . . . . . . . . . 11
182180, 181remulcld 9620 . . . . . . . . . 10
183 1re 9591 . . . . . . . . . . 11
184183a1i 11 . . . . . . . . . 10
185182, 184readdcld 9619 . . . . . . . . 9
186105nngt0d 10575 . . . . . . . . 9
187178ltp1d 10472 . . . . . . . . 9
188177, 178, 185, 186, 187lttrd 9738 . . . . . . . 8
189188gt0ne0d 10113 . . . . . . 7
190168, 172, 175, 189divassd 10351 . . . . . 6
191164, 140, 150, 158div12d 10352 . . . . . . . . . 10
1929, 17, 41mulexpd 12287 . . . . . . . . . . . . 13
19360, 62sqmuld 12284 . . . . . . . . . . . . 13
194192, 193oveq12d 6300 . . . . . . . . . . . 12
195148oveq1d 6297 . . . . . . . . . . . . 13
19638, 195oveq12d 6300 . . . . . . . . . . . 12
1979, 41expcld 12272 . . . . . . . . . . . . 13
19860sqcld 12270 . . . . . . . . . . . . 13
19917, 41expcld 12272 . . . . . . . . . . . . 13
20062sqcld 12270 . . . . . . . . . . . . 13
20160, 67, 72expne0d 12278 . . . . . . . . . . . . 13
20262, 74, 72expne0d 12278 . . . . . . . . . . . . 13
203197, 198, 199, 200, 201, 202divmuldivd 10357 . . . . . . . . . . . 12
204194, 196, 2033eqtr4d 2518 . . . . . . . . . . 11
205204oveq2d 6298 . . . . . . . . . 10
20665rprege0d 11259 . . . . . . . . . . . . . . . 16
207 resqrtth 13046 . . . . . . . . . . . . . . . 16
208206, 207syl 16 . . . . . . . . . . . . . . 15
209208oveq2d 6298 . . . . . . . . . . . . . 14
210 2t2e4 10681 . . . . . . . . . . . . . . . . . . 19
211210eqcomi 2480 . . . . . . . . . . . . . . . . . 18
212211a1i 11 . . . . . . . . . . . . . . . . 17
213212oveq2d 6298 . . . . . . . . . . . . . . . 16
2149, 53, 53expmuld 12275 . . . . . . . . . . . . . . . 16
21522rprege0d 11259 . . . . . . . . . . . . . . . . . 18
216 resqrtth 13046 . . . . . . . . . . . . . . . . . 18
217215, 216syl 16 . . . . . . . . . . . . . . . . 17
218217oveq1d 6297 . . . . . . . . . . . . . . . 16
219213, 214, 2183eqtrd 2512 . . . . . . . . . . . . . . 15
2206, 6, 7mulassd 9615 . . . . . . . . . . . . . . . 16
221210a1i 11 . . . . . . . . . . . . . . . . 17
222221oveq1d 6297 . . . . . . . . . . . . . . . 16
223220, 222eqtr3d 2510 . . . . . . . . . . . . . . 15
224219, 223oveq12d 6300 . . . . . . . . . . . . . 14
2256, 7sqmuld 12284 . . . . . . . . . . . . . . . . 17
226 sq2 12226 . . . . . . . . . . . . . . . . . . 19
227226a1i 11 . . . . . . . . . . . . . . . . . 18
228227oveq1d 6297 . . . . . . . . . . . . . . . . 17
229225, 228eqtrd 2508 . . . . . . . . . . . . . . . 16
230229oveq1d 6297 . . . . . . . . . . . . . . 15
231 4cn 10609 . . . . . . . . . . . . . . . . . . 19
232 4ne0 10628 . . . . . . . . . . . . . . . . . . 19
233231, 232dividi 10273 . . . . . . . . . . . . . . . . . 18
234233a1i 11 . . . . . . . . . . . . . . . . 17
2357sqvald 12269 . . . . . . . . . . . . . . . . . . 19
236235oveq1d 6297 . . . . . . . . . . . . . . . . . 18
2377, 7, 25divcan4d 10322 . . . . . . . . . . . . . . . . . 18
238236, 237eqtrd 2508 . . . . . . . . . . . . . . . . 17
239234, 238oveq12d 6300 . . . . . . . . . . . . . . . 16
24041nn0cnd 10850 . . . . . . . . . . . . . . . . 17
2417sqcld 12270 . . . . . . . . . . . . . . . . 17
242232a1i 11 . . . . . . . . . . . . . . . . 17
243240, 240, 241, 7, 242, 25divmuldivd 10357 . . . . . . . . . . . . . . . 16
2447mulid2d 9610 . . . . . . . . . . . . . . . 16
245239, 243, 2443eqtr3d 2516 . . . . . . . . . . . . . . 15
246230, 245eqtrd 2508 . . . . . . . . . . . . . 14
247209, 224, 2463eqtrd 2512 . . . . . . . . . . . . 13
2487, 240mulcomd 9613 . . . . . . . . . . . . . . . . 17
249248oveq2d 6298 . . . . . . . . . . . . . . . 16
25016, 41, 2expmuld 12275 . . . . . . . . . . . . . . . 16
2517, 12, 15, 139expdivd 12286 . . . . . . . . . . . . . . . 16
252249, 250, 2513eqtr3d 2516 . . . . . . . . . . . . . . 15
2536, 7, 6mul32d 9785 . . . . . . . . . . . . . . . . . 18
254253, 222eqtrd 2508 . . . . . . . . . . . . . . . . 17
255254oveq2d 6298 . . . . . . . . . . . . . . . 16
25661, 53, 54expmuld 12275 . . . . . . . . . . . . . . . 16
2578, 12, 15, 139expdivd 12286 . . . . . . . . . . . . . . . 16
258255, 256, 2573eqtr3d 2516 . . . . . . . . . . . . . . 15
259252, 258oveq12d 6300 . . . . . . . . . . . . . 14
260252, 199eqeltrrd 2556 . . . . . . . . . . . . . . 15
2618, 139expcld 12272 . . . . . . . . . . . . . . 15
26212, 139expcld 12272 . . . . . . . . . . . . . . 15
26346, 27zmulcld 10968 . . . . . . . . . . . . . . . 16
2648, 69, 263expne0d 12278 . . . . . . . . . . . . . . 15
26512, 15, 263expne0d 12278 . . . . . . . . . . . . . . 15
266260, 261, 262, 264, 265divdiv2d 10348 . . . . . . . . . . . . . 14
2677, 139expcld 12272 . . . . . . . . . . . . . . . . 17
268267, 262, 265divcan1d 10317 . . . . . . . . . . . . . . . 16
269268oveq1d 6297 . . . . . . . . . . . . . . 15
2706, 7, 139mulexpd 12287 . . . . . . . . . . . . . . . 16
271270oveq2d 6298 . . . . . . . . . . . . . . 15
272140, 267mulcomd 9613 . . . . . . . . . . . . . . . . 17
273272oveq2d 6298 . . . . . . . . . . . . . . . 16
2747, 25, 263expne0d 12278 . . . . . . . . . . . . . . . . 17
2756, 68, 263expne0d 12278 . . . . . . . . . . . . . . . . 17
276267, 267, 140, 274, 275divdiv1d 10347 . . . . . . . . . . . . . . . 16
277267, 274dividd 10314 . . . . . . . . . . . . . . . . 17
278277oveq1d 6297 . . . . . . . . . . . . . . . 16
279273, 276, 2783eqtr2d 2514 . . . . . . . . . . . . . . 15
280269, 271, 2793eqtrd 2512 . . . . . . . . . . . . . 14
281259, 266, 2803eqtrd 2512 . . . . . . . . . . . . 13
282247, 281oveq12d 6300 . . . . . . . . . . . 12
283282oveq2d 6298 . . . . . . . . . . 11
284140, 275reccld 10309 . . . . . . . . . . . 12
285140, 7, 284mul12d 9784 . . . . . . . . . . 11
2867mulid1d 9609 . . . . . . . . . . . 12
287140, 275recidd 10311 . . . . . . . . . . . . 13
288287oveq2d 6298 . . . . . . . . . . . 12
289286, 288, 2383eqtr4d 2518 . . . . . . . . . . 11
290283, 285, 2893eqtrd 2512 . . . . . . . . . 10
291191, 205, 2903eqtrd 2512 . . . . . . . . 9
292291oveq1d 6297 . . . . . . . 8
293241, 7, 175, 25, 189divdiv1d 10347 . . . . . . . 8
294292, 293eqtrd 2508 . . . . . . 7
295294oveq2d 6298 . . . . . 6
296190, 295eqtrd 2508 . . . . 5
297167, 171, 2963eqtrd 2512 . . . 4
298144, 161, 2973eqtrd 2512 . . 3
299298mpteq2ia 4529 . 2
3001, 138, 2993eqtri 2500 1
 Colors of variables: wff setvar class Syntax hints:   wa 369   wceq 1379   wcel 1767   wne 2662   class class class wbr 4447   cmpt 4505  cfv 5586  (class class class)co 6282  cc 9486  cr 9487  cc0 9488  c1 9489   caddc 9491   cmul 9493   cle 9625   cdiv 10202  cn 10532  c2 10581  c4 10583  cn0 10791  cz 10860  crp 11216  cexp 12129  cfa 12315  csqrt 13023  ceu 13653 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566  ax-addf 9567  ax-mulf 9568 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-pm 7420  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-sup 7897  df-oi 7931  df-card 8316  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-4 10592  df-n0 10792  df-z 10861  df-uz 11079  df-q 11179  df-rp 11217  df-ico 11531  df-fz 11669  df-fzo 11789  df-fl 11893  df-seq 12071  df-exp 12130  df-fac 12316  df-bc 12343  df-hash 12368  df-shft 12857  df-cj 12889  df-re 12890  df-im 12891  df-sqrt 13025  df-abs 13026  df-limsup 13250  df-clim 13267  df-rlim 13268  df-sum 13465  df-ef 13658  df-e 13659 This theorem is referenced by:  stirlinglem15  31388
 Copyright terms: Public domain W3C validator