caucvgi - Metamath Proof Explorer

Home

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem caucvgi 8423

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
caucvgi

Distinct variable groups:

**Proof of Theorem caucvgi**
Step	Hyp	Ref	Expression
1		caucvg.2	. . . 4
2		breq2 3342	. . . . . . . 8
3		breq2 3342	. . . . . . . . . 10
4	3	imbi2d 674	. . . . . . . . 9
5	4	rexralbidv 2142	. . . . . . . 8
6	2, 5	imbi12d 688	. . . . . . 7
7	6	rcla4cv 2377	. . . . . 6
8		rehalfcl 7220	. . . . . . . . . . 11
9	8	adantr 425	. . . . . . . . . 10 $/\$
10		halfpos2 7223	. . . . . . . . . . 11
11	10	biimpa 460	. . . . . . . . . 10 $/\$
12		biimt 803	. . . . . . . . . . 11 $/\$ $/\$
13		impexp 374	. . . . . . . . . . 11 $/\$
14	12, 13	syl6bb 595	. . . . . . . . . 10 $/\$
15	9, 11, 14	syl11anc 524	. . . . . . . . 9 $/\$
16		caucvg.1	. . . . . . . . . . . . . . . . . . . . . . 23
17		caucvg.3	. . . . . . . . . . . . . . . . . . . . . . 23
18	16, 1, 17	caucvglem5 8421	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
19	16, 1, 17	caucvglem6 8422	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
20	18, 19	jcad 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
22	16, 1, 17	caucvglem3 8419	. . . . . . . . . . . . . . . . . . . . . . . 24
23	16	ffvelrni 4788	. . . . . . . . . . . . . . . . . . . . . . . 24
24	21, 22, 23	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . 23
25	24	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
26	8	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
27		absle 8133	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	25, 26, 27	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	20, 28	sylibrd 221	. . . . . . . . . . . . . . . . . . . 20 $/\$
30	29	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
31	24	recnd 6468	. . . . . . . . . . . . . . . . . . . . . 22
32		abscl 8084	. . . . . . . . . . . . . . . . . . . . . 22
33	31, 32	syl 12	. . . . . . . . . . . . . . . . . . . . 21
34	33	ad2antlr 441	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
35	8	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
36		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
37	16	ffvelrni 4788	. . . . . . . . . . . . . . . . . . . . . . . . 25
38	36, 37, 23	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
39	38	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	39	recnd 6468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
41		abscl 8084	. . . . . . . . . . . . . . . . . . . . . 22
42	40, 41	syl 12	. . . . . . . . . . . . . . . . . . . . 21 $/\$
43	42	adantll 428	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
44		leadd1 6808	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
45	34, 35, 43, 44	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
46	30, 45	sylibd 219	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47	22	recni 6467	. . . . . . . . . . . . . . . . . . . . . . . . 25
48		npncan 6560	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
49	47, 48	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
50	23	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . . 24
51	37	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . . 24
52	49, 50, 51	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
53	52	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54	31	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
55		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
56	55, 23, 37	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
57	56	recnd 6468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
58		abstri 8150	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
59	54, 57, 58	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
60	53, 59	eqbrtrrd 3359	. . . . . . . . . . . . . . . . . . . . 21 $/\$
61		abssub 8146	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
62	61, 47, 51	sylancr 526	. . . . . . . . . . . . . . . . . . . . . 22
63	62	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 $/\$
64		abssub 8146	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
65	64, 50, 51	syl2an 503	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
66	65	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . 21 $/\$
67	60, 63, 66	3brtr3d 3366	. . . . . . . . . . . . . . . . . . . 20 $/\$
68	67	adantll 428	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
69		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
70	69, 37, 22	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . 23
71	70	recnd 6468	. . . . . . . . . . . . . . . . . . . . . 22
72		abscl 8084	. . . . . . . . . . . . . . . . . . . . . 22
73	71, 72	syl 12	. . . . . . . . . . . . . . . . . . . . 21
74	73	adantl 424	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
75	33	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
76		readdcl 6455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
77	75, 42, 76	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 $/\$
78	77	adantll 428	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
79		readdcl 6455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
80	79, 8, 42	syl2an 503	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
81	80	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
82		letr 6695	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
83	74, 78, 81, 82	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
84	68, 83	mpand 765	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85	46, 84	syld 30	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
86	85	adantrl 430	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
87		breq2 3342	. . . . . . . . . . . . . . . . . . . . . 22
88		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . 25
89	88	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . 24
90	89	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . 23
91	90	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . 22
92	87, 91	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21
93	92	rcla4v 2376	. . . . . . . . . . . . . . . . . . . 20
94	93	com3r 39	. . . . . . . . . . . . . . . . . . 19
95	94	imp 377	. . . . . . . . . . . . . . . . . 18 $/\$
96	95	adantl 424	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
97		ltadd2 6807	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
98	43, 35, 35, 97	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99	98	adantrl 430	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
100		recn 6466	. . . . . . . . . . . . . . . . . . . . 21
101		2halves 7225	. . . . . . . . . . . . . . . . . . . . 21
102	100, 101	syl 12	. . . . . . . . . . . . . . . . . . . 20
103	102	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
104	103	breq2d 3350	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
105	99, 104	bitrd 587	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
106	96, 105	sylibd 219	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
107	86, 106	jcad 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
108		simpll 448	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
109		lelttr 6693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
110	74, 81, 108, 109	syl111anc 1100	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
111	110	adantrl 430	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
112	107, 111	syld 30	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
113	112	exp32 408	. . . . . . . . . . . . 13 $/\$
114	113	com24 41	. . . . . . . . . . . 12 $/\$
115	114	r19.21adv 2181	. . . . . . . . . . 11 $/\$
116	115	reximdva 2203	. . . . . . . . . 10
117	116	adantr 425	. . . . . . . . 9 $/\$
118	15, 117	sylbird 222	. . . . . . . 8 $/\$
119	118	com12 14	. . . . . . 7 $/\$
120	119	exp3a 405	. . . . . 6
121	7, 120	syl 12	. . . . 5
122	121	r19.21aiv 2175	. . . 4
123	1, 122	ax-mp 7	. . 3
124		nnuz 7608	. . . . . 6
125	124	cvg1 8173	. . . . 5
126	125	imbi2i 202	. . . 4
127	126	ralbii 2127	. . 3
128	123, 127	mpbi 206	. 2
129		axresscn 6420	. . . 4
130		fss 4571	. . . 4 $/\$
131	16, 129, 130	mp2an 761	. . 3
132		climfnn 8352	. . 3 $/\$
133	131, 47, 132	mp2an 761	. 2
134	128, 133	mpbir 207	1

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240

wceq 1298

wcel 1300

wral 2105

wrex 2106

crab 2108

wss 2593 class class class wbr 3338

wf 3994

cfv 3998 (class class class)co 4884

csup 5663

cc 6384

cr 6385

cc0 6386

c1 6387

caddc 6389

cmin 6445

cneg 6446

cdiv 6447

cle 6448

cn 6449

clt 6653

c2 7145

cabs 8000

cli 8234

This theorem is referenced by: caucvg3ai 8424 caucvg2i 8425

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-sup 5664 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-div 6892 df-n 7108 df-2 7154 df-n0 7309 df-z 7345 df-uz 7587 df-seq1 7721 df-exp 7812 df-sqr 7920 df-re 8001 df-im 8002 df-cj 8003 df-abs 8004 df-clim 8235