Metamath Proof Explorer


Theorem rge0scvg

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

Ref Expression
Assertion rge0scvg F : 0 +∞ seq 1 + F dom sup ran seq 1 + F <

Proof

Step Hyp Ref Expression
1 nnuz = 1
2 1zzd F : 0 +∞ 1
3 rge0ssre 0 +∞
4 fss F : 0 +∞ 0 +∞ F :
5 3 4 mpan2 F : 0 +∞ F :
6 5 ffvelrnda F : 0 +∞ j F j
7 1 2 6 serfre F : 0 +∞ seq 1 + F :
8 7 frnd F : 0 +∞ ran seq 1 + F
9 8 adantr F : 0 +∞ seq 1 + F dom ran seq 1 + F
10 1nn 1
11 fdm seq 1 + F : dom seq 1 + F =
12 10 11 eleqtrrid seq 1 + F : 1 dom seq 1 + F
13 ne0i 1 dom seq 1 + F dom seq 1 + F
14 dm0rn0 dom seq 1 + F = ran seq 1 + F =
15 14 necon3bii dom seq 1 + F ran seq 1 + F
16 13 15 sylib 1 dom seq 1 + F ran seq 1 + F
17 7 12 16 3syl F : 0 +∞ ran seq 1 + F
18 17 adantr F : 0 +∞ seq 1 + F dom ran seq 1 + F
19 1zzd F : 0 +∞ seq 1 + F dom 1
20 climdm seq 1 + F dom seq 1 + F seq 1 + F
21 20 biimpi seq 1 + F dom seq 1 + F seq 1 + F
22 21 adantl F : 0 +∞ seq 1 + F dom seq 1 + F seq 1 + F
23 7 adantr F : 0 +∞ seq 1 + F dom seq 1 + F :
24 23 ffvelrnda F : 0 +∞ seq 1 + F dom k seq 1 + F k
25 1 19 22 24 climrecl F : 0 +∞ seq 1 + F dom seq 1 + F
26 simpr F : 0 +∞ seq 1 + F dom k k
27 22 adantr F : 0 +∞ seq 1 + F dom k seq 1 + F seq 1 + F
28 simplll F : 0 +∞ seq 1 + F dom k j F : 0 +∞
29 ffvelrn F : 0 +∞ j F j 0 +∞
30 3 29 sseldi F : 0 +∞ j F j
31 28 30 sylancom F : 0 +∞ seq 1 + F dom k j F j
32 elrege0 F j 0 +∞ F j 0 F j
33 32 simprbi F j 0 +∞ 0 F j
34 29 33 syl F : 0 +∞ j 0 F j
35 34 adantlr F : 0 +∞ seq 1 + F dom j 0 F j
36 35 adantlr F : 0 +∞ seq 1 + F dom k j 0 F j
37 1 26 27 31 36 climserle F : 0 +∞ seq 1 + F dom k seq 1 + F k seq 1 + F
38 37 ralrimiva F : 0 +∞ seq 1 + F dom k seq 1 + F k seq 1 + F
39 brralrspcev seq 1 + F k seq 1 + F k seq 1 + F x k seq 1 + F k x
40 25 38 39 syl2anc F : 0 +∞ seq 1 + F dom x k seq 1 + F k x
41 ffn seq 1 + F : seq 1 + F Fn
42 breq1 z = seq 1 + F k z x seq 1 + F k x
43 42 ralrn seq 1 + F Fn z ran seq 1 + F z x k seq 1 + F k x
44 7 41 43 3syl F : 0 +∞ z ran seq 1 + F z x k seq 1 + F k x
45 44 rexbidv F : 0 +∞ x z ran seq 1 + F z x x k seq 1 + F k x
46 45 adantr F : 0 +∞ seq 1 + F dom x z ran seq 1 + F z x x k seq 1 + F k x
47 40 46 mpbird F : 0 +∞ seq 1 + F dom x z ran seq 1 + F z x
48 suprcl ran seq 1 + F ran seq 1 + F x z ran seq 1 + F z x sup ran seq 1 + F <
49 9 18 47 48 syl3anc F : 0 +∞ seq 1 + F dom sup ran seq 1 + F <