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 ~~> )