Metamath Proof Explorer


Theorem cvgcmpce

Description: A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses cvgcmpce.1
|- Z = ( ZZ>= ` M )
cvgcmpce.2
|- ( ph -> N e. Z )
cvgcmpce.3
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
cvgcmpce.4
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
cvgcmpce.5
|- ( ph -> seq M ( + , F ) e. dom ~~> )
cvgcmpce.6
|- ( ph -> C e. RR )
cvgcmpce.7
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( G ` k ) ) <_ ( C x. ( F ` k ) ) )
Assertion cvgcmpce
|- ( ph -> seq M ( + , G ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 cvgcmpce.1
 |-  Z = ( ZZ>= ` M )
2 cvgcmpce.2
 |-  ( ph -> N e. Z )
3 cvgcmpce.3
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
4 cvgcmpce.4
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
5 cvgcmpce.5
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 cvgcmpce.6
 |-  ( ph -> C e. RR )
7 cvgcmpce.7
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( G ` k ) ) <_ ( C x. ( 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 serf
 |-  ( ph -> seq M ( + , G ) : Z --> CC )
12 11 ffvelrnda
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. CC )
13 fveq2
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
14 13 oveq2d
 |-  ( m = k -> ( C x. ( F ` m ) ) = ( C x. ( F ` k ) ) )
15 eqid
 |-  ( m e. Z |-> ( C x. ( F ` m ) ) ) = ( m e. Z |-> ( C x. ( F ` m ) ) )
16 ovex
 |-  ( C x. ( F ` k ) ) e. _V
17 14 15 16 fvmpt
 |-  ( k e. Z -> ( ( m e. Z |-> ( C x. ( F ` m ) ) ) ` k ) = ( C x. ( F ` k ) ) )
18 17 adantl
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( C x. ( F ` m ) ) ) ` k ) = ( C x. ( F ` k ) ) )
19 6 adantr
 |-  ( ( ph /\ k e. Z ) -> C e. RR )
20 19 3 remulcld
 |-  ( ( ph /\ k e. Z ) -> ( C x. ( F ` k ) ) e. RR )
21 18 20 eqeltrd
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( C x. ( F ` m ) ) ) ` k ) e. RR )
22 2fveq3
 |-  ( m = k -> ( abs ` ( G ` m ) ) = ( abs ` ( G ` k ) ) )
23 eqid
 |-  ( m e. Z |-> ( abs ` ( G ` m ) ) ) = ( m e. Z |-> ( abs ` ( G ` m ) ) )
24 fvex
 |-  ( abs ` ( G ` k ) ) e. _V
25 22 23 24 fvmpt
 |-  ( k e. Z -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) = ( abs ` ( G ` k ) ) )
26 25 adantl
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) = ( abs ` ( G ` k ) ) )
27 4 abscld
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( G ` k ) ) e. RR )
28 26 27 eqeltrd
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) e. RR )
29 6 recnd
 |-  ( ph -> C e. CC )
30 climdm
 |-  ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
31 5 30 sylib
 |-  ( ph -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
32 3 recnd
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
33 1 10 29 31 32 18 isermulc2
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( C x. ( F ` m ) ) ) ) ~~> ( C x. ( ~~> ` seq M ( + , F ) ) ) )
34 climrel
 |-  Rel ~~>
35 34 releldmi
 |-  ( seq M ( + , ( m e. Z |-> ( C x. ( F ` m ) ) ) ) ~~> ( C x. ( ~~> ` seq M ( + , F ) ) ) -> seq M ( + , ( m e. Z |-> ( C x. ( F ` m ) ) ) ) e. dom ~~> )
36 33 35 syl
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( C x. ( F ` m ) ) ) ) e. dom ~~> )
37 1 uztrn2
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
38 2 37 sylan
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
39 4 absge0d
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( abs ` ( G ` k ) ) )
40 39 26 breqtrrd
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) )
41 38 40 syldan
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) )
42 38 25 syl
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) = ( abs ` ( G ` k ) ) )
43 38 17 syl
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( m e. Z |-> ( C x. ( F ` m ) ) ) ` k ) = ( C x. ( F ` k ) ) )
44 7 42 43 3brtr4d
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) <_ ( ( m e. Z |-> ( C x. ( F ` m ) ) ) ` k ) )
45 1 2 21 28 36 41 44 cvgcmp
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) e. dom ~~> )
46 1 climcau
 |-  ( ( M e. ZZ /\ seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x )
47 10 45 46 syl2anc
 |-  ( ph -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x )
48 1 10 28 serfre
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) : Z --> RR )
49 48 ad2antrr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) : Z --> RR )
50 1 uztrn2
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
51 50 adantl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n e. Z )
52 49 51 ffvelrnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) e. RR )
53 simprl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j e. Z )
54 49 53 ffvelrnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) e. RR )
55 52 54 resubcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) e. RR )
56 0red
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 e. RR )
57 11 ad2antrr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> seq M ( + , G ) : Z --> CC )
58 57 51 ffvelrnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , G ) ` n ) e. CC )
59 57 53 ffvelrnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , G ) ` j ) e. CC )
60 58 59 subcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) e. CC )
61 60 abscld
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) e. RR )
62 60 absge0d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 <_ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) )
63 fzfid
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( M ... n ) e. Fin )
64 difss
 |-  ( ( M ... n ) \ ( M ... j ) ) C_ ( M ... n )
65 ssfi
 |-  ( ( ( M ... n ) e. Fin /\ ( ( M ... n ) \ ( M ... j ) ) C_ ( M ... n ) ) -> ( ( M ... n ) \ ( M ... j ) ) e. Fin )
66 63 64 65 sylancl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( M ... n ) \ ( M ... j ) ) e. Fin )
67 eldifi
 |-  ( k e. ( ( M ... n ) \ ( M ... j ) ) -> k e. ( M ... n ) )
68 simpll
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ph )
69 elfzuz
 |-  ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) )
70 69 1 eleqtrrdi
 |-  ( k e. ( M ... n ) -> k e. Z )
71 68 70 4 syl2an
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... n ) ) -> ( G ` k ) e. CC )
72 67 71 sylan2
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ( M ... n ) \ ( M ... j ) ) ) -> ( G ` k ) e. CC )
73 66 72 fsumabs
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) ) <_ sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( abs ` ( G ` k ) ) )
74 eqidd
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... n ) ) -> ( G ` k ) = ( G ` k ) )
75 51 1 eleqtrdi
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n e. ( ZZ>= ` M ) )
76 74 75 71 fsumser
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... n ) ( G ` k ) = ( seq M ( + , G ) ` n ) )
77 eqidd
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... j ) ) -> ( G ` k ) = ( G ` k ) )
78 53 1 eleqtrdi
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j e. ( ZZ>= ` M ) )
79 elfzuz
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
80 79 1 eleqtrrdi
 |-  ( k e. ( M ... j ) -> k e. Z )
81 68 80 4 syl2an
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... j ) ) -> ( G ` k ) e. CC )
82 77 78 81 fsumser
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... j ) ( G ` k ) = ( seq M ( + , G ) ` j ) )
83 76 82 oveq12d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( M ... n ) ( G ` k ) - sum_ k e. ( M ... j ) ( G ` k ) ) = ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) )
84 fzfid
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( M ... j ) e. Fin )
85 84 81 fsumcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... j ) ( G ` k ) e. CC )
86 66 72 fsumcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) e. CC )
87 disjdif
 |-  ( ( M ... j ) i^i ( ( M ... n ) \ ( M ... j ) ) ) = (/)
88 87 a1i
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( M ... j ) i^i ( ( M ... n ) \ ( M ... j ) ) ) = (/) )
89 undif2
 |-  ( ( M ... j ) u. ( ( M ... n ) \ ( M ... j ) ) ) = ( ( M ... j ) u. ( M ... n ) )
90 fzss2
 |-  ( n e. ( ZZ>= ` j ) -> ( M ... j ) C_ ( M ... n ) )
