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

Theorem stirlinglem10 27832
 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 10263 . 2
2 1nn0 9981 . . . 4
32a1i 10 . . 3
43nn0zd 10115 . 2
5 stirlinglem10.1 . . 3
6 stirlinglem10.2 . . 3
7 eqid 2283 . . 3
8 stirlinglem10.4 . . 3
95, 6, 7, 8stirlinglem9 27831 . 2
10 2cn 9816 . . . . . . . . 9
1110a1i 10 . . . . . . . 8
12 nncn 9754 . . . . . . . 8
1311, 12mulcld 8855 . . . . . . 7
14 ax-1cn 8795 . . . . . . . 8
1514a1i 10 . . . . . . 7
1613, 15addcld 8854 . . . . . 6
1716sqcld 11243 . . . . 5
18 0re 8838 . . . . . . . 8
1918a1i 10 . . . . . . 7
20 1re 8837 . . . . . . . . 9
2120a1i 10 . . . . . . . 8
22 2re 9815 . . . . . . . . . . 11
2322a1i 10 . . . . . . . . . 10
24 nnre 9753 . . . . . . . . . 10
2523, 24remulcld 8863 . . . . . . . . 9
2625, 21readdcld 8862 . . . . . . . 8
27 0lt1 9296 . . . . . . . . 9
2827a1i 10 . . . . . . . 8
29 2rp 10359 . . . . . . . . . . 11
3029a1i 10 . . . . . . . . . 10
31 nnrp 10363 . . . . . . . . . 10
3230, 31rpmulcld 10406 . . . . . . . . 9
3321, 32ltaddrp2d 10420 . . . . . . . 8
3419, 21, 26, 28, 33lttrd 8977 . . . . . . 7
3519, 34gtned 8954 . . . . . 6
36 2z 10054 . . . . . . 7
3736a1i 10 . . . . . 6
3816, 35, 37expne0d 11251 . . . . 5
3917, 38reccld 9529 . . . 4
4021renegcld 9210 . . . . . . 7
4126, 35, 37reexpclzd 11270 . . . . . . . 8
4221, 41, 38redivcld 9588 . . . . . . 7
43 lt0neg2 9281 . . . . . . . . 9
4420, 43ax-mp 8 . . . . . . . 8
4528, 44sylib 188 . . . . . . 7
4626, 35sqgt0d 11273 . . . . . . . 8
4741, 46recgt0d 9691 . . . . . . 7
4840, 19, 42, 45, 47lttrd 8977 . . . . . 6
49 2nn 9877 . . . . . . . . . 10
5049a1i 10 . . . . . . . . 9
5126, 50, 333jca 1132 . . . . . . . 8
52 expgt1 11140 . . . . . . . 8
5351, 52syl 15 . . . . . . 7
5441, 46elrpd 10388 . . . . . . . 8
5554recgt1d 10404 . . . . . . 7
5653, 55mpbid 201 . . . . . 6
5748, 56jca 518 . . . . 5
5842, 21absltd 11912 . . . . 5
5957, 58mpbird 223 . . . 4
60 stirlinglem10.5 . . . . . 6
6160a1i 10 . . . . 5
62 simpr 447 . . . . . 6
6362oveq2d 5874 . . . . 5
64 elnnuz 10264 . . . . . . 7
6564biimpri 197 . . . . . 6
6665adantl 452 . . . . 5
6739adantr 451 . . . . . 6
6866nnnn0d 10018 . . . . . 6
6967, 68expcld 11245 . . . . 5
7061, 63, 66, 69fvmptd 5606 . . . 4
7139, 59, 3, 70geolim2 12327 . . 3
7239exp1d 11240 . . . . 5
7317, 38dividd 9534 . . . . . . . 8
7473eqcomd 2288 . . . . . . 7
7574oveq1d 5873 . . . . . 6
7654rpcnne0d 10399 . . . . . . . . 9
7717, 15, 763jca 1132 . . . . . . . 8
78 divsubdir 9456 . . . . . . . 8
7977, 78syl 15 . . . . . . 7
8079eqcomd 2288 . . . . . 6
8113, 15jca 518 . . . . . . . . . 10
82 binom2 11218 . . . . . . . . . 10
8381, 82syl 15 . . . . . . . . 9
8483oveq1d 5873 . . . . . . . 8
8550nnnn0d 10018 . . . . . . . . . . . . . 14
8611, 12, 85mulexpd 11260 . . . . . . . . . . . . 13
87 sq2 11199 . . . . . . . . . . . . . . 15
8887a1i 10 . . . . . . . . . . . . . 14
8988oveq1d 5873 . . . . . . . . . . . . 13
9086, 89eqtrd 2315 . . . . . . . . . . . 12
9113mulid1d 8852 . . . . . . . . . . . . . 14
9291oveq2d 5874 . . . . . . . . . . . . 13
9311, 11, 12mulassd 8858 . . . . . . . . . . . . . 14
9493eqcomd 2288 . . . . . . . . . . . . 13
95 2t2e4 9871 . . . . . . . . . . . . . . 15
9695a1i 10 . . . . . . . . . . . . . 14
9796oveq1d 5873 . . . . . . . . . . . . 13
9892, 94, 973eqtrd 2319 . . . . . . . . . . . 12
9990, 98oveq12d 5876 . . . . . . . . . . 11
100 4cn 9820 . . . . . . . . . . . . . 14
101100a1i 10 . . . . . . . . . . . . 13
10212sqcld 11243 . . . . . . . . . . . . 13
103101, 102, 12adddid 8859 . . . . . . . . . . . 12
104103eqcomd 2288 . . . . . . . . . . 11
10512sqvald 11242 . . . . . . . . . . . . . 14
10612mulid1d 8852 . . . . . . . . . . . . . . 15
107106eqcomd 2288 . . . . . . . . . . . . . 14
108105, 107oveq12d 5876 . . . . . . . . . . . . 13
10912, 12, 15adddid 8859 . . . . . . . . . . . . . 14
110109eqcomd 2288 . . . . . . . . . . . . 13
111108, 110eqtrd 2315 . . . . . . . . . . . 12
112111oveq2d 5874 . . . . . . . . . . 11
11399, 104, 1123eqtrd 2319 . . . . . . . . . 10
114 sq1 11198 . . . . . . . . . . 11
115114a1i 10 . . . . . . . . . 10
116113, 115oveq12d 5876 . . . . . . . . 9
117116oveq1d 5873 . . . . . . . 8
11812, 15addcld 8854 . . . . . . . . . . 11
11912, 118mulcld 8855 . . . . . . . . . 10
120101, 119mulcld 8855 . . . . . . . . 9
121120, 15pncand 9158 . . . . . . . 8
12284, 117, 1213eqtrd 2319 . . . . . . 7
123122oveq1d 5873 . . . . . 6
12475, 80, 1233eqtrd 2319 . . . . 5
12572, 124oveq12d 5876 . . . 4
126 4pos 9832 . . . . . . . . 9
127126a1i 10 . . . . . . . 8
12819, 127gtned 8954 . . . . . . 7
129 nnne0 9778 . . . . . . . 8
13024, 21readdcld 8862 . . . . . . . . . 10
131 nngt0 9775 . . . . . . . . . 10
13224ltp1d 9687 . . . . . . . . . 10
13319, 24, 130, 131, 132lttrd 8977 . . . . . . . . 9
13419, 133gtned 8954 . . . . . . . 8
13512, 118, 129, 134mulne0d 9420 . . . . . . 7
136101, 119, 128, 135mulne0d 9420 . . . . . 6
13715, 17, 120, 17, 38, 38, 136divdivdivd 9583 . . . . 5
13815, 17mulcomd 8856 . . . . . 6
139138oveq1d 5873 . . . . 5
14017, 17, 15, 120, 38, 136divmuldivd 9577 . . . . . . 7
141140eqcomd 2288 . . . . . 6
14215mulid1d 8852 . . . . . . . . . 10
143142eqcomd 2288 . . . . . . . . 9
144143oveq1d 5873 . . . . . . . 8
14515, 101, 15, 119, 128, 135divmuldivd 9577 . . . . . . . . 9
146145eqcomd 2288 . . . . . . . 8
147144, 146eqtrd 2315 . . . . . . 7
14873, 147oveq12d 5876 . . . . . 6
149101, 128reccld 9529 . . . . . . . 8
150119, 135reccld 9529 . . . . . . . 8
151149, 150mulcld 8855 . . . . . . 7
152151mulid2d 8853 . . . . . 6
153141, 148, 1523eqtrd 2319 . . . . 5
154137, 139, 1533eqtrd 2319 . . . 4
155125, 154eqtrd 2315 . . 3
15671, 155breqtrd 4047 . 2
15764biimpi 186 . . . 4
1598a1i 10 . . . . . 6
160 oveq2 5866 . . . . . . . . . 10
161160oveq1d 5873 . . . . . . . . 9
162161oveq2d 5874 . . . . . . . 8
163160oveq2d 5874 . . . . . . . 8
164162, 163oveq12d 5876 . . . . . . 7
165164adantl 452 . . . . . 6
166 elfznn 10819 . . . . . . 7
167166adantl 452 . . . . . 6
16810a1i 10 . . . . . . . . . 10
169167nncnd 9762 . . . . . . . . . 10
170168, 169mulcld 8855 . . . . . . . . 9
17114a1i 10 . . . . . . . . 9
172170, 171addcld 8854 . . . . . . . 8
17318a1i 10 . . . . . . . . . 10
17418a1i 10 . . . . . . . . . . . 12
17520a1i 10 . . . . . . . . . . . 12
17622a1i 10 . . . . . . . . . . . . . 14
177 nnre 9753 . . . . . . . . . . . . . 14
178176, 177remulcld 8863 . . . . . . . . . . . . 13
179178, 175readdcld 8862 . . . . . . . . . . . 12
18027a1i 10 . . . . . . . . . . . 12
18129a1i 10 . . . . . . . . . . . . . 14
182 nnrp 10363 . . . . . . . . . . . . . 14
183181, 182rpmulcld 10406 . . . . . . . . . . . . 13
184175, 183ltaddrp2d 10420 . . . . . . . . . . . 12
185174, 175, 179, 180, 184lttrd 8977 . . . . . . . . . . 11
186166, 185syl 15 . . . . . . . . . 10
187173, 186gtned 8954 . . . . . . . . 9
188187adantl 452 . . . . . . . 8
189172, 188reccld 9529 . . . . . . 7
19012adantr 451 . . . . . . . . . . 11
191168, 190mulcld 8855 . . . . . . . . . 10
192191, 171addcld 8854 . . . . . . . . 9
19335adantr 451 . . . . . . . . 9
194192, 193reccld 9529 . . . . . . . 8
195 2nn0 9982 . . . . . . . . . 10
196195a1i 10 . . . . . . . . 9
197167nnnn0d 10018 . . . . . . . . 9
198196, 197nn0mulcld 10023 . . . . . . . 8
199194, 198expcld 11245 . . . . . . 7
200189, 199mulcld 8855 . . . . . 6
201159, 165, 167, 200fvmptd 5606 . . . . 5
202201adantlr 695 . . . 4
203174, 185gtned 8954 . . . . . . . 8
204175, 179, 203redivcld 9588 . . . . . . 7
205166, 204syl 15 . . . . . 6
206205adantl 452 . . . . 5
20726, 35rereccld 9587 . . . . . . . 8
208207adantr 451 . . . . . . 7
209208, 198reexpcld 11262 . . . . . 6
210209adantlr 695 . . . . 5
211206, 210remulcld 8863 . . . 4
212202, 211eqeltrd 2357 . . 3
213 readdcl 8820 . . . 4
215158, 212, 214seqcl 11066 . 2
21660a1i 10 . . . . . 6
217 oveq2 5866 . . . . . . 7
218217adantl 452 . . . . . 6
21939adantr 451 . . . . . . 7
220219, 197expcld 11245 . . . . . 6
221216, 218, 167, 220fvmptd 5606 . . . . 5
22242adantr 451 . . . . . 6
223222, 197reexpcld 11262 . . . . 5
224221, 223eqeltrd 2357 . . . 4
226158, 225, 214seqcl 11066 . 2
227171, 192, 193, 198expdivd 11259 . . . . . . . 8
22836a1i 10 . . . . . . . . . . . . 13
229 elfzelz 10798 . . . . . . . . . . . . 13
230228, 229zmulcld 10123 . . . . . . . . . . . 12
231 1exp 11131 . . . . . . . . . . . 12
232230, 231syl 15 . . . . . . . . . . 11
233 1exp 11131 . . . . . . . . . . . . 13
234229, 233syl 15 . . . . . . . . . . . 12
235234eqcomd 2288 . . . . . . . . . . 11
236232, 235eqtrd 2315 . . . . . . . . . 10
237236adantl 452 . . . . . . . . 9
238192, 197, 196expmuld 11248 . . . . . . . . 9
239237, 238oveq12d 5876 . . . . . . . 8
240192sqcld 11243 . . . . . . . . . 10
24136a1i 10 . . . . . . . . . . 11
242192, 193, 241expne0d 11251 . . . . . . . . . 10
243171, 240, 242, 197expdivd 11259 . . . . . . . . 9
244243eqcomd 2288 . . . . . . . 8
245227, 239, 2443eqtrd 2319 . . . . . . 7
246245oveq2d 5874 . . . . . 6
247 1rp 10358 . . . . . . . . . . 11
248247a1i 10 . . . . . . . . . 10
24922a1i 10 . . . . . . . . . . . 12
250167, 177syl 15 . . . . . . . . . . . 12
251249, 250remulcld 8863 . . . . . . . . . . 11
252196nn0ge0d 10021 . . . . . . . . . . . 12
253197nn0ge0d 10021 . . . . . . . . . . . 12
254249, 250, 252, 253mulge0d 9349 . . . . . . . . . . 11
255251, 254ge0p1rpd 10416 . . . . . . . . . 10
25620a1i 10 . . . . . . . . . 10
257248rpge0d 10394 . . . . . . . . . 10
258175, 179, 184ltled 8967 . . . . . . . . . . . 12
259166, 258syl 15 . . . . . . . . . . 11
260259adantl 452 . . . . . . . . . 10
261248, 255, 256, 257, 260lediv2ad 10412 . . . . . . . . 9
262171div1d 9528 . . . . . . . . 9
263261, 262breqtrd 4047 . . . . . . . 8
264167, 204syl 15 . . . . . . . . 9
26524adantr 451 . . . . . . . . . . . . . 14
266249, 265remulcld 8863 . . . . . . . . . . . . 13
26719, 24, 131ltled 8967 . . . . . . . . . . . . . . 15
268267adantr 451 . . . . . . . . . . . . . 14
269249, 265, 252, 268mulge0d 9349 . . . . . . . . . . . . 13
270266, 269ge0p1rpd 10416 . . . . . . . . . . . 12
271270, 241rpexpcld 11268 . . . . . . . . . . 11
272271rpreccld 10400 . . . . . . . . . 10
273229adantl 452 . . . . . . . . . 10
274272, 273rpexpcld 11268 . . . . . . . . 9
275264, 256, 274lemul1d 10429 . . . . . . . 8
276263, 275mpbid 201 . . . . . . 7
277220mulid2d 8853 . . . . . . 7
278276, 277breqtrd 4047 . . . . . 6
279246, 278eqbrtrd 4043 . . . . 5
280279, 201, 2213brtr4d 4053 . . . 4