Theorem cvgcmp3ce 7187

Description: A comparison test for convergence of a complex infinite series. If, beyond a certain index B, the absolute value of sequence G is smaller than a constant C times a convergent reference sequence F, then G converges to a complex number. This version of cvgcmp3c 7186 shows just the existence of the limit rather than its explicit value.

Hypotheses

Ref	Expression
cvgcmp3ce.1	|- A e. V
cvgcmp3ce.2	|- B e. NN
cvgcmp3ce.3	|- F:NN-->RR
cvgcmp3ce.4	|- (x e. NN -> 0 <_ (F` x))
cvgcmp3ce.5	|- ( + seq1 F) ~~> A
cvgcmp3ce.6	|- C e. RR
cvgcmp3ce.7	|- 0 <_ C
cvgcmp3ce.8	|- G:NN-->CC
cvgcmp3ce.9	|- ((x e. NN /\ B < x) -> (abs` (G` x)) <_ (C x. (F` x)))

Assertion

Ref	Expression
cvgcmp3ce	|- E.y( + seq1 G) ~~> y

Distinct variable groups:   x,A   x,B   x,F   x,y,G   x,C

Proof of Theorem cvgcmp3ce

Step	Hyp	Ref	Expression
1		cvgcmp3ce.3	. . 3 |- F:NN-->RR
2		cvgcmp3ce.8	. . 3 |- G:NN-->CC
3		cvgcmp3ce.4	. . 3 |- (x e. NN -> 0 <_ (F` x))
4		cvgcmp3ce.1	. . 3 |- A e. V
5		cvgcmp3ce.5	. . 3 |- ( + seq1 F) ~~> A
6		fvex 3732	. . . 4 |- (abs` (G` u)) e. V
7		eqid 1475	. . . 4 |- {<.u, t>. | (u e. NN /\ t = (abs` (G` u)))} = {<.u, t>. | (u e. NN /\ t = (abs` (G` u)))}
8	6, 7	fnopab2 3618	. . 3 |- {<.u, t>. | (u e. NN /\ t = (abs` (G` u)))} Fn NN
9		fveq2 3724	. . . . 5 |- (u = x -> (G` u) = (G` x))
10	9	fveq2d 3728	. . . 4 |- (u = x -> (abs` (G` u)) = (abs` (G` x)))
11		fvex 3732	. . . 4 |- (abs` (G` x)) e. V
12	10, 7, 11	fvopab4 3780	. . 3 |- (x e. NN -> ({<.u, t>. | (u e. NN /\ t = (abs` (G` u)))}` x) = (abs` (G` x)))
13		fvex 3732	. . . 4 |- (Re` (( + seq1 G)` u)) e. V
14		eqid 1475	. . . 4 |- {<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))} = {<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}
15	13, 14	fnopab2 3618	. . 3 |- {<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))} Fn NN
16		fveq2 3724	. . . . 5 |- (u = x -> (( + seq1 G)` u) = (( + seq1 G)` x))
17	16	fveq2d 3728	. . . 4 |- (u = x -> (Re` (( + seq1 G)` u)) = (Re` (( + seq1 G)` x)))
18		fvex 3732	. . . 4 |- (Re` (( + seq1 G)` x)) e. V
19	17, 14, 18	fvopab4 3780	. . 3 |- (x e. NN -> ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` x) = (Re` (( + seq1 G)` x)))
20		eqid 1475	. . 3 |- {z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))} = {z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))}
21		fvex 3732	. . . 4 |- (Im` (( + seq1 G)` u)) e. V
22		eqid 1475	. . . 4 |- {<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))} = {<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}
23	21, 22	fnopab2 3618	. . 3 |- {<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))} Fn NN
24	16	fveq2d 3728	. . . 4 |- (u = x -> (Im` (( + seq1 G)` u)) = (Im` (( + seq1 G)` x)))
25		fvex 3732	. . . 4 |- (Im` (( + seq1 G)` x)) e. V
26	24, 22, 25	fvopab4 3780	. . 3 |- (x e. NN -> ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` x) = (Im` (( + seq1 G)` x)))
27		eqid 1475	. . 3 |- {z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` v))} = {z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` v))}
28		oprex 3983	. . . 4 |- (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)) e. V
29		eqid 1475	. . . 4 |- {<.h, g>. | (h e. NN /\ g = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)))} = {<.h, g>. | (h e. NN /\ g = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)))}
30	28, 29	fnopab2 3618	. . 3 |- {<.h, g>. | (h e. NN /\ g = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)))} Fn NN
31		fveq2 3724	. . . . 5 |- (h = x -> ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h) = ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` x))
32	31	opreq2d 3976	. . . 4 |- (h = x -> (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)) = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` x)))
33		oprex 3983	. . . 4 |- (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` x)) e. V
34	32, 29, 33	fvopab4 3780	. . 3 |- (x e. NN -> ({<.h, g>. | (h e. NN /\ g = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` h)))}` x) = (i x. ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` x)))
35		cvgcmp3ce.2	. . 3 |- B e. NN
36		cvgcmp3ce.6	. . 3 |- C e. RR
37		cvgcmp3ce.7	. . 3 |- 0 <_ C
38		cvgcmp3ce.9	. . 3 |- ((x e. NN /\ B < x) -> (abs` (G` x)) <_ (C x. (F` x)))
39	1, 2, 3, 4, 5, 8, 12, 15, 19, 20, 23, 26, 27, 30, 34, 35, 36, 37, 38	cvgcmp3c 7186	. 2 |- ( + seq1 G) ~~> (sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))}, RR, < ) + (i x. sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` v))}, RR, < )))
40		oprex 3983	. . 3 |- (sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))}, RR, < ) + (i x. sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` v))}, RR, < ))) e. V
41		breq2 2623	. . 3 |- (y = (sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))}, RR, < ) + (i x. sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Im` (( + seq1 G)` u)))}` v))}, RR, < ))) -> (( + seq1 G) ~~> y <-> ( + seq1 G) ~~> (sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN /\ t = (Re` (( + seq1 G)` u)))}` v))}, RR, < ) + (i x. sup({z e. RR | E.w e. NN A.v e. NN (w <_ v -> z < ({<.u, t>. | (u e. NN