Theorem climcau 7109

Description: A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part).

Hypotheses

Ref	Expression
climcau.1	|- A e. V
climcau.2	|- F ~~> A
climcau.3	|- F:NN-->CC

Assertion

Ref	Expression
climcau	|- A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y < z -> (abs` ((F` z) - (F` y))) < x))

Distinct variable groups:   x,y,z,F   y,A,z

Proof of Theorem climcau

Step	Hyp	Ref	Expression
1		halfpos2t 5994	. . . 4 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
2		rehalfclt 5991	. . . . 5 |- (x e. RR -> (x / 2) e. RR)
3		breq2 2619	. . . . . . 7 |- (w = (x / 2) -> (0 < w <-> 0 < (x / 2)))
4		breq2 2619	. . . . . . . . 9 |- (w = (x / 2) -> ((abs` ((F` v) - A)) < w <-> (abs` ((F` v) - A)) < (x / 2)))
5	4	imbi2d 611	. . . . . . . 8 |- (w = (x / 2) -> ((y <_ v -> (abs` ((F` v) - A)) < w) <-> (y <_ v -> (abs` ((F` v) - A)) < (x / 2))))
6	5	rexralbidv 1680	. . . . . . 7 |- (w = (x / 2) -> (E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w) <-> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))))
7	3, 6	imbi12d 625	. . . . . 6 |- (w = (x / 2) -> ((0 < w -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w)) <-> (0 < (x / 2) -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)))))
8		climcau.2	. . . . . . 7 |- F ~~> A
9		climcau.1	. . . . . . . . . 10 |- A e. V
10		1z 6116	. . . . . . . . . . 11 |- 1 e. ZZ
11		nnuz 6384	. . . . . . . . . . . 12 |- NN = (ZZ>` 1)
12	11	eqimss2i 2109	. . . . . . . . . . 11 |- (ZZ>` 1) (_ NN
13		nnssz 6108	. . . . . . . . . . 11 |- NN (_ ZZ
14	10, 12, 13	clmi2 7040	. . . . . . . . . 10 |- (((A e. V /\ F ~~> A) /\ (w e. RR /\ 0 < w)) -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w))
15	9, 14	mpanl1 705	. . . . . . . . 9 |- ((F ~~> A /\ (w e. RR /\ 0 < w)) -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w))
16	15	exp32 377	. . . . . . . 8 |- (F ~~> A -> (w e. RR -> (0 < w -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w))))
17	16	r19.21aiv 1711	. . . . . . 7 |- (F ~~> A -> A.w e. RR (0 < w -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w)))
18	8, 17	ax-mp 7	. . . . . 6 |- A.w e. RR (0 < w -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < w))
19	7, 18	vtoclri 1856	. . . . 5 |- ((x / 2) e. RR -> (0 < (x / 2) -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))))
20	2, 19	syl 10	. . . 4 |- (x e. RR -> (0 < (x / 2) -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))))
21	1, 20	sylbid 203	. . 3 |- (x e. RR -> (0 < x -> E.y e. NN A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))))
22		ltlet 5503	. . . . . . . . . . . . . . . 16 |- ((y e. RR /\ z e. RR) -> (y < z -> y <_ z))
23		nnret 5887	. . . . . . . . . . . . . . . 16 |- (y e. NN -> y e. RR)
24		nnret 5887	. . . . . . . . . . . . . . . 16 |- (z e. NN -> z e. RR)
25	22, 23, 24	syl2an 454	. . . . . . . . . . . . . . 15 |- ((y e. NN /\ z e. NN) -> (y < z -> y <_ z))
26	25	adantrl 394	. . . . . . . . . . . . . 14 |- ((y e. NN /\ (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) /\ z e. NN)) -> (y < z -> y <_ z))
27		breq2 2619	. . . . . . . . . . . . . . . . 17 |- (v = z -> (y <_ v <-> y <_ z))
28		fveq2 3719	. . . . . . . . . . . . . . . . . . . 20 |- (v = z -> (F` v) = (F` z))
29	28	opreq1d 3970	. . . . . . . . . . . . . . . . . . 19 |- (v = z -> ((F` v) - A) = ((F` z) - A))
30	29	fveq2d 3723	. . . . . . . . . . . . . . . . . 18 |- (v = z -> (abs` ((F` v) - A)) = (abs` ((F` z) - A)))
31	30	breq1d 2625	. . . . . . . . . . . . . . . . 17 |- (v = z -> ((abs` ((F` v) - A)) < (x / 2) <-> (abs` ((F` z) - A)) < (x / 2)))
32	27, 31	imbi12d 625	. . . . . . . . . . . . . . . 16 |- (v = z -> ((y <_ v -> (abs` ((F` v) - A)) < (x / 2)) <-> (y <_ z -> (abs` ((F` z) - A)) < (x / 2))))
33	32	rcla4cva 1873	. . . . . . . . . . . . . . 15 |- ((A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) /\ z e. NN) -> (y <_ z -> (abs` ((F` z) - A)) < (x / 2)))
34	33	adantl 388	. . . . . . . . . . . . . 14 |- ((y e. NN /\ (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) /\ z e. NN)) -> (y <_ z -> (abs` ((F` z) - A)) < (x / 2)))
35	26, 34	syld 27	. . . . . . . . . . . . 13 |- ((y e. NN /\ (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) /\ z e. NN)) -> (y < z -> (abs` ((F` z) - A)) < (x / 2)))
36	35	imp 350	. . . . . . . . . . . 12 |- (((y e. NN /\ (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) /\ z e. NN)) /\ y < z) -> (abs` ((F` z) - A)) < (x / 2))
37		climcau.3	. . . . . . . . . . . . . . . . . 18 |- F:NN-->CC
38	37	ffvelrni 3810	. . . . . . . . . . . . . . . . 17 |- (y e. NN -> (F` y) e. CC)
39		climcl 6931	. . . . . . . . . . . . . . . . . . 19 |- ((A e. V /\ F ~~> A) -> A e. CC)
40	9, 8, 39	mp2an 696	. . . . . . . . . . . . . . . . . 18 |- A e. CC
41		abssubt 6847	. . . . . . . . . . . . . . . . . 18 |- ((A e. CC /\ (F` y) e. CC) -> (abs` (A - (F` y))) = (abs` ((F` y) - A)))
42	40, 41	mpan 694	. . . . . . . . . . . . . . . . 17 |- ((F` y) e. CC -> (abs` (A - (F` y))) = (abs` ((F` y) - A)))
43	38, 42	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. NN -> (abs` (A - (F` y))) = (abs` ((F` y) - A)))
44	43	adantr 389	. . . . . . . . . . . . . . 15 |- ((y e. NN /\ A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))) -> (abs` (A - (F` y))) = (abs` ((F` y) - A)))
45		leidt 5514	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> y <_ y)
46	23, 45	syl 10	. . . . . . . . . . . . . . . . 17 |- (y e. NN -> y <_ y)
47		breq2 2619	. . . . . . . . . . . . . . . . . . 19 |- (v = y -> (y <_ v <-> y <_ y))
48		fveq2 3719	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = y -> (F` v) = (F` y))
49	48	opreq1d 3970	. . . . . . . . . . . . . . . . . . . . 21 |- (v = y -> ((F` v) - A) = ((F` y) - A))
50	49	fveq2d 3723	. . . . . . . . . . . . . . . . . . . 20 |- (v = y -> (abs` ((F` v) - A)) = (abs` ((F` y) - A)))
51	50	breq1d 2625	. . . . . . . . . . . . . . . . . . 19 |- (v = y -> ((abs` ((F` v) - A)) < (x / 2) <-> (abs` ((F` y) - A)) < (x / 2)))
52	47, 51	imbi12d 625	. . . . . . . . . . . . . . . . . 18 |- (v = y -> ((y <_ v -> (abs` ((F` v) - A)) < (x / 2)) <-> (y <_ y -> (abs` ((F` y) - A)) < (x / 2))))
53	52	rcla4v 1870	. . . . . . . . . . . . . . . . 17 |- (y e. NN -> (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) -> (y <_ y -> (abs` ((F` y) - A)) < (x / 2))))
54	46, 53	mpid 47	. . . . . . . . . . . . . . . 16 |- (y e. NN -> (A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2)) -> (abs` ((F` y) - A)) < (x / 2)))
55	54	imp 350	. . . . . . . . . . . . . . 15 |- ((y e. NN /\ A.v e. NN (y <_ v -> (abs` ((F` v) - A)) < (x / 2))) -> (abs` ((F` y