Metamath Proof Explorer

Theorem abscvgcvg

Description: An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypotheses abscvgcvg.1 
|- Z = ( ZZ>= ` M )
abscvgcvg.2 
|- ( ph -> M e. ZZ )
abscvgcvg.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( abs ` ( G ` k ) ) )
abscvgcvg.4 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
abscvgcvg.5 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion abscvgcvg 
|- ( ph -> seq M ( + , G ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 abscvgcvg.1 
 |-  Z = ( ZZ>= ` M )
2 abscvgcvg.2 
 |-  ( ph -> M e. ZZ )
3 abscvgcvg.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( abs ` ( G ` k ) ) )
4 abscvgcvg.4 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
5 abscvgcvg.5 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
7 2 6 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
8 7 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
9 4 abscld 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( G ` k ) ) e. RR )
10 3 9 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
11 1red 
 |-  ( ph -> 1 e. RR )
12 1 eleq2i 
 |-  ( k e. Z <-> k e. ( ZZ>= ` M ) )
13 3 eqcomd 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( G ` k ) ) = ( F ` k ) )
14 9 13 eqled 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( G ` k ) ) <_ ( F ` k ) )
15 10 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
16 15 mulid2d 
 |-  ( ( ph /\ k e. Z ) -> ( 1 x. ( F ` k ) ) = ( F ` k ) )
17 14 16 breqtrrd 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( G ` k ) ) <_ ( 1 x. ( F ` k ) ) )
18 12 17 sylan2br 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( abs ` ( G ` k ) ) <_ ( 1 x. ( F ` k ) ) )
19 1 8 10 4 5 11 18 cvgcmpce 
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )