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

Metamath Proof Explorer

Theorem cvgcmpub

Description: An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 cvgcmp.1 
 |-  Z = ( ZZ>= ` M )
2 cvgcmp.2 
 |-  ( ph -> N e. Z )
3 cvgcmp.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
4 cvgcmp.4 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
5 cvgcmpub.5 
 |-  ( ph -> seq M ( + , F ) ~~> A )
6 cvgcmpub.6 
 |-  ( ph -> seq M ( + , G ) ~~> B )
7 cvgcmpub.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )
8 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
9 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
10 8 9 syl 
 |-  ( ph -> M e. ZZ )
11 1 10 4 serfre 
 |-  ( ph -> seq M ( + , G ) : Z --> RR )
12 11 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. RR )
13 1 10 3 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
14 13 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. RR )
15 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
16 15 1 eleqtrdi 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` M ) )
17 simpl 
 |-  ( ( ph /\ n e. Z ) -> ph )
18 elfzuz 
 |-  ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
19 18 1 eleqtrrdi 
 |-  ( k e. ( M ... n ) -> k e. Z )
20 17 19 4 syl2an 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( G ` k ) e. RR )
21 17 19 3 syl2an 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. RR )
22 17 19 7 syl2an 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. ( M ... n ) ) -> ( G ` k ) <_ ( F ` k ) )
23 16 20 21 22 serle 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) <_ ( seq M ( + , F ) ` n ) )
24 1 10 6 5 12 14 23 climle 
 |-  ( ph -> B <_ A )