Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rge0scvg Structured version   Unicode version

Theorem rge0scvg 28707
 Description: Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 14808. (Contributed by Thierry Arnoux, 28-Jul-2017.)
Assertion
Ref Expression
rge0scvg

Proof of Theorem rge0scvg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11145 . . . . 5
2 1zzd 10919 . . . . 5
3 rge0ssre 11691 . . . . . . 7
4 fss 5697 . . . . . . 7
53, 4mpan2 675 . . . . . 6
65ffvelrnda 5981 . . . . 5
71, 2, 6serfre 12192 . . . 4
8 frn 5695 . . . 4
97, 8syl 17 . . 3
11 1nn 10571 . . . . 5
12 fdm 5693 . . . . 5
1311, 12syl5eleqr 2513 . . . 4
14 ne0i 3710 . . . . 5
15 dm0rn0 5013 . . . . . 6
1615necon3bii 2653 . . . . 5
1714, 16sylib 199 . . . 4
187, 13, 173syl 18 . . 3
20 1zzd 10919 . . . . 5
21 climdm 13561 . . . . . . 7
2221biimpi 197 . . . . . 6
2322adantl 467 . . . . 5
247adantr 466 . . . . . 6
2524ffvelrnda 5981 . . . . 5
261, 20, 23, 25climrecl 13590 . . . 4
27 simpr 462 . . . . . 6
2823adantr 466 . . . . . 6
29 simplll 766 . . . . . . 7
30 ffvelrn 5979 . . . . . . . 8
313, 30sseldi 3405 . . . . . . 7
3229, 31sylancom 671 . . . . . 6
33 elrege0 11689 . . . . . . . . . 10
3433simprbi 465 . . . . . . . . 9
3530, 34syl 17 . . . . . . . 8
3635adantlr 719 . . . . . . 7
3736adantlr 719 . . . . . 6
381, 27, 28, 32, 37climserle 13669 . . . . 5
3938ralrimiva 2779 . . . 4
40 breq2 4370 . . . . . 6
4140ralbidv 2804 . . . . 5
4241rspcev 3125 . . . 4
4326, 39, 42syl2anc 665 . . 3
44 ffn 5689 . . . . . 6
45 breq1 4369 . . . . . . 7
4645ralrn 5984 . . . . . 6
477, 44, 463syl 18 . . . . 5
4847rexbidv 2878 . . . 4