91 90 ad2antll
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( M ... j ) C_ ( M ... n ) )
92 ssequn1
 |-  ( ( M ... j ) C_ ( M ... n ) <-> ( ( M ... j ) u. ( M ... n ) ) = ( M ... n ) )
93 91 92 sylib
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( M ... j ) u. ( M ... n ) ) = ( M ... n ) )
94 89 93 eqtr2id
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( M ... n ) = ( ( M ... j ) u. ( ( M ... n ) \ ( M ... j ) ) ) )
95 88 94 63 71 fsumsplit
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... n ) ( G ` k ) = ( sum_ k e. ( M ... j ) ( G ` k ) + sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) ) )
96 85 86 95 mvrladdd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( M ... n ) ( G ` k ) - sum_ k e. ( M ... j ) ( G ` k ) ) = sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) )
97 83 96 eqtr3d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) = sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) )
98 97 fveq2d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) = ( abs ` sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( G ` k ) ) )
99 70 adantl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... n ) ) -> k e. Z )
100 99 25 syl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... n ) ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) = ( abs ` ( G ` k ) ) )
101 abscl
 |-  ( ( G ` k ) e. CC -> ( abs ` ( G ` k ) ) e. RR )
102 101 recnd
 |-  ( ( G ` k ) e. CC -> ( abs ` ( G ` k ) ) e. CC )
