Metamath Proof Explorer

Theorem isumsup2

Description: An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses isumsup.1 
|- Z = ( ZZ>= ` M )
isumsup.2 
|- G = seq M ( + , F )
isumsup.3 
|- ( ph -> M e. ZZ )
isumsup.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
isumsup.5 
|- ( ( ph /\ k e. Z ) -> A e. RR )
isumsup.6 
|- ( ( ph /\ k e. Z ) -> 0 <_ A )
isumsup.7 
|- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )
Assertion isumsup2 
|- ( ph -> G ~~> sup ( ran G , RR , < ) )

Proof

Step Hyp Ref Expression
1 isumsup.1 
 |-  Z = ( ZZ>= ` M )
2 isumsup.2 
 |-  G = seq M ( + , F )
3 isumsup.3 
 |-  ( ph -> M e. ZZ )
4 isumsup.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5 isumsup.5 
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
6 isumsup.6 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ A )
7 isumsup.7 
 |-  ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )
8 4 5 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
9 1 3 8 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
10 2 feq1i 
 |-  ( G : Z --> RR <-> seq M ( + , F ) : Z --> RR )
11 9 10 sylibr 
 |-  ( ph -> G : Z --> RR )
12 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
13 12 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
14 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
15 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
16 peano2uz 
 |-  ( j e. ( ZZ>= ` j ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
17 13 14 15 16 4syl 
 |-  ( ( ph /\ j e. Z ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
18 simpl 
 |-  ( ( ph /\ j e. Z ) -> ph )
19 elfzuz 
 |-  ( k e. ( M ... ( j + 1 ) ) -> k e. ( ZZ>= ` M ) )
20 19 1 eleqtrrdi 
 |-  ( k e. ( M ... ( j + 1 ) ) -> k e. Z )
21 18 20 8 syl2an 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... ( j + 1 ) ) ) -> ( F ` k ) e. RR )
22 1 peano2uzs 
 |-  ( j e. Z -> ( j + 1 ) e. Z )
23 22 adantl 
 |-  ( ( ph /\ j e. Z ) -> ( j + 1 ) e. Z )
24 elfzuz 
 |-  ( k e. ( ( j + 1 ) ... ( j + 1 ) ) -> k e. ( ZZ>= ` ( j + 1 ) ) )
25 1 uztrn2 
 |-  ( ( ( j + 1 ) e. Z /\ k e. ( ZZ>= ` ( j + 1 ) ) ) -> k e. Z )
26 23 24 25 syl2an 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> k e. Z )
27 6 4 breqtrrd 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
28 27 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. Z ) -> 0 <_ ( F ` k ) )
29 26 28 syldan 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ( j + 1 ) ... ( j + 1 ) ) ) -> 0 <_ ( F ` k ) )
30 13 17 21 29 sermono 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( seq M ( + , F ) ` ( j + 1 ) ) )
31 2 fveq1i 
 |-  ( G ` j ) = ( seq M ( + , F ) ` j )
32 2 fveq1i 
 |-  ( G ` ( j + 1 ) ) = ( seq M ( + , F ) ` ( j + 1 ) )
33 30 31 32 3brtr4g 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) <_ ( G ` ( j + 1 ) ) )
34 1 3 11 33 7 climsup 
 |-  ( ph -> G ~~> sup ( ran G , RR , < ) )