heicant - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > heicant		Structured version Visualization version Unicode version

Theorem heicant 31975

Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.)

**Hypotheses**
Ref	Expression
heicant.c
heicant.d
heicant.j
heicant.x
heicant.y

**Assertion**
Ref	Expression
heicant	metUnif Cn_umetUnif

Proof of Theorem heicant Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4406	. . . . . . . . . . 11
2	1	imbi2d 318	. . . . . . . . . 10
3	2	2ralbidv 2832	. . . . . . . . 9
4	3	rexbidv 2901	. . . . . . . 8
5	4	cbvralv 3019	. . . . . . 7
6		r19.12 2916	. . . . . . . 8
7	6	ralimi 2781	. . . . . . 7
8	5, 7	sylbi 199	. . . . . 6
9		rphalfcl 11327	. . . . . . . . 9
10		breq2 4406	. . . . . . . . . . . . . . . 16
11	10	imbi2d 318	. . . . . . . . . . . . . . 15
12	11	ralbidv 2827	. . . . . . . . . . . . . 14
13	12	rexbidv 2901	. . . . . . . . . . . . 13
14	13	ralbidv 2827	. . . . . . . . . . . 12
15	14	rspcva 3148	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 736	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 572	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11327	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11342	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 21515	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11344	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 21426	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 4866	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
35	21, 34	sylan2 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
36	35	ad4ant23 1239	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
37		rpcn 11310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
38	37	2halvesd 10858	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
39	38	breq2d 4414	. . . . . . . . . . . . . . . . . . . . . . . . . 26
40	39	imbi1d 319	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	ralbidv 2827	. . . . . . . . . . . . . . . . . . . . . . . 24
42		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	42	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
46	45	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	43, 46	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	cbvralv 3019	. . . . . . . . . . . . . . . . . . . . . . . 24
49	41, 48	syl6bb 265	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	biimpar 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
51	50	adantll 720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
52		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53		ovex 6318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54	52, 53	op1std 6803	. . . . . . . . . . . . . . . . . . . . . . . . . 26
55	52, 53	op2ndd 6804	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	54, 55	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	biantrurd 511	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
59	54	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	55, 55	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	59, 60	breq12d 4415	. . . . . . . . . . . . . . . . . . . . . . . . 25
62	54	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
63	62	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . . . . 26
64	63	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	61, 64	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . 24
66	65	ralbidv 2827	. . . . . . . . . . . . . . . . . . . . . . 23
67	58, 66	bitr3d 259	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
68	67	rspcev 3150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69	36, 51, 68	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		eleq2 2518	. . . . . . . . . . . . . . . . . . . . . 22
71		eqeq1 2455	. . . . . . . . . . . . . . . . . . . . . . . 24
72	71	anbi1d 711	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
73	72	rexbidv 2901	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
74	70, 73	anbi12d 717	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
75	74	rspcev 3150	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
76	27, 33, 69, 75	syl12anc 1266	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	76	ex 436	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	rexlimdva 2879	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
79	78	ralimdva 2796	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80	79	imp 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
81	23	mopnuni 21456	. . . . . . . . . . . . . . . . . 18
82	18, 81	syl 17	. . . . . . . . . . . . . . . . 17
83	82	raleqdv 2993	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
84	83	ad3antrrr 736	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	80, 84	mpbid 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
86		eqid 2451	. . . . . . . . . . . . . . 15
87		fveq2 5865	. . . . . . . . . . . . . . . . . 18
88		fveq2 5865	. . . . . . . . . . . . . . . . . 18
89	87, 88	oveq12d 6308	. . . . . . . . . . . . . . . . 17
90	89	eqeq2d 2461	. . . . . . . . . . . . . . . 16
91	87	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
92	88, 88	oveq12d 6308	. . . . . . . . . . . . . . . . . . 19
93	91, 92	breq12d 4415	. . . . . . . . . . . . . . . . . 18
94	87	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20
95	94	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
96	95	breq1d 4412	. . . . . . . . . . . . . . . . . 18
97	93, 96	imbi12d 322	. . . . . . . . . . . . . . . . 17
98	97	ralbidv 2827	. . . . . . . . . . . . . . . 16
99	90, 98	anbi12d 717	. . . . . . . . . . . . . . 15 $/\$ $/\$
100	86, 99	cmpcovf 20406	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	17, 85, 100	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	ex 436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
103		elinel2 3620	. . . . . . . . . . . . . 14
104		simpll 760	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	anim1i 572	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106		frn 5735	. . . . . . . . . . . . . . . . . . . . . . . 24
107		rnss 5063	. . . . . . . . . . . . . . . . . . . . . . . 24
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
109		rnxpss 5269	. . . . . . . . . . . . . . . . . . . . . . 23
110	108, 109	syl6ss 3444	. . . . . . . . . . . . . . . . . . . . . 22
111	110	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112		simplr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ffun 5731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
114		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	114	fundmen 7643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116	115	ensymd 7620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
117	113, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		fdm 5733	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	117, 118	breqtrd 4427	. . . . . . . . . . . . . . . . . . . . . . . . 25
120		enfii 7789	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
121	119, 120	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
122		rnfi 7857	. . . . . . . . . . . . . . . . . . . . . . . 24
123		rnfi 7857	. . . . . . . . . . . . . . . . . . . . . . . 24
124	121, 122, 123	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	112, 124	sylan 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
126	118	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
127		eqtr 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
128	82, 127	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
129		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130	129	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131	128, 130	eqnetrrd 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
132		unieq 4206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		uni0 4225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	necon3i 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	131, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	126, 137	eqnetrd 2691	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
139		dm0rn0 5051	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	necon3bii 2676	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142		relxp 4942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143		relss 4922	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	106, 142, 143	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145		relrn0 5092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	145	necon3bid 2668	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147	144, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
148	147	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	141, 148	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
150	149	adantllr 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151		rpssre 11312	. . . . . . . . . . . . . . . . . . . . . . 23
152	111, 151	syl6ss 3444	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		ltso 9714	. . . . . . . . . . . . . . . . . . . . . . 23
154		fiinfcl 8017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ inf
155	153, 154	mpan 676	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ inf
156	125, 150, 152, 155	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ inf
157	111, 156	sseldd 3433	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ inf
158	105, 157	sylanl1 656	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ inf
159	158	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
160	82	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
161	160	anim1i 572	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163		simpl 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$
164	127	eleq2d 2514	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
165		eluni2 4202	. . . . . . . . . . . . . . . . . . . . . . 23
166	164, 165	syl6bb 265	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
167	166	biimpa 487	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
168	162, 163, 167	syl2an 480	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		nfv 1761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
170		nfra1 2769	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
171	169, 170	nfan 2011	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172		nfv 1761	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
173	171, 172	nfan 2011	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1761	. . . . . . . . . . . . . . . . . . . . 21 inf
175		rspa 2755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
176		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
177	176	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
178		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180	179	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
181	177, 180	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
182	181	rspcva 3148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
183		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	44	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	185	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188	187	rspcva 3148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
189	182, 188	anim12i 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
190	189	anandirs 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
191		prth 575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
193	192	adantrl 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
194	193	ad4ant23 1239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
195		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	195	anim1i 572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	anim1i 572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	110, 151	syl6ss 3444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
199	198	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
200		0re 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
201		rpge0 11314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
202	201	rgen 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
203		ssralv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
204	110, 202, 203	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
205		breq1 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
206	205	ralbidv 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	206	rspcev 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
208	200, 204, 207	sylancr 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
209	208	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
210	144	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
211		ffn 5728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
212		fnfvelrn 6019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
213	211, 212	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		2ndrn 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
215	210, 213, 214	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
216		infrelb 10596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ inf
217	199, 209, 215, 216	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
218	217	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ inf
219	218	ad2ant2r 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
220	18	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
221		xmetcl 21346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
222	221	3expb 1209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
223	220, 222	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		simplr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
226		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
227		ne0i 3737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
228	215, 227	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
229		infrecl 10590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ inf
230	199, 228, 209, 229	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ inf
231	230	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
232	225, 226, 231	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
233		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
234	233	ffvelrnda 6022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
235		xp2nd 6824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
237	236	rpxrd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
238	237	ad2ant2r 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239		xrltletr 11454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ inf $/\$ inf $/\$ inf
240	224, 232, 238, 239	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$ inf
241	219, 240	mpan2d 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
242	241	adantlr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
243	18	ad6antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244		simpllr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		ffvelrn 6020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
246		xp1st 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
248	244, 226, 247	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
250	249	ad3antlr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251		xmetcl 21346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
252	243, 248, 250, 251	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253	252	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	245, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
255	225, 254	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	255	ad2ant2r 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$