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