Theorem caure 6893

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

Hypotheses

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

Assertion

Ref	Expression
caure	|- 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 caure

Step	Hyp	Ref	Expression
1		caure.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 3721	. . . . . . . . . . . . . . . . 17 |- (x = y -> (G` x) = (G` y))
3		fveq2 3721	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (F` x) = (F` y))
4	3	fveq2d 3725	. . . . . . . . . . . . . . . . 17 |- (x = y -> (Re` (F` x)) = (Re` (F` y)))
5	2, 4	eqeq12d 1488	. . . . . . . . . . . . . . . 16 |- (x = y -> ((G` x) = (Re` (F` x)) <-> (G` y) = (Re` (F` y))))
6		caure.4	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (G` x) = (Re` (F` x)))
7	5, 6	vtoclga 1850	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) = (Re` (F` y)))
8		fveq2 3721	. . . . . . . . . . . . . . . . 17 |- (x = w -> (G` x) = (G` w))
9		fveq2 3721	. . . . . . . . . . . . . . . . . 18 |- (x = w -> (F` x) = (F` w))
10	9	fveq2d 3725	. . . . . . . . . . . . . . . . 17 |- (x = w -> (Re` (F` x)) = (Re` (F` w)))
11	8, 10	eqeq12d 1488	. . . . . . . . . . . . . . . 16 |- (x = w -> ((G` x) = (Re` (F` x)) <-> (G` w) = (Re` (F` w))))
12	11, 6	vtoclga 1850	. . . . . . . . . . . . . . 15 |- (w e. NN -> (G` w) = (Re` (F` w)))
13	7, 12	opreqan12d 3976	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = ((Re` (F` y)) - (Re` (F` w))))
14		resubt 6767	. . . . . . . . . . . . . . 15 |- (((F` y) e. CC /\ (F` w) e. CC) -> (Re` ((F` y) - (F` w))) = ((Re` (F` y)) - (Re` (F` w))))
15		caure.1	. . . . . . . . . . . . . . . 16 |- F:NN-->CC
16	15	ffvelrni 3812	. . . . . . . . . . . . . . 15 |- (y e. NN -> (F` y) e. CC)
17	15	ffvelrni 3812	. . . . . . . . . . . . . . 15 |- (w e. NN -> (F` w) e. CC)
18	14, 16, 17	syl2an 454	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> (Re` ((F` y) - (F` w))) = ((Re` (F` y)) - (Re` (F` w))))
19	13, 18	eqtr4d 1509	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = (Re` ((F` y) - (F` w))))
20	19	fveq2d 3725	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) = (abs` (Re` ((F` y) - (F` w)))))
21		subclt 5354	. . . . . . . . . . . . . 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		absrelet 6831	. . . . . . . . . . . . 13 |- (((F` y) - (F` w)) e. CC -> (abs` (Re` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
24	22, 23	syl 10	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (Re` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
25	20, 24	eqbrtrd 2632	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
26	25	3adant3 798	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
27		lelttrt 5510	. . . . . . . . . . 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 5425	. . . . . . . . . . . . . . 15 |- (((G` y) e. RR /\ (G` w) e. RR) -> ((G` y) - (G` w)) e. RR)
29		ffnfv 3825	. . . . . . . . . . . . . . . . 17 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
30		caure.3	. . . . . . . . . . . . . . . . 17 |- G Fn NN
31	15	ffvelrni 3812	. . . . . . . . . . . . . . . . . . . 20 |- (x e. NN -> (F` x) e. CC)
32		reclt 6709	. . . . . . . . . . . . . . . . . . . 20 |- ((F` x) e. CC -> (Re` (F` x)) e. RR)
33	31, 32	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (x e. NN -> (Re` (F` x)) e. RR)
34	6, 33	eqeltrd 1547	. . . . . . . . . . . . . . . . . 18 |- (x e. NN -> (G` x) e. RR)
35	34	rgen 1697	. . . . . . . . . . . . . . . . 17 |- A.x e. NN (G` x) e. RR
36	29, 30, 35	mpbir2an 729	. . . . . . . . . . . . . . . 16 |- G:NN-->RR
37	36	ffvelrni 3812	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) e. RR)
38	36	ffvelrni 3812	. . . . . . . . . . . . . . 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 5302	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) e. CC)
41		absclt 6794	. . . . . . . . . . . . 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 798	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) e. RR)
44		absclt 6794	. . . . . . . . . . . . 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 798	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((F` y) - (F` w))) e. RR)
47		3simp3 789	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> z e. RR)
48	27, 43, 46, 47	syl3anc 857	. . . . . . . . . 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 700	. . . . . . . . 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 837	. . . . . . . 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 832	. . . . . . 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 1708	. . . . 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 1738	. . . 4 |- (z e. RR -> (E.w e. NN A.