Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem xplm 7909

Description: Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

Ref	Expression
xplm.a
xplm.b
xplm.1
xplm.3
xplm.5	Met
xplm.6	Met
xplm.7
xplm.9
xplm.10
xplm.11

Assertion

Ref	Expression
xplm

Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,

---

Proof of Theorem xplm

Step	Hyp	Ref	Expression
1		opelxpi 3207	. . . . 5
2		xplm.5	. . . . . 6 Met
3		xplm.a	. . . . . 6
4		xplm.1	. . . . . . 7
5	4	lmcl 7884	. . . . . 6 Met
6	2, 3, 5	mp3an12 903	. . . . 5
7		xplm.6	. . . . . 6 Met
8		xplm.b	. . . . . 6
9		xplm.3	. . . . . . 7
10	9	lmcl 7884	. . . . . 6 Met
11	7, 8, 10	mp3an12 903	. . . . 5
12	1, 6, 11	syl2an 454	. . . 4
13		1z 6106	. . . . . . . . . . . . 13
14		nnuz 6371	. . . . . . . . . . . . 13
15	4, 13, 14	lmcvg2 7871	. . . . . . . . . . . 12 Met
16	2, 15	mp3anl1 907	. . . . . . . . . . 11
17	3, 16	mpanl1 704	. . . . . . . . . 10
18	9, 13, 14	lmcvg2 7871	. . . . . . . . . . . 12 Met
19	7, 18	mp3anl1 907	. . . . . . . . . . 11
20	8, 19	mpanl1 704	. . . . . . . . . 10
21	17, 20	anim12i 333	. . . . . . . . 9
22	21	anandirs 512	. . . . . . . 8
23		reeanv 1770	. . . . . . . . 9
24		nnret 5877	. . . . . . . . . . . . 13
25	24	adantr 389	. . . . . . . . . . . 12
26		nnret 5877	. . . . . . . . . . . . 13
27	26	adantl 388	. . . . . . . . . . . 12
28		letrt 5498	. . . . . . . . . . . . . . . . . . . . . 22
29		nnret 5877	. . . . . . . . . . . . . . . . . . . . . 22
30	28, 24, 26, 29	syl3an 866	. . . . . . . . . . . . . . . . . . . . 21
31	30	3expa 831	. . . . . . . . . . . . . . . . . . . 20
32	31	exp3a 375	. . . . . . . . . . . . . . . . . . 19
33	32	imp 350	. . . . . . . . . . . . . . . . . 18
34	33	an1rs 488	. . . . . . . . . . . . . . . . 17
35	34	ancrd 299	. . . . . . . . . . . . . . . 16
36	35	imim1d 28	. . . . . . . . . . . . . . 15
37	36	r19.20dva 1701	. . . . . . . . . . . . . 14
38		simplr 413	. . . . . . . . . . . . . 14
39	37, 38	jctild 599	. . . . . . . . . . . . 13
40		breq1 2612	. . . . . . . . . . . . . . . 16
41	40	imbi1d 611	. . . . . . . . . . . . . . 15
42	41	ralbidv 1655	. . . . . . . . . . . . . 14
43	42	rcla4ev 1868	. . . . . . . . . . . . 13
44	39, 43	syl6 22	. . . . . . . . . . . 12
45		letrt 5498	. . . . . . . . . . . . . . . . . . . . . . 23
46	45, 26, 24, 29	syl3an 866	. . . . . . . . . . . . . . . . . . . . . 22
47	46	3com12 835	. . . . . . . . . . . . . . . . . . . . 21