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