Theorem cauim 6924

Description: The imaginary part of a complex Caucy sequence is a Cauchy sequence.

Hypotheses

Ref	Expression
cauim.1	|- F:NN-->CC
cauim.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
cauim.3	|- G Fn NN
cauim.4	|- (x e. NN -> (G` x) = (Im` (F` x)))

Assertion

Ref	Expression
cauim	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z))

Distinct variable groups:   y,z,w   x,y,w   x,F   x,G

Proof of Theorem cauim

Step	Hyp	Ref	Expression
1		cauim.2	. 2 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
2		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (x = y -> (G` x) = (G` y))
3		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (F` x) = (F` y))
4	3	fveq2d 3728	. . . . . . . . . . . . . . . . 17 |- (x = y -> (Im` (F` x)) = (Im` (F` y)))
5	2, 4	eqeq12d 1489	. . . . . . . . . . . . . . . 16 |- (x = y -> ((G` x) = (Im` (F` x)) <-> (G` y) = (Im` (F` y))))
6		cauim.4	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (G` x) = (Im` (F` x)))
7	5, 6	vtoclga 1852	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) = (Im` (F` y)))
8		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (x = w -> (G` x) = (G` w))
9		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (x = w -> (F` x) = (F` w))
10	9	fveq2d 3728	. . . . . . . . . . . . . . . . 17 |- (x = w -> (Im` (F` x)) = (Im` (F` w)))
11	8, 10	eqeq12d 1489	. . . . . . . . . . . . . . . 16 |- (x = w -> ((G` x) = (Im` (F` x)) <-> (G` w) = (Im` (F` w))))
12	11, 6	vtoclga 1852	. . . . . . . . . . . . . . 15 |- (w e. NN -> (G` w) = (Im` (F` w)))
13	7, 12	opreqan12d 3979	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = ((Im` (F` y)) - (Im` (F` w))))
14		imsubt 6805	. . . . . . . . . . . . . . 15 |- (((F` y) e. CC /\ (F` w) e. CC) -> (Im` ((F` y) - (F` w))) = ((Im` (F` y)) - (Im` (F` w))))
15		cauim.1	. . . . . . . . . . . . . . . 16 |- F:NN-->CC
16	15	ffvelrni 3815	. . . . . . . . . . . . . . 15 |- (y e. NN -> (F` y) e. CC)
17	15	ffvelrni 3815	. . . . . . . . . . . . . . 15 |- (w e. NN -> (F` w) e. CC)
18	14, 16, 17	syl2an 454	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> (Im` ((F` y) - (F` w))) = ((Im` (F` y)) - (Im` (F` w))))
19	13, 18	eqtr4d 1510	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = (Im` ((F` y) - (F` w))))
20	19	fveq2d 3728	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) = (abs` (Im` ((F` y) - (F` w)))))
21		subclt 5364	. . . . . . . . . . . . . 14 |- (((F` y) e. CC /\ (F` w) e. CC) -> ((F` y) - (F` w)) e. CC)
22	21, 16, 17	syl2an 454	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((F` y) - (F` w)) e. CC)
23		absimlet 6866	. . . . . . . . . . . . 13 |- (((F` y) - (F` w)) e. CC -> (abs` (Im` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
24	22, 23	syl 10	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (Im` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
25	20, 24	eqbrtrd 2635	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
26	25	3adant3 799	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
27		lelttrt 5520	. . . . . . . . . . 11 |- (((abs` ((G` y) - (G` w))) e. RR /\ (abs` ((F` y) - (F` w))) e. RR /\ z e. RR) -> (((abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))) /\ (abs` ((F` y) - (F` w))) < z) -> (abs` ((G` y) - (G` w))) < z))
28		resubclt 5435	. . . . . . . . . . . . . . 15 |- (((G` y) e. RR /\ (G` w) e. RR) -> ((G` y) - (G` w)) e. RR)
29		ffnfv 3828	. . . . . . . . . . . . . . . . 17 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
30		cauim.3	. . . . . . . . . . . . . . . . 17 |- G Fn NN
31	15	ffvelrni 3815	. . . . . . . . . . . . . . . . . . . 20 |- (x e. NN -> (F` x) e. CC)
32		imclt 6755	. . . . . . . . . . . . . . . . . . . 20 |- ((F` x) e. CC -> (Im` (F` x)) e. RR)
33	31, 32	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (x e. NN -> (Im` (F` x)) e. RR)
34	6, 33	eqeltrd 1548	. . . . . . . . . . . . . . . . . 18 |- (x e. NN -> (G` x) e. RR)
35	34	rgen 1698	. . . . . . . . . . . . . . . . 17 |- A.x e. NN (G` x) e. RR
36	29, 30, 35	mpbir2an 730	. . . . . . . . . . . . . . . 16 |- G:NN-->RR
37	36	ffvelrni 3815	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) e. RR)
38	36	ffvelrni 3815	. . . . . . . . . . . . . . 15 |- (w e. NN -> (G` w) e. RR)
39	28, 37, 38	syl2an 454	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) e. RR)
40	39	recnd 5312	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) e. CC)
41		absclt 6829	. . . . . . . . . . . . 13 |- (((G` y) - (G` w)) e. CC -> (abs` ((G` y) - (G` w))) e. RR)
42	40, 41	syl 10	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) e. RR)
43	42	3adant3 799	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) e. RR)
44		absclt 6829	. . . . . . . . . . . . 13 |- (((F` y) - (F` w)) e. CC -> (abs` ((F` y) - (F` w))) e. RR)
45	22, 44	syl 10	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((F` y) - (F` w))) e. RR)
46	45	3adant3 799	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((F` y) - (F` w))) e. RR)
47		3simp3 790	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> z e. RR)
48	27, 43, 46, 47	syl3anc 858	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (((abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))) /\ (abs` ((F` y) - (F` w))) < z) -> (abs` ((G` y) - (G` w))) < z))
49	26, 48	mpand 701	. . . . . . . . 9 |- ((y e. NN /\ w e. NN /\ z e. RR) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
50	49	3com13 838	. . . . . . . 8 |- ((z e. RR /\ w e. NN /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
51	50	3expa 833	. . . . . . 7 |- (((z e. RR /\ w e. NN) /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
52	51	imim2d 25	. . . . . 6 |- (((z e. RR /\ w e. NN) /\ y e. NN) -> ((w < y -> (abs` ((F` y) - (F` w))) < z) -> (w < y -> (abs` ((G` y) - (G` w))) < z)))
53	52	r19.20dva 1709	. . . . 5 |- ((z e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z) -> A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z)))
54	53	r19.22dva 1739	. . . 4 |- (z e. RR -> (E.w e. NN