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 : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> sup ( ran seq 1 ( + , F ) , RR , < ) e. RR )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1zzd 
 |-  ( F : NN --> ( 0 [,) +oo ) -> 1 e. ZZ )
3 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
4 fss 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : NN --> RR )
5 3 4 mpan2 
 |-  ( F : NN --> ( 0 [,) +oo ) -> F : NN --> RR )
6 5 ffvelrnda 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> ( F ` j ) e. RR )
7 1 2 6 serfre 
 |-  ( F : NN --> ( 0 [,) +oo ) -> seq 1 ( + , F ) : NN --> RR )
8 7 frnd 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , F ) C_ RR )
9 8 adantr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> ran seq 1 ( + , F ) C_ RR )
10 1nn 
 |-  1 e. NN
11 fdm 
 |-  ( seq 1 ( + , F ) : NN --> RR -> dom seq 1 ( + , F ) = NN )
12 10 11 eleqtrrid 
 |-  ( seq 1 ( + , F ) : NN --> RR -> 1 e. dom seq 1 ( + , F ) )
13 ne0i 
 |-  ( 1 e. 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 e. dom seq 1 ( + , F ) -> ran seq 1 ( + , F ) =/= (/) )
17 7 12 16 3syl 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , F ) =/= (/) )
18 17 adantr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> ran seq 1 ( + , F ) =/= (/) )
19 1zzd 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> 1 e. ZZ )
20 climdm 
 |-  ( seq 1 ( + , F ) e. dom ~~> <-> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
21 20 biimpi 
 |-  ( seq 1 ( + , F ) e. dom ~~> -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
22 21 adantl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
23 7 adantr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , F ) : NN --> RR )
24 23 ffvelrnda 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. RR )
25 1 19 22 24 climrecl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> ( ~~> ` seq 1 ( + , F ) ) e. RR )
26 simpr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> k e. NN )
27 22 adantr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
28 simplll 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> F : NN --> ( 0 [,) +oo ) )
29 ffvelrn 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> ( F ` j ) e. ( 0 [,) +oo ) )
30 3 29 sselid 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> ( F ` j ) e. RR )
31 28 30 sylancom 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> ( F ` j ) e. RR )
32 elrege0 
 |-  ( ( F ` j ) e. ( 0 [,) +oo ) <-> ( ( F ` j ) e. RR /\ 0 <_ ( F ` j ) ) )
33 32 simprbi 
 |-  ( ( F ` j ) e. ( 0 [,) +oo ) -> 0 <_ ( F ` j ) )
34 29 33 syl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
35 34 adantlr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
36 35 adantlr 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
37 1 26 27 31 36 climserle 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
38 37 ralrimiva 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
39 brralrspcev 
 |-  ( ( ( ~~> ` seq 1 ( + , F ) ) e. RR /\ A. k e. NN ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) ) -> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
40 25 38 39 syl2anc 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
41 ffn 
 |-  ( seq 1 ( + , F ) : NN --> RR -> seq 1 ( + , F ) Fn NN )
42 breq1 
 |-  ( z = ( seq 1 ( + , F ) ` k ) -> ( z <_ x <-> ( seq 1 ( + , F ) ` k ) <_ x ) )
43 42 ralrn 
 |-  ( seq 1 ( + , F ) Fn NN -> ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
44 7 41 43 3syl 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
45 44 rexbidv 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ( E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x <-> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
46 45 adantr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> ( E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x <-> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
47 40 46 mpbird 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x )
48 suprcl 
 |-  ( ( ran seq 1 ( + , F ) C_ RR /\ ran seq 1 ( + , F ) =/= (/) /\ E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x ) -> sup ( ran seq 1 ( + , F ) , RR , < ) e. RR )
49 9 18 47 48 syl3anc 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> sup ( ran seq 1 ( + , F ) , RR , < ) e. RR )