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 32039

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 4399	. . . . . . . . . . 11
2	1	imbi2d 323	. . . . . . . . . 10
3	2	2ralbidv 2832	. . . . . . . . 9
4	3	rexbidv 2892	. . . . . . . 8
5	4	cbvralv 3005	. . . . . . 7
6		r19.12 2903	. . . . . . . 8
7	6	ralimi 2796	. . . . . . 7
8	5, 7	sylbi 200	. . . . . 6
9		rphalfcl 11350	. . . . . . . . 9
10		breq2 4399	. . . . . . . . . . . . . . . 16
11	10	imbi2d 323	. . . . . . . . . . . . . . 15
12	11	ralbidv 2829	. . . . . . . . . . . . . 14
13	12	rexbidv 2892	. . . . . . . . . . . . 13
14	13	ralbidv 2829	. . . . . . . . . . . 12
15	14	rspcva 3134	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 744	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 578	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11350	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11365	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 21593	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1231	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11367	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 21504	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1231	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 4871	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
35	21, 34	sylan2 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
36	35	ad4ant23 1263	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
37		rpcn 11333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
38	37	2halvesd 10881	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
39	38	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . 26
40	39	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . . . . 24
42		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	42	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
46	45	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	43, 46	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	cbvralv 3005	. . . . . . . . . . . . . . . . . . . . . . . 24
49	41, 48	syl6bb 269	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	biimpar 493	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
51	50	adantll 728	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
52		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53		ovex 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54	52, 53	op1std 6822	. . . . . . . . . . . . . . . . . . . . . . . . . 26
55	52, 53	op2ndd 6823	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	54, 55	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	biantrurd 516	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
59	54	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	55, 55	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	59, 60	breq12d 4408	. . . . . . . . . . . . . . . . . . . . . . . . 25
62	54	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
63	62	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . 26
64	63	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	61, 64	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . 24
66	65	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . . . 23
67	58, 66	bitr3d 263	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
68	67	rspcev 3136	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69	36, 51, 68	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		eleq2 2538	. . . . . . . . . . . . . . . . . . . . . 22
71		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . . . . 24
72	71	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
73	72	rexbidv 2892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
74	70, 73	anbi12d 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
75	74	rspcev 3136	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
76	27, 33, 69, 75	syl12anc 1290	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	76	ex 441	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	rexlimdva 2871	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
79	78	ralimdva 2805	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80	79	imp 436	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
81	23	mopnuni 21534	. . . . . . . . . . . . . . . . . 18
82	18, 81	syl 17	. . . . . . . . . . . . . . . . 17
83	82	raleqdv 2979	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
84	83	ad3antrrr 744	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	80, 84	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
86		eqid 2471	. . . . . . . . . . . . . . 15
87		fveq2 5879	. . . . . . . . . . . . . . . . . 18
88		fveq2 5879	. . . . . . . . . . . . . . . . . 18
89	87, 88	oveq12d 6326	. . . . . . . . . . . . . . . . 17
90	89	eqeq2d 2481	. . . . . . . . . . . . . . . 16
91	87	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
92	88, 88	oveq12d 6326	. . . . . . . . . . . . . . . . . . 19
93	91, 92	breq12d 4408	. . . . . . . . . . . . . . . . . 18
94	87	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
95	94	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
96	95	breq1d 4405	. . . . . . . . . . . . . . . . . 18
97	93, 96	imbi12d 327	. . . . . . . . . . . . . . . . 17
98	97	ralbidv 2829	. . . . . . . . . . . . . . . 16
99	90, 98	anbi12d 725	. . . . . . . . . . . . . . 15 $/\$ $/\$
100	86, 99	cmpcovf 20483	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	17, 85, 100	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	ex 441	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
103		elinel2 3611	. . . . . . . . . . . . . 14
104		simpll 768	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	anim1i 578	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . 24
107		rnss 5069	. . . . . . . . . . . . . . . . . . . . . . . 24
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
109		rnxpss 5275	. . . . . . . . . . . . . . . . . . . . . . 23
110	108, 109	syl6ss 3430	. . . . . . . . . . . . . . . . . . . . . 22
111	110	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112		simplr 770	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ffun 5742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
114		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	114	fundmen 7661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116	115	ensymd 7638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
117	113, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		fdm 5745	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	117, 118	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . . . . 25
120		enfii 7807	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
121	119, 120	sylan2 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
122		rnfi 7875	. . . . . . . . . . . . . . . . . . . . . . . 24
123		rnfi 7875	. . . . . . . . . . . . . . . . . . . . . . . 24
124	121, 122, 123	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	112, 124	sylan 479	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
126	118	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
127		eqtr 2490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
128	82, 127	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
129		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130	129	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131	128, 130	eqnetrrd 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
132		unieq 4198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		uni0 4217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	necon3i 2675	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	131, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	126, 137	eqnetrd 2710	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
139		dm0rn0 5057	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	necon3bii 2695	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142		relxp 4947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143		relss 4927	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	106, 142, 143	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145		relrn0 5098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	145	necon3bid 2687	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147	144, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
148	147	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	141, 148	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
150	149	adantllr 733	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151		rpssre 11335	. . . . . . . . . . . . . . . . . . . . . . 23
152	111, 151	syl6ss 3430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		ltso 9732	. . . . . . . . . . . . . . . . . . . . . . 23
154		fiinfcl 8035	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ inf
155	153, 154	mpan 684	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ inf
156	125, 150, 152, 155	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ inf
157	111, 156	sseldd 3419	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ inf
158	105, 157	sylanl1 662	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ inf
159	158	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
160	82	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
161	160	anim1i 578	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163		simpl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$
164	127	eleq2d 2534	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
165		eluni2 4194	. . . . . . . . . . . . . . . . . . . . . . 23
166	164, 165	syl6bb 269	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
167	166	biimpa 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
168	162, 163, 167	syl2an 485	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		nfv 1769	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
170		nfra1 2785	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
171	169, 170	nfan 2031	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172		nfv 1769	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
173	171, 172	nfan 2031	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1769	. . . . . . . . . . . . . . . . . . . . 21 inf
175		rspa 2774	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
176		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
177	176	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
178		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180	179	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
181	177, 180	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
182	181	rspcva 3134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
183		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	44	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	185	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188	187	rspcva 3134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
189	182, 188	anim12i 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
190	189	anandirs 847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
191		prth 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
193	192	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
194	193	ad4ant23 1263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
195		simpll 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	195	anim1i 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	anim1i 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	110, 151	syl6ss 3430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
199	198	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
200		0re 9661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
201		rpge0 11337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
202	201	rgen 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
203		ssralv 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
204	110, 202, 203	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
205		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
206	205	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	206	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
208	200, 204, 207	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
209	208	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
210	144	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
211		ffn 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
212		fnfvelrn 6034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
213	211, 212	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		2ndrn 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
215	210, 213, 214	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
216		infrelb 10618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ inf
217	199, 209, 215, 216	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
218	217	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ inf
219	218	ad2ant2r 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
220	18	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
221		xmetcl 21424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
222	221	3expb 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
223	220, 222	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		simplr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
226		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
227		ne0i 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
228	215, 227	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
229		infrecl 10612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ inf
230	199, 228, 209, 229	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ inf
231	230	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
232	225, 226, 231	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
233		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
234	233	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
235		xp2nd 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
237	236	rpxrd 11365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
238	237	ad2ant2r 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239		xrltletr 11477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ inf $/\$ inf $/\$ inf
240	224, 232, 238, 239	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$ inf
241	219, 240	mpan2d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
242	241	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
243	18	ad6antr 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244		simpllr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		ffvelrn 6035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
246		xp1st 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
248	244, 226, 247	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
250	249	ad3antlr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251		xmetcl 21424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
252	243, 248, 250, 251	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253	252	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	245, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
255	225, 254	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	255	ad2ant2r 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$