Theorem caucvg 7099

Description: A Cauchy sequence of real numbers converges. The second hypothesis specifies that F is a Cauchy sequence. S is the set of numbers less than all values of F except for finitely many. Reference: Bert G. Wachsmuth, http://www.shu.edu/projects/reals/numseq/proofs/cauconv.html. Request: Please contact Norm Megill if you know of a textbook reference for the version of the proof in the link above. Warning: The HTML proof page is 1/2 megabyte in size.

Hypotheses

Ref	Expression
caucvg.1	|- F:NN-->RR
caucvg.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
caucvg.3	|- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}

Assertion

Ref	Expression
caucvg	|- F ~~> sup(S, RR, < )

Distinct variable groups:   y,z,w,u,v,F   z,S,w

Proof of Theorem caucvg

Step	Hyp	Ref	Expression
1		caucvg.2	. . . 4 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
2		breq2 2613	. . . . . . . 8 |- (z = (x / 2) -> (0 < z <-> 0 < (x / 2)))
3		breq2 2613	. . . . . . . . . 10 |- (z = (x / 2) -> ((abs` ((F` y) - (F` w))) < z <-> (abs` ((F` y) - (F` w))) < (x / 2)))
4	3	imbi2d 610	. . . . . . . . 9 |- (z = (x / 2) -> ((w < y -> (abs` ((F` y) - (F` w))) < z) <-> (w < y -> (abs` ((F` y) - (F` w))) < (x / 2))))
5	4	rexralbidv 1674	. . . . . . . 8 |- (z = (x / 2) -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z) <-> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2))))
6	2, 5	imbi12d 624	. . . . . . 7 |- (z = (x / 2) -> ((0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) <-> (0 < (x / 2) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)))))
7	6	rcla4cv 1865	. . . . . 6 |- (A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) -> ((x / 2) e. RR -> (0 < (x / 2) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)))))
8		biimt 729	. . . . . . . . . . 11 |- (((x / 2) e. RR /\ 0 < (x / 2)) -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) <-> (((x / 2) e. RR /\ 0 < (x / 2)) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)))))
9		impexp 347	. . . . . . . . . . 11 |- ((((x / 2) e. RR /\ 0 < (x / 2)) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2))) <-> ((x / 2) e. RR -> (0 < (x / 2) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)))))
10	8, 9	syl6bb 534	. . . . . . . . . 10 |- (((x / 2) e. RR /\ 0 < (x / 2)) -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) <-> ((x / 2) e. RR -> (0 < (x / 2) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2))))))
11		rehalfclt 5981	. . . . . . . . . . 11 |- (x e. RR -> (x / 2) e. RR)
12	11	adantr 389	. . . . . . . . . 10 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
13		halfpos2t 5984	. . . . . . . . . . 11 |- (x e. RR -> (0 < x <-> 0 < (x / 2)))
14	13	biimpa 416	. . . . . . . . . 10 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
15	10, 12, 14	sylanc 471	. . . . . . . . 9 |- ((x e. RR /\ 0 < x) -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) <-> ((x / 2) e. RR -> (0 < (x / 2) -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2))))))
16		caucvg.1	. . . . . . . . . . . . . . . . . . . . . . 23 |- F:NN-->RR
17		caucvg.3	. . . . . . . . . . . . . . . . . . . . . . 23 |- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}
18	16, 1, 17	caucvglem5 7097	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> -u(x / 2) <_ (sup(S, RR, < ) - (F` w))))
19	16, 1, 17	caucvglem6 7098	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> (sup(S, RR, < ) - (F` w)) <_ (x / 2)))
20	18, 19	jcad 598	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> (-u(x / 2) <_ (sup(S, RR, < ) - (F` w)) /\ (sup(S, RR, < ) - (F` w)) <_ (x / 2))))
21		abslet 6819	. . . . . . . . . . . . . . . . . . . . . 22 |- (((sup(S, RR, < ) - (F` w)) e. RR /\ (x / 2) e. RR) -> ((abs` (sup(S, RR, < ) - (F` w))) <_ (x / 2) <-> (-u(x / 2) <_ (sup(S, RR, < ) - (F` w)) /\ (sup(S, RR, < ) - (F` w)) <_ (x / 2))))
22	16	ffvelrni 3800	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w e. NN -> (F` w) e. RR)
23	16, 1, 17	caucvglem3 7095	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- sup(S, RR, < ) e. RR
24		resubclt 5410	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((sup(S, RR, < ) e. RR /\ (F` w) e. RR) -> (sup(S, RR, < ) - (F` w)) e. RR)
25	23, 24	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` w) e. RR -> (sup(S, RR, < ) - (F` w)) e. RR)
26	22, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. NN -> (sup(S, RR, < ) - (F` w)) e. RR)
27	26	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. RR /\ w e. NN) -> (sup(S, RR, < ) - (F` w)) e. RR)
28	11	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. RR /\ w e. NN) -> (x / 2) e. RR)
29	21, 27, 28	sylanc 471	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ w e. NN) -> ((abs` (sup(S, RR, < ) - (F` w))) <_ (x / 2) <-> (-u(x / 2) <_ (sup(S, RR, < ) - (F` w)) /\ (sup(S, RR, < ) - (F` w)) <_ (x / 2))))
30	20, 29	sylibrd 204	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> (abs` (sup(S, RR, < ) - (F` w))) <_ (x / 2)))
31	30	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- (((x e. RR /\ w e. NN) /\ t e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> (abs` (sup(S, RR, < ) - (F` w))) <_ (x / 2)))
32		leadd1t 5599	. . . . . . . . . . . . . . . . . . . 20 |- (((abs` (sup(S, RR, < ) - (F` w))) e. RR /\ (x / 2) e. RR /\ (abs` ((F` t) - (F` w))) e. RR) -> ((abs` (sup(S, RR, < ) - (F` w))) <_ (x / 2) <-> ((abs` (sup(S, RR, < ) - (F` w))) + (abs` ((F` t) - (F` w)))) <_ ((x / 2) + (abs` ((F` t) - (F` w))))))
33	26	recnd 5287	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. NN -> (sup(S, RR, < ) - (F` w)) e. CC)
34		absclt 6768	. . . . . . . . . . . . . . . . . . . . . 22 |- ((sup(S,