HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cvgcmp3c 7122
Description: A comparison test for convergence of a complex infinite series, where the reference sequence is multiplied by a constant. This version of cvgcmp3ce 7123 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
StepHypRef Expression
1 cvgcmp3.2 . . 3 |- T:NN-->CC
21ser1f 6266 . 2 |- ( + seq1 T):NN-->CC
3 ltso 5484 . . . . 5 |- < Or RR
43supex 4551 . . . 4 |- sup(ran ( + seq1 H), RR, < ) e. V
5 cvgcmp3.6 . . . . 5 |- A e. V
6 cvgcmp3.1 . . . . 5 |- F:NN-->RR
7 ffnfv 3813 . . . . . 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)))
101ffvelrni 3800 . . . . . . . . 9 |- (x e. NN -> (T` x) e. CC)
11 absclt 6768 . . . . . . . . 9 |- ((T` x) e. CC -> (abs` (T` x)) e. RR)
1210, 11syl 10 . . . . . . . 8 |- (x e. NN -> (abs` (T` x)) e. RR)
139, 12eqeltrd 1540 . . . . . . 7 |- (x e. NN -> (H` x) e. RR)
1413rgen 1690 . . . . . 6 |- A.x e. NN (H` x) e. RR
157, 8, 14mpbir2an 728 . . . . 5 |- H:NN-->RR
16 cvgcmp3.3 . . . . 5 |- (x e. NN -> 0 <_ (F` x))
17 absge0t 6789 . . . . . . 7 |- ((T` x) e. CC -> 0 <_ (abs` (T` x)))
1810, 17syl 10 . . . . . 6 |- (x e. NN -> 0 <_ (abs` (T` x)))
1918, 9breqtrrd 2631 . . . . 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
249adantr 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)))
2624, 25eqbrtrd 2625 . . . . 5 |- ((x e. NN /\ B < x) -> (H` x) <_ (Q x. (F` x)))
275, 6, 15, 16, 19, 20, 21, 22, 23, 26cvgcmp2c 7119 . . . 4 |- ( + seq1 H) ~~> sup(ran ( + seq1 H), RR, < )
28 axresscn 5240 . . . . . 6 |- RR (_ CC
29 fss 3620 . . . . . 6 |- ((H:NN-->RR /\ RR (_ CC) -> H:NN-->CC)
3015, 28, 29mp2an 695 . . . . 5 |- H:NN-->CC
3130ser1f 6266 . . . 4 |- ( + seq1 H):NN-->CC
324, 27, 31climcau 7092 . . 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 5339 . . . . . . . . . . . . . . . 16 |- (((( + seq1 T)` v) e. CC /\ (( + seq1 T)` w) e. CC) -> ((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC)
341ser1cl1 6267 . . . . . . . . . . . . . . . 16 |- (v e. NN -> (( + seq1 T)` v) e. CC)
351ser1cl1 6267 . . . . . . . . . . . . . . . 16 |- (w e. NN -> (( + seq1 T)` w) e. CC)
3633, 34, 35syl2an 454 . . . . . . . . . . . . . . 15 |- ((v e. NN /\ w e. NN) -> ((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC)
37 absclt 6768 . . . . . . . . . . . . . . 15 |- (((( + seq1 T)` v) - (( + seq1 T)` w)) e. CC -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
3836, 37syl 10 . . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
3938adantr 389 . . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR)
40 resubclt 5410 . . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) e. RR /\ (( + seq1 H)` w) e. RR) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
4115ser1recl 6268 . . . . . . . . . . . . . . 15 |- (v e. NN -> (( + seq1 H)` v) e. RR)
4215ser1recl 6268 . . . . . . . . . . . . . . 15 |- (w e. NN -> (( + seq1 H)` w) e. RR)
4340, 41, 42syl2an 454 . . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
4443adantr 389 . . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR)
4543recnd 5287 . . . . . . . . . . . . . . 15 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) e. CC)
46 absclt 6768 . . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) - (( + seq1 H)` w)) e. CC -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
4745, 46syl 10 . . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
4847adantr 389 . . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR)
491, 8, 9ser1absdif 6867 . . . . . . . . . . . . . . 15 |- ((w e. NN /\ v e. NN /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
50493com12 835 . . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
51503expa 831 . . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ ((( + seq1 H)` v) - (( + seq1 H)` w)))
52 leabst 6799 . . . . . . . . . . . . . . 15 |- (((( + seq1 H)` v) - (( + seq1 H)` w)) e. RR -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
5343, 52syl 10 . . . . . . . . . . . . . 14 |- ((v e. NN /\ w e. NN) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
5453adantr 389 . . . . . . . . . . . . 13 |- (((v e. NN /\ w e. NN) /\ w < v) -> ((( + seq1 H)` v) - (( + seq1 H)` w)) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
5539, 44, 48, 51, 54letrd 5499 . . . . . . . . . . . 12 |- (((v e. NN /\ w e. NN) /\ w < v) -> (abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) <_ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))))
5655adantlll 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 5496 . . . . . . . . . . . . 13 |- (((abs` ((( + seq1 T)` v) - (( + seq1 T)` w))) e. RR /\ (abs` ((( + seq1 H)` v) - (( + seq1 H)` w))) e. RR /\ z e. RR) -> (((abs` ((( + seq1