Metamath Proof Explorer

Theorem iserle

Description: Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
iserle.2 
|- ( ph -> M e. ZZ )
iserle.4 
|- ( ph -> seq M ( + , F ) ~~> A )
iserle.5 
|- ( ph -> seq M ( + , G ) ~~> B )
iserle.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
iserle.7 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
iserle.8 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
Assertion iserle 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 iserle.2 
 |-  ( ph -> M e. ZZ )
3 iserle.4 
 |-  ( ph -> seq M ( + , F ) ~~> A )
4 iserle.5 
 |-  ( ph -> seq M ( + , G ) ~~> B )
5 iserle.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6 iserle.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
7 iserle.8 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
8 1 2 5 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
9 8 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
10 1 2 6 serfre 
 |-  ( ph -> seq M ( + , G ) : Z --> RR )
11 10 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , G ) ` j ) e. RR )
12 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
13 12 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
14 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ph )
15 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
16 15 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
17 16 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> k e. Z )
18 14 17 5 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. RR )
19 14 17 6 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( G ` k ) e. RR )
20 14 17 7 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) <_ ( G ` k ) )
21 13 18 19 20 serle 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) <_ ( seq M ( + , G ) ` j ) )
22 1 2 3 4 9 11 21 climle 
 |-  ( ph -> A <_ B )