Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem caucvg 7107

Description: A Cauchy sequence of real numbers converges. The second hypothesis specifies that is a Cauchy sequence. is the set of numbers less than all values of 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
caucvg.2
caucvg.3

Assertion

Ref	Expression
caucvg

Distinct variable groups:   ,,,,,   ,,

---

Proof of Theorem caucvg

Step	Hyp	Ref	Expression
1		caucvg.2	. . . 4
2		breq2 2618	. . . . . . . 8
3		breq2 2618	. . . . . . . . . 10
4	3	imbi2d 611	. . . . . . . . 9
5	4	rexralbidv 1679	. . . . . . . 8
6	2, 5	imbi12d 625	. . . . . . 7
7	6	rcla4cv 1870	. . . . . 6
8		biimt 730	. . . . . . . . . . 11
9		impexp 347	. . . . . . . . . . 11
10	8, 9	syl6bb 535	. . . . . . . . . 10
11		rehalfclt 5989	. . . . . . . . . . 11
12	11	adantr 389	. . . . . . . . . 10
13		halfpos2t 5992	. . . . . . . . . . 11
14	13	biimpa 416	. . . . . . . . . 10
15	10, 12, 14	sylanc 471	. . . . . . . . 9
16		caucvg.1	. . . . . . . . . . . . . . . . . . . . . . 23
17		caucvg.3	. . . . . . . . . . . . . . . . . . . . . . 23
18	16, 1, 17	caucvglem5 7105	. . . . . . . . . . . . . . . . . . . . . 22
19	16, 1, 17	caucvglem6 7106	. . . . . . . . . . . . . . . . . . . . . 22
20	18, 19	jcad 599	. . . . . . . . . . . . . . . . . . . . 21
21		abslet 6827	. . . . . . . . . . . . . . . . . . . . . 22
22	16	ffvelrni 3806	. . . . . . . . . . . . . . . . . . . . . . . 24
23	16, 1, 17	caucvglem3 7103	. . . . . . . . . . . . . . . . . . . . . . . . 25
24		resubclt 5418	. . . . . . . . . . . . . . . . . . . . . . . . 25
25	23, 24	mpan 694	. . . . . . . . . . . . . . . . . . . . . . . 24
26	22, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23
27	26	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22
28	11	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22
29	21, 27, 28	sylanc 471	. . . . . . . . . . . . . . . . . . . . 21
30	20, 29	sylibrd 204	. . . . . . . . . . . . . . . . . . . 20
31	30	adantr 389	. . . . . . . . . . . . . . . . . . 19
32		leadd1t 5607	. . . . . . . . . . . . . . . . . . . 20
33	26	recnd 5295	. . . . . . . . . . . . . . . . . . . . . 22
34		absclt 6776	. . . . . . . . . . . . . . . . . . . . . 22