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 ffvelcdmda 
 |-  ( ( 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 bilani 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
22 7 adantr 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> seq 1 ( + , F ) : NN --> RR )
23 22 ffvelcdmda 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. RR )
24 1 19 21 23 climrecl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> ( ~~> ` seq 1 ( + , F ) ) e. RR )
25 simpr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> k e. NN )
26 21 adantr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
27 simplll 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> F : NN --> ( 0 [,) +oo ) )
28 ffvelcdm 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> ( F ` j ) e. ( 0 [,) +oo ) )
29 3 28 sselid 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> ( F ` j ) e. RR )
30 27 29 sylancom 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> ( F ` j ) e. RR )
31 elrege0 
 |-  ( ( F ` j ) e. ( 0 [,) +oo ) <-> ( ( F ` j ) e. RR /\ 0 <_ ( F ` j ) ) )
32 31 simprbi 
 |-  ( ( F ` j ) e. ( 0 [,) +oo ) -> 0 <_ ( F ` j ) )
33 28 32 syl 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
34 33 adantlr 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
35 34 adantlr 
 |-  ( ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) /\ j e. NN ) -> 0 <_ ( F ` j ) )
36 1 25 26 30 35 climserle 
 |-  ( ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
37 36 ralrimiva 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ ( ~~> ` seq 1 ( + , F ) ) )
38 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 )
39 24 37 38 syl2anc 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> E. x e. RR A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x )
40 ffn 
 |-  ( seq 1 ( + , F ) : NN --> RR -> seq 1 ( + , F ) Fn NN )
41 breq1 
 |-  ( z = ( seq 1 ( + , F ) ` k ) -> ( z <_ x <-> ( seq 1 ( + , F ) ` k ) <_ x ) )
42 41 ralrn 
 |-  ( seq 1 ( + , F ) Fn NN -> ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
43 7 40 42 3syl 
 |-  ( F : NN --> ( 0 [,) +oo ) -> ( A. z e. ran seq 1 ( + , F ) z <_ x <-> A. k e. NN ( seq 1 ( + , F ) ` k ) <_ x ) )
44 43 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 ) )
45 44 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 ) )
46 39 45 mpbird 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> E. x e. RR A. z e. ran seq 1 ( + , F ) z <_ x )
47 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 )
48 9 18 46 47 syl3anc 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ seq 1 ( + , F ) e. dom ~~> ) -> sup ( ran seq 1 ( + , F ) , RR , < ) e. RR )