This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climserle

Description: The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005) (Revised by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
climserle.2 
|- ( ph -> N e. Z )
climserle.3 
|- ( ph -> seq M ( + , F ) ~~> A )
climserle.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
climserle.5 
|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
Assertion climserle 
|- ( ph -> ( seq M ( + , F ) ` N ) <_ A )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 climserle.2 
 |-  ( ph -> N e. Z )
3 climserle.3 
 |-  ( ph -> seq M ( + , F ) ~~> A )
4 climserle.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5 climserle.5 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
6 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
7 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8 6 7 syl 
 |-  ( ph -> M e. ZZ )
9 1 8 4 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
10 9 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
11 1 peano2uzs 
 |-  ( j e. Z -> ( j + 1 ) e. Z )
12 fveq2 
 |-  ( k = ( j + 1 ) -> ( F ` k ) = ( F ` ( j + 1 ) ) )
13 12 breq2d 
 |-  ( k = ( j + 1 ) -> ( 0 <_ ( F ` k ) <-> 0 <_ ( F ` ( j + 1 ) ) ) )
14 13 imbi2d 
 |-  ( k = ( j + 1 ) -> ( ( ph -> 0 <_ ( F ` k ) ) <-> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) ) )
15 5 expcom 
 |-  ( k e. Z -> ( ph -> 0 <_ ( F ` k ) ) )
16 14 15 vtoclga 
 |-  ( ( j + 1 ) e. Z -> ( ph -> 0 <_ ( F ` ( j + 1 ) ) ) )
17 16 impcom 
 |-  ( ( ph /\ ( j + 1 ) e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) )
18 11 17 sylan2 
 |-  ( ( ph /\ j e. Z ) -> 0 <_ ( F ` ( j + 1 ) ) )
19 12 eleq1d 
 |-  ( k = ( j + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( j + 1 ) ) e. RR ) )
20 19 imbi2d 
 |-  ( k = ( j + 1 ) -> ( ( ph -> ( F ` k ) e. RR ) <-> ( ph -> ( F ` ( j + 1 ) ) e. RR ) ) )
21 4 expcom 
 |-  ( k e. Z -> ( ph -> ( F ` k ) e. RR ) )
22 20 21 vtoclga 
 |-  ( ( j + 1 ) e. Z -> ( ph -> ( F ` ( j + 1 ) ) e. RR ) )
23 22 impcom 
 |-  ( ( ph /\ ( j + 1 ) e. Z ) -> ( F ` ( j + 1 ) ) e. RR )
24 11 23 sylan2 
 |-  ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) e. RR )
25 10 24 addge01d 
 |-  ( ( ph /\ j e. Z ) -> ( 0 <_ ( F ` ( j + 1 ) ) <-> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) ) )
26 18 25 mpbid 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
27 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
28 27 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
29 seqp1 
 |-  ( j e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
30 28 29 syl 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` ( j + 1 ) ) = ( ( seq M ( + , F ) ` j ) + ( F ` ( j + 1 ) ) ) )
31 26 30 breqtrrd 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( seq M ( + , F ) ` ( j + 1 ) ) )
32 1 2 3 10 31 climub 
 |-  ( ph -> ( seq M ( + , F ) ` N ) <_ A )