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 = M
cvgcmpce.2 φ N Z
cvgcmpce.3 φ k Z F k
cvgcmpce.4 φ k Z G k
cvgcmpce.5 φ seq M + F dom
cvgcmpce.6 φ C
cvgcmpce.7 φ k N G k C F k
Assertion cvgcmpce φ seq M + G dom

Proof

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