Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem climcau 7092

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
climcau.2
climcau.3

Assertion

Ref	Expression
climcau

Distinct variable groups:   ,,,   ,,

---

Proof of Theorem climcau

Step	Hyp	Ref	Expression
1		halfpos2t 5984	. . . 4
2		rehalfclt 5981	. . . . 5
3		breq2 2613	. . . . . . 7
4		breq2 2613	. . . . . . . . 9
5	4	imbi2d 610	. . . . . . . 8
6	5	rexralbidv 1674	. . . . . . 7
7	3, 6	imbi12d 624	. . . . . 6
8		climcau.2	. . . . . . 7
9		climcau.1	. . . . . . . . . 10
10		1z 6106	. . . . . . . . . . 11
11		nnuz 6371	. . . . . . . . . . . 12
12	11	eqimss2i 2102	. . . . . . . . . . 11
13		nnssz 6098	. . . . . . . . . . 11
14	10, 12, 13	clmi2 7025	. . . . . . . . . 10
15	9, 14	mpanl1 704	. . . . . . . . 9
16	15	exp32 377	. . . . . . . 8
17	16	r19.21aiv 1705	. . . . . . 7
18	8, 17	ax-mp 7	. . . . . 6
19	7, 18	vtoclri 1850	. . . . 5
20	2, 19	syl 10	. . . 4
21	1, 20	sylbid 203	. . 3
22		ltlet 5493	. . . . . . . . . . . . . . . 16
23		nnret 5877	. . . . . . . . . . . . . . . 16
24		nnret 5877	. . . . . . . . . . . . . . . 16
25	22, 23, 24	syl2an 454	. . . . . . . . . . . . . . 15
26	25	adantrl 394	. . . . . . . . . . . . . 14
27		breq2 2613	. . . . . . . . . . . . . . . . 17
28		fveq2 3709	. . . . . . . . . . . . . . . . . . . 20
29	28	opreq1d 3960	. . . . . . . . . . . . . . . . . . 19
30	29	fveq2d 3713	. . . . . . . . . . . . . . . . . 18
31	30	breq1d 2619	. . . . . . . . . . . . . . . . 17
32	27, 31	imbi12d 624	. . . . . . . . . . . . . . . 16
33	32	rcla4cva 1867	. . . . . . . . . . . . . . 15
34	33	adantl 388	. . . . . . . . . . . . . 14
35	26, 34	syld 27	. . . . . . . . . . . . 13
36	35	imp 350	. . . . . . . . . . . 12
37		climcau.3	. . . . . . . . . . . . . . . . . 18
38	37	ffvelrni 3800	. . . . . . . . . . . . . . . . 17
39		climcl 6916	. . . . . . . . . . . . . . . . . . 19
40	9, 8, 39	mp2an 695	. . . . . . . . . . . . . . . . . 18
41		abssubt 6832	. . . . . . . . . . . . . . . . . 18
42	40, 41	mpan 693	. . . . . . . . . . . . . . . . 17
43	38, 42	syl 10	. . . . . . . . . . . . . . . 16
44	43	adantr 389	. . . . . . . . . . . . . . 15
45		leidt 5504	. . . . . . . . . . . . . . . . . 18
46	23, 45	syl 10	. . . . . . . . . . . . . . . . 17
47		breq2 2613	. . . . . . . . . . . . . . . . . . 19
48		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . 22
49	48	opreq1d 3960	. . . . . . . . . . . . . . . . . . . . 21
50	49	fveq2d 3713	. . . . . . . . . . . . . . . . . . . 20
51	50	breq1d 2619	. . . . . . . . . . . . . . . . . . 19
52	47, 51	imbi12d 624	. . . . . . . . . . . . . . . . . 18
53	52	rcla4v 1864	. . . . . . . . . . . . . . . . 17
54	46, 53	mpid 47	. . . . . . . . . . . . . . . 16
55	54	imp 350	. . . . . . . . . . . . . . 15