103 71 102 syl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... n ) ) -> ( abs ` ( G ` k ) ) e. CC )
104 100 75 103 fsumser
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... n ) ( abs ` ( G ` k ) ) = ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) )
105 80 adantl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... j ) ) -> k e. Z )
106 105 25 syl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... j ) ) -> ( ( m e. Z |-> ( abs ` ( G ` m ) ) ) ` k ) = ( abs ` ( G ` k ) ) )
107 81 102 syl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( M ... j ) ) -> ( abs ` ( G ` k ) ) e. CC )
108 106 78 107 fsumser
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... j ) ( abs ` ( G ` k ) ) = ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) )
109 104 108 oveq12d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( M ... n ) ( abs ` ( G ` k ) ) - sum_ k e. ( M ... j ) ( abs ` ( G ` k ) ) ) = ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) )
110 84 107 fsumcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... j ) ( abs ` ( G ` k ) ) e. CC )
111 72 102 syl
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ k e. ( ( M ... n ) \ ( M ... j ) ) ) -> ( abs ` ( G ` k ) ) e. CC )
112 66 111 fsumcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( abs ` ( G ` k ) ) e. CC )
113 88 94 63 103 fsumsplit
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( M ... n ) ( abs ` ( G ` k ) ) = ( sum_ k e. ( M ... j ) ( abs ` ( G ` k ) ) + sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( abs ` ( G ` k ) ) ) )
114 110 112 113 mvrladdd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( M ... n ) ( abs ` ( G ` k ) ) - sum_ k e. ( M ... j ) ( abs ` ( G ` k ) ) ) = sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( abs ` ( G ` k ) ) )
115 109 114 eqtr3d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) = sum_ k e. ( ( M ... n ) \ ( M ... j ) ) ( abs ` ( G ` k ) ) )
116 73 98 115 3brtr4d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) <_ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) )
117 56 61 55 62 116 letrd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 <_ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) )
118 55 117 absidd
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) = ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) )
119 118 breq1d
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x <-> ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) < x ) )
120 rpre
 |-  ( x e. RR+ -> x e. RR )
121 120 ad2antlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> x e. RR )
122 lelttr
 |-  ( ( ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) e. RR /\ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) <_ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) /\ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) < x ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
123 61 55 121 122 syl3anc
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) <_ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) /\ ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) < x ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
124 116 123 mpand
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) < x -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
125 119 124 sylbid
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
126 125 anassrs
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ n e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
127 126 ralimdva
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x -> A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
128 127 reximdva
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x -> E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
129 128 ralimdva
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` n ) - ( seq M ( + , ( m e. Z |-> ( abs ` ( G ` m ) ) ) ) ` j ) ) ) < x -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x ) )
130 47 129 mpd
 |-  ( ph -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` j ) ) ) < x )
131 seqex
 |-  seq M ( + , G ) e. _V
132 131 a1i
 |-  ( ph -> seq M ( + , G ) e. _V )
133 1 12 130 132 caucvg
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )