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

Metamath Proof Explorer

Theorem isumle

Description: Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007) (Revised by Mario Carneiro, 24-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 isumle.1 
 |-  Z = ( ZZ>= ` M )
2 isumle.2 
 |-  ( ph -> M e. ZZ )
3 isumle.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumle.4 
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
5 isumle.5 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = B )
6 isumle.6 
 |-  ( ( ph /\ k e. Z ) -> B e. RR )
7 isumle.7 
 |-  ( ( ph /\ k e. Z ) -> A <_ B )
8 isumle.8 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
9 isumle.9 
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )
10 climdm 
 |-  ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
11 8 10 sylib 
 |-  ( ph -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
12 climdm 
 |-  ( seq M ( + , G ) e. dom ~~> <-> seq M ( + , G ) ~~> ( ~~> ` seq M ( + , G ) ) )
13 9 12 sylib 
 |-  ( ph -> seq M ( + , G ) ~~> ( ~~> ` seq M ( + , G ) ) )
14 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
15 5 6 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
16 7 3 5 3brtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )
17 1 2 11 13 14 15 16 iserle 
 |-  ( ph -> ( ~~> ` seq M ( + , F ) ) <_ ( ~~> ` seq M ( + , G ) ) )
18 4 recnd 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
19 1 2 3 18 isum 
 |-  ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
20 6 recnd 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
21 1 2 5 20 isum 
 |-  ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , G ) ) )
22 17 19 21 3brtr4d 
 |-  ( ph -> sum_ k e. Z A <_ sum_ k e. Z B )