Theorem cvgcmp3c 7186

Description: A comparison test for convergence of a complex infinite series, where the reference sequence is multiplied by a constant. This version of cvgcmp3ce 7187 shows the explicit value of the limit (which is why we need all the hypotheses).

Hypotheses

Ref	Expression
cvgcmp3.1	|- F:NN-->RR
cvgcmp3.2	|- T:NN-->CC
cvgcmp3.3	|- (x e. NN -> 0 <_ (F` x))
cvgcmp3.6	|- A e. V
cvgcmp3.7	|- ( + seq1 F) ~~> A
cvgcmp3.8	|- H Fn NN
cvgcmp3.9	|- (x e. NN -> (H` x) = (abs` (T` x)))
cvgcmp3.10	|- G Fn NN
cvgcmp3.11	|- (x e. NN -> (G` x) = (Re` (( + seq1 T)` x)))
cvgcmp3.12	|- R = {u e. RR | E.y e. NN A.v e. NN (y <_ v -> u < (G` v))}
cvgcmp3.13	|- C Fn NN
cvgcmp3.14	|- (x e. NN -> (C` x) = (Im` (( + seq1 T)` x)))
cvgcmp3.15	|- S = {u e. RR | E.y e. NN A.v e. NN (y <_ v -> u < (C` v))}
cvgcmp3.16	|- D Fn NN
cvgcmp3.17	|- (x e. NN -> (D` x) = (i x. (C` x)))
cvgcmp3.4	|- B e. NN
cvgcmp3c.18	|- Q e. RR
cvgcmp3c.19	|- 0 <_ Q
cvgcmp3c.5	|- ((x e. NN /\ B < x) -> (abs` (T` x)) <_ (Q x. (F` x)))

Assertion

Ref	Expression
cvgcmp3c	|- ( + seq1 T) ~~> (sup(R, RR, < ) + (i x. sup(S, RR, < )))

Distinct variable groups:   x,A   x,B   x,F   x,y,v,u,G   x,H,v,u   x,T,y,u   x,R   x,D,y,u   x,C,y,v,u   x,Q

Proof of Theorem cvgcmp3c

Step	Hyp	Ref	Expression
1		cvgcmp3.2	. . 3 |- T:NN-->CC
2	1	ser1f 6329	. 2 |- ( + seq1 T):NN-->CC
3		ltso 5512	. . . . 5 |- < Or RR
4	3	supex 4577	. . . 4 |- sup(ran ( + seq1 H), RR, < ) e. V
5		cvgcmp3.6	. . . . 5 |- A e. V
6		cvgcmp3.1	. . . . 5 |- F:NN-->RR
7		ffnfv 3828	. . . . . 6 |- (H:NN-->RR <-> (H Fn NN /\ A.x e. NN (H` x) e. RR))
8		cvgcmp3.8	. . . . . 6 |- H Fn NN
9		cvgcmp3.9	. . . . . . . 8 |- (x e. NN -> (H` x) = (abs` (T` x)))
10	1	ffvelrni 3815	. . . . . . . . 9 |- (x e. NN -> (T` x) e. CC)
11		absclt 6833	. . . . . . . . 9 |- ((T` x) e. CC -> (abs` (T` x)) e. RR)
12	10, 11	syl 10	. . . . . . . 8 |- (x e. NN -> (abs` (T` x)) e. RR)
13	9, 12	eqeltrd 1548	. . . . . . 7 |- (x e. NN -> (H` x) e. RR)
14	13	rgen 1698	. . . . . 6 |- A.x e. NN (H` x) e. RR
15	7, 8, 14	mpbir2an 730	. . . . 5 |- H:NN-->RR
16		cvgcmp3.3	. . . . 5 |- (x e. NN -> 0 <_ (F` x))
17		absge0t 6854	. . . . . . 7 |- ((T` x) e. CC -> 0 <_ (abs` (T` x)))
18	10, 17	syl 10	. . . . . 6 |- (x e. NN -> 0 <_ (abs` (T` x)))
19	18, 9	breqtrrd 2641	. . . . 5 |- (x e. NN -> 0 <_ (H` x))
20		cvgcmp3.7	. . . . 5 |- ( + seq1 F) ~~> A
21		cvgcmp3.4	. . . . 5 |- B e. NN
22		cvgcmp3c.18	. . . . 5 |- Q e. RR
23		cvgcmp3c.19	. . . . 5 |- 0 <_ Q
24	9	adantr 389	. . . . . 6 |- ((x e. NN /\ B < x) -> (H` x) = (abs` (T` x)))
25		cvgcmp3c.5	. . . . . 6 |- ((x e. NN /\ B < x) -> (abs` (T` x)) <_ (Q x. (F` x)))
26	24, 25	eqbrtrd 2635	. . . . 5 |- ((x e. NN /\ B < x) -> (H` x) <_ (Q x. (F` x)))
27	5, 6, 15, 16, 19, 20, 21, 22, 23, 26	cvgcmp2c 7183	. . . 4 |- ( + seq1 H) ~~> sup(ran ( + seq1 H), RR, < )
28		axresscn 5268	. . . . . 6 |- RR (_ CC
29		fss 3635	. . . . . 6 |- ((H:NN-->RR /\ RR (_ CC) -> H:NN-->CC)
30	15, 28, 29	mp2an 697	. . . . 5 |- H:NN-->CC
31	30	ser1f 6329	. . . 4 |- ( + seq1 H):NN-->CC
32	4, 27, 31	climcau 7156	. . 3 |- A.z e. RR (0 < z -> E.w e. NN A.v e. NN (w < v -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) < z))
33		subclt 5367	. . . . . . . . . . . . . . . 16 |- (((( + seq1 T)` v) e. CC /\ (( + seq1 T)` w) e. CC) -> ((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC)
34	1	ser1cl1 6330	. . . . . . . . . . . . . . . 16 |- (v e. NN -> (( + seq1 T)` v) e. CC)
35	1	ser1cl1 6330	. . . . . . . . . . . . . . . 16 |- (w e. NN -> (( + seq1 T)` w) e. CC)
36	33, 34, 35	syl2an 454	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ w e. NN) -> ((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC)
37		absclt 6833	. . . . . . . . . . . . . . 15 |- (((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
38	36, 37	syl 10	. . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
39	38	adantr 389	. . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
40		resubclt 5438	. . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) e. RR /\ (( + seq1 H)` w) e. RR) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
41	15	ser1recl 6331	. . . . . . . . . . . . . . 15 |- (v e. NN -> (( + seq1 H)` v) e. RR)
42	15	ser1recl 6331	. . . . . . . . . . . . . . 15 |- (w e. NN -> (( + seq1 H)` w) e. RR)
43	40, 41, 42	syl2an 454	. . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
44	43	adantr 389	. . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
45	43	recnd 5315	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. CC)
46		absclt 6833	. . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) - (( + seq1 H)` w)) e. CC -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
47	45, 46	syl 10	. . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
48	47	adantr 389	. . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
49	1, 8, 9	ser1absdif 6930	. . . . . . . . . . . . . . 15 |- ((w e. NN /\ v e. NN /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
50	49	3com12 837	. . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
51	50	3expa 833	. . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
52		leabst 6864	. . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
53	43, 52	syl 10	. . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
54	53	adantr 389	. . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
55	39, 44, 48, 51, 54	letrd 5526	. . . . . . . . . . . 12 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
56	55	adantlll 396	. . . . . . . . . . 11 |- ((((z e. RR /\ v e. NN) /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
57		lelttrt 5523	. . . . . . . . . . . . 13 |- (((abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR /\ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR /\ z e. RR) -> (((abs` ((( +