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

Theorem stirlinglem10 37762
 Description: A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem10.1
stirlinglem10.2
stirlinglem10.4
stirlinglem10.5
Assertion
Ref Expression
stirlinglem10
Distinct variable groups:   ,   ,   ,   ,,
Allowed substitution hints:   (,)   (,)   ()   ()

Proof of Theorem stirlinglem10
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11194 . 2
2 1zzd 10968 . 2
3 stirlinglem10.1 . . 3
4 stirlinglem10.2 . . 3
5 eqid 2422 . . 3
6 stirlinglem10.4 . . 3
73, 4, 5, 6stirlinglem9 37761 . 2
8 2cnd 10682 . . . . . . . 8
9 nncn 10617 . . . . . . . 8
108, 9mulcld 9663 . . . . . . 7
11 1cnd 9659 . . . . . . 7
1210, 11addcld 9662 . . . . . 6
1312sqcld 12413 . . . . 5
14 0red 9644 . . . . . . . 8
15 1red 9658 . . . . . . . 8
16 2re 10679 . . . . . . . . . . 11
1716a1i 11 . . . . . . . . . 10
18 nnre 10616 . . . . . . . . . 10
1917, 18remulcld 9671 . . . . . . . . 9
2019, 15readdcld 9670 . . . . . . . 8
21 0lt1 10136 . . . . . . . . 9
2221a1i 11 . . . . . . . 8
23 2rp 11307 . . . . . . . . . . 11
2423a1i 11 . . . . . . . . . 10
25 nnrp 11311 . . . . . . . . . 10
2624, 25rpmulcld 11357 . . . . . . . . 9
2715, 26ltaddrp2d 11372 . . . . . . . 8
2814, 15, 20, 22, 27lttrd 9796 . . . . . . 7
2928gt0ne0d 10178 . . . . . 6
30 2z 10969 . . . . . . 7
3130a1i 11 . . . . . 6
3212, 29, 31expne0d 12421 . . . . 5
3313, 32reccld 10376 . . . 4
3415renegcld 10046 . . . . . 6
3520resqcld 12441 . . . . . . 7
3635, 32rereccld 10434 . . . . . 6
37 1re 9642 . . . . . . . 8
38 lt0neg2 10121 . . . . . . . 8
3937, 38ax-mp 5 . . . . . . 7
4022, 39sylib 199 . . . . . 6
4120, 29sqgt0d 12443 . . . . . . 7
4235, 41recgt0d 10541 . . . . . 6
4334, 14, 36, 40, 42lttrd 9796 . . . . 5
44 2nn 10767 . . . . . . . 8
4544a1i 11 . . . . . . 7
46 expgt1 12309 . . . . . . 7
4720, 45, 27, 46syl3anc 1264 . . . . . 6
4835, 41elrpd 11338 . . . . . . 7
4948recgt1d 11355 . . . . . 6
5047, 49mpbid 213 . . . . 5
5136, 15absltd 13477 . . . . 5
5243, 50, 51mpbir2and 930 . . . 4
53 1nn0 10885 . . . . 5
5453a1i 11 . . . 4
55 stirlinglem10.5 . . . . . 6
5655a1i 11 . . . . 5
57 simpr 462 . . . . . 6
5857oveq2d 6317 . . . . 5
59 elnnuz 11195 . . . . . . 7
6059biimpri 209 . . . . . 6
6160adantl 467 . . . . 5
6233adantr 466 . . . . . 6
6361nnnn0d 10925 . . . . . 6
6462, 63expcld 12415 . . . . 5
6556, 58, 61, 64fvmptd 5966 . . . 4
6633, 52, 54, 65geolim2 13912 . . 3
6733exp1d 12410 . . . . 5
6813, 32dividd 10381 . . . . . . . 8
6968eqcomd 2430 . . . . . . 7
7069oveq1d 6316 . . . . . 6
7148rpcnne0d 11350 . . . . . . 7
72 divsubdir 10303 . . . . . . 7
7313, 11, 71, 72syl3anc 1264 . . . . . 6
74 ax-1cn 9597 . . . . . . . . . 10
75 binom2 12388 . . . . . . . . . 10
7610, 74, 75sylancl 666 . . . . . . . . 9
7776oveq1d 6316 . . . . . . . 8
788, 9sqmuld 12427 . . . . . . . . . . . . 13
79 sq2 12370 . . . . . . . . . . . . . . 15
8079a1i 11 . . . . . . . . . . . . . 14
8180oveq1d 6316 . . . . . . . . . . . . 13
8278, 81eqtrd 2463 . . . . . . . . . . . 12
8310mulid1d 9660 . . . . . . . . . . . . . 14
8483oveq2d 6317 . . . . . . . . . . . . 13
858, 8, 9mulassd 9666 . . . . . . . . . . . . 13
86 2t2e4 10759 . . . . . . . . . . . . . . 15
8786a1i 11 . . . . . . . . . . . . . 14
8887oveq1d 6316 . . . . . . . . . . . . 13
8984, 85, 883eqtr2d 2469 . . . . . . . . . . . 12
9082, 89oveq12d 6319 . . . . . . . . . . 11
91 4cn 10687 . . . . . . . . . . . . 13
9291a1i 11 . . . . . . . . . . . 12
939sqcld 12413 . . . . . . . . . . . 12
9492, 93, 9adddid 9667 . . . . . . . . . . 11
959sqvald 12412 . . . . . . . . . . . . . 14
969mulid1d 9660 . . . . . . . . . . . . . . 15
9796eqcomd 2430 . . . . . . . . . . . . . 14
9895, 97oveq12d 6319 . . . . . . . . . . . . 13
999, 9, 11adddid 9667 . . . . . . . . . . . . 13
10098, 99eqtr4d 2466 . . . . . . . . . . . 12
101100oveq2d 6317 . . . . . . . . . . 11
10290, 94, 1013eqtr2d 2469 . . . . . . . . . 10
103 sq1 12368 . . . . . . . . . . 11
104103a1i 11 . . . . . . . . . 10
105102, 104oveq12d 6319 . . . . . . . . 9
106105oveq1d 6316 . . . . . . . 8
1079, 11addcld 9662 . . . . . . . . . . 11
1089, 107mulcld 9663 . . . . . . . . . 10
10992, 108mulcld 9663 . . . . . . . . 9
110109, 11pncand 9987 . . . . . . . 8
11177, 106, 1103eqtrd 2467 . . . . . . 7
112111oveq1d 6316 . . . . . 6
11370, 73, 1123eqtr2d 2469 . . . . 5
11467, 113oveq12d 6319 . . . 4
115 4pos 10705 . . . . . . . . 9
116115a1i 11 . . . . . . . 8
117116gt0ne0d 10178 . . . . . . 7
118 nnne0 10642 . . . . . . . 8
11918, 15readdcld 9670 . . . . . . . . . 10
120 nngt0 10638 . . . . . . . . . 10
12118ltp1d 10537 . . . . . . . . . 10
12214, 18, 119, 120, 121lttrd 9796 . . . . . . . . 9
123122gt0ne0d 10178 . . . . . . . 8
1249, 107, 118, 123mulne0d 10264 . . . . . . 7
12592, 108, 117, 124mulne0d 10264 . . . . . 6
12611, 13, 109, 13, 32, 32, 125divdivdivd 10430 . . . . 5
12711, 13mulcomd 9664 . . . . . 6
128127oveq1d 6316 . . . . 5
12911mulid1d 9660 . . . . . . . . . 10
130129eqcomd 2430 . . . . . . . . 9
131130oveq1d 6316 . . . . . . . 8
13211, 92, 11, 108, 117, 124divmuldivd 10424 . . . . . . . 8
133131, 132eqtr4d 2466 . . . . . . 7
13468, 133oveq12d 6319 . . . . . 6
13513, 13, 11, 109, 32, 125divmuldivd 10424 . . . . . 6
13692, 117reccld 10376 . . . . . . . 8
137108, 124reccld 10376 . . . . . . . 8
138136, 137mulcld 9663 . . . . . . 7
139138mulid2d 9661 . . . . . 6
140134, 135, 1393eqtr3d 2471 . . . . 5
141126, 128, 1403eqtrd 2467 . . . 4
142114, 141eqtrd 2463 . . 3
14366, 142breqtrd 4445 . 2
14459biimpi 197 . . . 4
1466a1i 11 . . . . . 6
147 oveq2 6309 . . . . . . . . . 10
148147oveq1d 6316 . . . . . . . . 9
149148oveq2d 6317 . . . . . . . 8
150147oveq2d 6317 . . . . . . . 8
151149, 150oveq12d 6319 . . . . . . 7
152151adantl 467 . . . . . 6
153 elfznn 11828 . . . . . . 7
154153adantl 467 . . . . . 6
155 2cnd 10682 . . . . . . . . . 10
156154nncnd 10625 . . . . . . . . . 10
157155, 156mulcld 9663 . . . . . . . . 9
158 1cnd 9659 . . . . . . . . 9
159157, 158addcld 9662 . . . . . . . 8
160 0red 9644 . . . . . . . . . . . 12
161 1red 9658 . . . . . . . . . . . 12
16216a1i 11 . . . . . . . . . . . . . 14
163 nnre 10616 . . . . . . . . . . . . . 14
164162, 163remulcld 9671 . . . . . . . . . . . . 13
165164, 161readdcld 9670 . . . . . . . . . . . 12
16621a1i 11 . . . . . . . . . . . 12
16723a1i 11 . . . . . . . . . . . . . 14
168 nnrp 11311 . . . . . . . . . . . . . 14
169167, 168rpmulcld 11357 . . . . . . . . . . . . 13
170161, 169ltaddrp2d 11372 . . . . . . . . . . . 12
171160, 161, 165, 166, 170lttrd 9796 . . . . . . . . . . 11
172153, 171syl 17 . . . . . . . . . 10
173172gt0ne0d 10178 . . . . . . . . 9
174173adantl 467 . . . . . . . 8
175159, 174reccld 10376 . . . . . . 7
1769adantr 466 . . . . . . . . . . 11
177155, 176mulcld 9663 . . . . . . . . . 10
178177, 158addcld 9662 . . . . . . . . 9
17929adantr 466 . . . . . . . . 9
180178, 179reccld 10376 . . . . . . . 8
181 2nn0 10886 . . . . . . . . . 10
182181a1i 11 . . . . . . . . 9
183154nnnn0d 10925 . . . . . . . . 9
184182, 183nn0mulcld 10930 . . . . . . . 8
185180, 184expcld 12415 . . . . . . 7
186175, 185mulcld 9663 . . . . . 6
187146, 152, 154, 186fvmptd 5966 . . . . 5
188187adantlr 719 . . . 4
189171gt0ne0d 10178 . . . . . . . 8
190165, 189rereccld 10434 . . . . . . 7
191153, 190syl 17 . . . . . 6
192191adantl 467 . . . . 5
19320, 29rereccld 10434 . . . . . . . 8
194193adantr 466 . . . . . . 7
195194, 184reexpcld 12432 . . . . . 6
196195adantlr 719 . . . . 5
197192, 196remulcld 9671 . . . 4
198188, 197eqeltrd 2510 . . 3
199 readdcl 9622 . . . 4
201145, 198, 200seqcl 12232 . 2
20255a1i 11 . . . . . 6
203 oveq2 6309 . . . . . . 7
204203adantl 467 . . . . . 6
20533adantr 466 . . . . . . 7
206205, 183expcld 12415 . . . . . 6
207202, 204, 154, 206fvmptd 5966 . . . . 5
20836adantr 466 . . . . . 6
209208, 183reexpcld 12432 . . . . 5
210207, 209eqeltrd 2510 . . . 4
212145, 211, 200seqcl 12232 . 2
21330a1i 11 . . . . . . . . . . . . 13
214 elfzelz 11800 . . . . . . . . . . . . 13
215213, 214zmulcld 11046 . . . . . . . . . . . 12
216 1exp 12300 . . . . . . . . . . . 12
217215, 216syl 17 . . . . . . . . . . 11
218 1exp 12300 . . . . . . . . . . . 12
219214, 218syl 17 . . . . . . . . . . 11
220217, 219eqtr4d 2466 . . . . . . . . . 10
221220adantl 467 . . . . . . . . 9
222178, 183, 182expmuld 12418 . . . . . . . . 9
223221, 222oveq12d 6319 . . . . . . . 8
224158, 178, 179, 184expdivd 12429 . . . . . . . 8
225178sqcld 12413 . . . . . . . . 9
22630a1i 11 . . . . . . . . . 10
227178, 179, 226expne0d 12421 . . . . . . . . 9
228158, 225, 227, 183expdivd 12429 . . . . . . . 8
229223, 224, 2283eqtr4d 2473 . . . . . . 7
230229oveq2d 6317 . . . . . 6
231 1rp 11306 . . . . . . . . . . 11
232231a1i 11 . . . . . . . . . 10
23316a1i 11 . . . . . . . . . . . 12
234154nnred 10624 . . . . . . . . . . . 12
235233, 234remulcld 9671 . . . . . . . . . . 11
236182nn0ge0d 10928 . . . . . . . . . . . 12
237183nn0ge0d 10928 . . . . . . . . . . . 12
238233, 234, 236, 237mulge0d 10190 . . . . . . . . . . 11
239235, 238ge0p1rpd 11368 . . . . . . . . . 10
240 1red 9658 . . . . . . . . . 10
241232rpge0d 11345 . . . . . . . . . 10
242161, 165, 170ltled 9783 . . . . . . . . . . . 12
243153, 242syl 17 . . . . . . . . . . 11
244243adantl 467 . . . . . . . . . 10
245232, 239, 240, 241, 244lediv2ad 11363 . . . . . . . . 9
246158div1d 10375 . . . . . . . . 9
247245, 246breqtrd 4445 . . . . . . . 8
248154, 190syl 17 . . . . . . . . 9
24918adantr 466 . . . . . . . . . . . . . 14
250233, 249remulcld 9671 . . . . . . . . . . . . 13
25114, 18, 120ltled 9783 . . . . . . . . . . . . . . 15
252251adantr 466 . . . . . . . . . . . . . 14
253233, 249, 236, 252mulge0d 10190 . . . . . . . . . . . . 13
254250, 253ge0p1rpd 11368 . . . . . . . . . . . 12
255254, 226rpexpcld 12438 . . . . . . . . . . 11
256255rpreccld 11351 . . . . . . . . . 10
257214adantl 467 . . . . . . . . . 10
258256, 257rpexpcld 12438 . . . . . . . . 9
259248, 240, 258lemul1d 11381 . . . . . . . 8
260247, 259mpbid 213 . . . . . . 7
261206mulid2d 9661 . . . . . . 7
262260, 261breqtrd 4445 . . . . . 6
263230, 262eqbrtrd 4441 . . . . 5
264263, 187, 2073brtr4d 4451 . . . 4