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

Theorem stirlinglem10 27808
 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 10521 . 2
2 1nn0 10237 . . . 4
32a1i 11 . . 3
43nn0zd 10373 . 2
5 stirlinglem10.1 . . 3
6 stirlinglem10.2 . . 3
7 eqid 2436 . . 3
8 stirlinglem10.4 . . 3
95, 6, 7, 8stirlinglem9 27807 . 2
10 2cn 10070 . . . . . . . . 9
1110a1i 11 . . . . . . . 8
12 nncn 10008 . . . . . . . 8
1311, 12mulcld 9108 . . . . . . 7
14 ax-1cn 9048 . . . . . . . 8
1514a1i 11 . . . . . . 7
1613, 15addcld 9107 . . . . . 6
1716sqcld 11521 . . . . 5
18 0re 9091 . . . . . . . . 9
1918a1i 11 . . . . . . . 8
20 1re 9090 . . . . . . . . 9
2120a1i 11 . . . . . . . 8
22 2re 10069 . . . . . . . . . . 11
2322a1i 11 . . . . . . . . . 10
24 nnre 10007 . . . . . . . . . 10
2523, 24remulcld 9116 . . . . . . . . 9
2625, 21readdcld 9115 . . . . . . . 8
27 0lt1 9550 . . . . . . . . 9
2827a1i 11 . . . . . . . 8
29 2rp 10617 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
31 nnrp 10621 . . . . . . . . . 10
3230, 31rpmulcld 10664 . . . . . . . . 9
3321, 32ltaddrp2d 10678 . . . . . . . 8
3419, 21, 26, 28, 33lttrd 9231 . . . . . . 7
3534gt0ne0d 9591 . . . . . 6
36 2z 10312 . . . . . . 7
3736a1i 11 . . . . . 6
3816, 35, 37expne0d 11529 . . . . 5
3917, 38reccld 9783 . . . 4
4021renegcld 9464 . . . . . 6
4126resqcld 11549 . . . . . . 7
4241, 38rereccld 9841 . . . . . 6
43 lt0neg2 9535 . . . . . . . 8
4420, 43ax-mp 8 . . . . . . 7
4528, 44sylib 189 . . . . . 6
4626, 35sqgt0d 11551 . . . . . . 7
4741, 46recgt0d 9945 . . . . . 6
4840, 19, 42, 45, 47lttrd 9231 . . . . 5
49 2nn 10133 . . . . . . . 8
5049a1i 11 . . . . . . 7
51 expgt1 11418 . . . . . . 7
5226, 50, 33, 51syl3anc 1184 . . . . . 6
5341, 46elrpd 10646 . . . . . . 7
5453recgt1d 10662 . . . . . 6
5552, 54mpbid 202 . . . . 5
5642, 21absltd 12232 . . . . 5
5748, 55, 56mpbir2and 889 . . . 4
58 stirlinglem10.5 . . . . . 6
5958a1i 11 . . . . 5
60 simpr 448 . . . . . 6
6160oveq2d 6097 . . . . 5
62 elnnuz 10522 . . . . . . 7
6362biimpri 198 . . . . . 6
6463adantl 453 . . . . 5
6539adantr 452 . . . . . 6
6664nnnn0d 10274 . . . . . 6
6765, 66expcld 11523 . . . . 5
6859, 61, 64, 67fvmptd 5810 . . . 4
6939, 57, 3, 68geolim2 12648 . . 3
7039exp1d 11518 . . . . 5
7117, 38dividd 9788 . . . . . . . 8
7271eqcomd 2441 . . . . . . 7
7372oveq1d 6096 . . . . . 6
7453rpcnne0d 10657 . . . . . . 7
75 divsubdir 9710 . . . . . . 7
7617, 15, 74, 75syl3anc 1184 . . . . . 6
77 binom2 11496 . . . . . . . . . 10
7813, 14, 77sylancl 644 . . . . . . . . 9
7978oveq1d 6096 . . . . . . . 8
8011, 12sqmuld 11535 . . . . . . . . . . . . 13
81 sq2 11477 . . . . . . . . . . . . . . 15
8281a1i 11 . . . . . . . . . . . . . 14
8382oveq1d 6096 . . . . . . . . . . . . 13
8480, 83eqtrd 2468 . . . . . . . . . . . 12
8513mulid1d 9105 . . . . . . . . . . . . . 14
8685oveq2d 6097 . . . . . . . . . . . . 13
8711, 11, 12mulassd 9111 . . . . . . . . . . . . 13
88 2t2e4 10127 . . . . . . . . . . . . . . 15
8988a1i 11 . . . . . . . . . . . . . 14
9089oveq1d 6096 . . . . . . . . . . . . 13
9186, 87, 903eqtr2d 2474 . . . . . . . . . . . 12
9284, 91oveq12d 6099 . . . . . . . . . . 11
93 4cn 10074 . . . . . . . . . . . . 13
9493a1i 11 . . . . . . . . . . . 12
9512sqcld 11521 . . . . . . . . . . . 12
9694, 95, 12adddid 9112 . . . . . . . . . . 11
9712sqvald 11520 . . . . . . . . . . . . . 14
9812mulid1d 9105 . . . . . . . . . . . . . . 15
9998eqcomd 2441 . . . . . . . . . . . . . 14
10097, 99oveq12d 6099 . . . . . . . . . . . . 13
10112, 12, 15adddid 9112 . . . . . . . . . . . . 13
102100, 101eqtr4d 2471 . . . . . . . . . . . 12
103102oveq2d 6097 . . . . . . . . . . 11
10492, 96, 1033eqtr2d 2474 . . . . . . . . . 10
105 sq1 11476 . . . . . . . . . . 11
106105a1i 11 . . . . . . . . . 10
107104, 106oveq12d 6099 . . . . . . . . 9
108107oveq1d 6096 . . . . . . . 8
10912, 15addcld 9107 . . . . . . . . . . 11
11012, 109mulcld 9108 . . . . . . . . . 10
11194, 110mulcld 9108 . . . . . . . . 9
112111, 15pncand 9412 . . . . . . . 8
11379, 108, 1123eqtrd 2472 . . . . . . 7
114113oveq1d 6096 . . . . . 6
11573, 76, 1143eqtr2d 2474 . . . . 5
11670, 115oveq12d 6099 . . . 4
117 4pos 10086 . . . . . . . . 9
118117a1i 11 . . . . . . . 8
119118gt0ne0d 9591 . . . . . . 7
120 nnne0 10032 . . . . . . . 8
12124, 21readdcld 9115 . . . . . . . . . 10
122 nngt0 10029 . . . . . . . . . 10
12324ltp1d 9941 . . . . . . . . . 10
12419, 24, 121, 122, 123lttrd 9231 . . . . . . . . 9
125124gt0ne0d 9591 . . . . . . . 8
12612, 109, 120, 125mulne0d 9674 . . . . . . 7
12794, 110, 119, 126mulne0d 9674 . . . . . 6
12815, 17, 111, 17, 38, 38, 127divdivdivd 9837 . . . . 5
12915, 17mulcomd 9109 . . . . . 6
130129oveq1d 6096 . . . . 5
13115mulid1d 9105 . . . . . . . . . 10
132131eqcomd 2441 . . . . . . . . 9
133132oveq1d 6096 . . . . . . . 8
13415, 94, 15, 110, 119, 126divmuldivd 9831 . . . . . . . 8
135133, 134eqtr4d 2471 . . . . . . 7
13671, 135oveq12d 6099 . . . . . 6
13717, 17, 15, 111, 38, 127divmuldivd 9831 . . . . . 6
13894, 119reccld 9783 . . . . . . . 8
139110, 126reccld 9783 . . . . . . . 8
140138, 139mulcld 9108 . . . . . . 7
141140mulid2d 9106 . . . . . 6
142136, 137, 1413eqtr3d 2476 . . . . 5
143128, 130, 1423eqtrd 2472 . . . 4
144116, 143eqtrd 2468 . . 3
14569, 144breqtrd 4236 . 2
14662biimpi 187 . . . 4
1488a1i 11 . . . . . 6
149 oveq2 6089 . . . . . . . . . 10
150149oveq1d 6096 . . . . . . . . 9
151150oveq2d 6097 . . . . . . . 8
152149oveq2d 6097 . . . . . . . 8
153151, 152oveq12d 6099 . . . . . . 7
154153adantl 453 . . . . . 6
155 elfznn 11080 . . . . . . 7
156155adantl 453 . . . . . 6
15710a1i 11 . . . . . . . . . 10
158156nncnd 10016 . . . . . . . . . 10
159157, 158mulcld 9108 . . . . . . . . 9
16014a1i 11 . . . . . . . . 9
161159, 160addcld 9107 . . . . . . . 8
16218a1i 11 . . . . . . . . . . . 12
16320a1i 11 . . . . . . . . . . . 12
16422a1i 11 . . . . . . . . . . . . . 14
165 nnre 10007 . . . . . . . . . . . . . 14
166164, 165remulcld 9116 . . . . . . . . . . . . 13
167166, 163readdcld 9115 . . . . . . . . . . . 12
16827a1i 11 . . . . . . . . . . . 12
16929a1i 11 . . . . . . . . . . . . . 14
170 nnrp 10621 . . . . . . . . . . . . . 14
171169, 170rpmulcld 10664 . . . . . . . . . . . . 13
172163, 171ltaddrp2d 10678 . . . . . . . . . . . 12
173162, 163, 167, 168, 172lttrd 9231 . . . . . . . . . . 11
174155, 173syl 16 . . . . . . . . . 10
175174gt0ne0d 9591 . . . . . . . . 9
176175adantl 453 . . . . . . . 8
177161, 176reccld 9783 . . . . . . 7
17812adantr 452 . . . . . . . . . . 11
179157, 178mulcld 9108 . . . . . . . . . 10
180179, 160addcld 9107 . . . . . . . . 9
18135adantr 452 . . . . . . . . 9
182180, 181reccld 9783 . . . . . . . 8
183 2nn0 10238 . . . . . . . . . 10
184183a1i 11 . . . . . . . . 9
185156nnnn0d 10274 . . . . . . . . 9
186184, 185nn0mulcld 10279 . . . . . . . 8
187182, 186expcld 11523 . . . . . . 7
188177, 187mulcld 9108 . . . . . 6
189148, 154, 156, 188fvmptd 5810 . . . . 5
190189adantlr 696 . . . 4
191173gt0ne0d 9591 . . . . . . . 8
192167, 191rereccld 9841 . . . . . . 7
193155, 192syl 16 . . . . . 6
194193adantl 453 . . . . 5
19526, 35rereccld 9841 . . . . . . . 8
196195adantr 452 . . . . . . 7
197196, 186reexpcld 11540 . . . . . 6
198197adantlr 696 . . . . 5
199194, 198remulcld 9116 . . . 4
200190, 199eqeltrd 2510 . . 3
201 readdcl 9073 . . . 4
203147, 200, 202seqcl 11343 . 2
20458a1i 11 . . . . . 6
205 oveq2 6089 . . . . . . 7
206205adantl 453 . . . . . 6
20739adantr 452 . . . . . . 7
208207, 185expcld 11523 . . . . . 6
209204, 206, 156, 208fvmptd 5810 . . . . 5
21042adantr 452 . . . . . 6
211210, 185reexpcld 11540 . . . . 5
212209, 211eqeltrd 2510 . . . 4
214147, 213, 202seqcl 11343 . 2
21536a1i 11 . . . . . . . . . . . . 13
216 elfzelz 11059 . . . . . . . . . . . . 13
217215, 216zmulcld 10381 . . . . . . . . . . . 12
218 1exp 11409 . . . . . . . . . . . 12
219217, 218syl 16 . . . . . . . . . . 11
220 1exp 11409 . . . . . . . . . . . 12
221216, 220syl 16 . . . . . . . . . . 11
222219, 221eqtr4d 2471 . . . . . . . . . 10
223222adantl 453 . . . . . . . . 9
224180, 185, 184expmuld 11526 . . . . . . . . 9
225223, 224oveq12d 6099 . . . . . . . 8
226160, 180, 181, 186expdivd 11537 . . . . . . . 8
227180sqcld 11521 . . . . . . . . 9
22836a1i 11 . . . . . . . . . 10
229180, 181, 228expne0d 11529 . . . . . . . . 9
230160, 227, 229, 185expdivd 11537 . . . . . . . 8
231225, 226, 2303eqtr4d 2478 . . . . . . 7
232231oveq2d 6097 . . . . . 6
233 1rp 10616 . . . . . . . . . . 11
234233a1i 11 . . . . . . . . . 10
23522a1i 11 . . . . . . . . . . . 12
236156nnred 10015 . . . . . . . . . . . 12
237235, 236remulcld 9116 . . . . . . . . . . 11
238184nn0ge0d 10277 . . . . . . . . . . . 12
239185nn0ge0d 10277 . . . . . . . . . . . 12
240235, 236, 238, 239mulge0d 9603 . . . . . . . . . . 11
241237, 240ge0p1rpd 10674 . . . . . . . . . 10
24220a1i 11 . . . . . . . . . 10
243234rpge0d 10652 . . . . . . . . . 10
244163, 167, 172ltled 9221 . . . . . . . . . . . 12
245155, 244syl 16 . . . . . . . . . . 11
246245adantl 453 . . . . . . . . . 10
247234, 241, 242, 243, 246lediv2ad 10670 . . . . . . . . 9
248160div1d 9782 . . . . . . . . 9
249247, 248breqtrd 4236 . . . . . . . 8
250156, 192syl 16 . . . . . . . . 9
25124adantr 452 . . . . . . . . . . . . . 14
252235, 251remulcld 9116 . . . . . . . . . . . . 13
25319, 24, 122ltled 9221 . . . . . . . . . . . . . . 15
254253adantr 452 . . . . . . . . . . . . . 14
255235, 251, 238, 254mulge0d 9603 . . . . . . . . . . . . 13
256252, 255ge0p1rpd 10674 . . . . . . . . . . . 12
257256, 228rpexpcld 11546 . . . . . . . . . . 11
258257rpreccld 10658 . . . . . . . . . 10
259216adantl 453 . . . . . . . . . 10
260258, 259rpexpcld 11546 . . . . . . . . 9
261250, 242, 260lemul1d 10687 . . . . . . . 8
262249, 261mpbid 202 . . . . . . 7
263208mulid2d 9106 . . . . . . 7
264262, 263breqtrd 4236 . . . . . 6
265232, 264eqbrtrd 4232 . . . . 5
266265, 189, 2093brtr4d 4242 . . . 4