heicant - Mathbox for Brendan Leahy

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

Theorem heicant 31933

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 4425	. . . . . . . . . . 11
2	1	imbi2d 318	. . . . . . . . . 10
3	2	2ralbidv 2870	. . . . . . . . 9
4	3	rexbidv 2940	. . . . . . . 8
5	4	cbvralv 3056	. . . . . . 7
6		r19.12 2955	. . . . . . . 8
7	6	ralimi 2819	. . . . . . 7
8	5, 7	sylbi 199	. . . . . 6
9		rphalfcl 11329	. . . . . . . . 9
10		breq2 4425	. . . . . . . . . . . . . . . 16
11	10	imbi2d 318	. . . . . . . . . . . . . . 15
12	11	ralbidv 2865	. . . . . . . . . . . . . 14
13	12	rexbidv 2940	. . . . . . . . . . . . 13
14	13	ralbidv 2865	. . . . . . . . . . . 12
15	14	rspcva 3181	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 735	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 571	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11329	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11344	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 21507	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1206	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11346	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 21418	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1206	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 4883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
35	21, 34	sylan2 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
36	35	ad4ant23 1236	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
37		rpcn 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
38	37	2halvesd 10860	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
39	38	breq2d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . 26
40	39	imbi1d 319	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	ralbidv 2865	. . . . . . . . . . . . . . . . . . . . . . . 24
42		oveq2 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	42	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
46	45	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	43, 46	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	cbvralv 3056	. . . . . . . . . . . . . . . . . . . . . . . 24
49	41, 48	syl6bb 265	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	biimpar 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
51	50	adantll 719	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
52		vex 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53		ovex 6331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54	52, 53	op1std 6815	. . . . . . . . . . . . . . . . . . . . . . . . . 26
55	52, 53	op2ndd 6816	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	54, 55	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	biantrurd 511	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
59	54	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	55, 55	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	59, 60	breq12d 4434	. . . . . . . . . . . . . . . . . . . . . . . . 25
62	54	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
63	62	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . . . 26
64	63	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	61, 64	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . 24
66	65	ralbidv 2865	. . . . . . . . . . . . . . . . . . . . . . 23
67	58, 66	bitr3d 259	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
68	67	rspcev 3183	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69	36, 51, 68	syl2anc 666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		eleq2 2496	. . . . . . . . . . . . . . . . . . . . . 22
71		eqeq1 2427	. . . . . . . . . . . . . . . . . . . . . . . 24
72	71	anbi1d 710	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
73	72	rexbidv 2940	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
74	70, 73	anbi12d 716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
75	74	rspcev 3183	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
76	27, 33, 69, 75	syl12anc 1263	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	76	ex 436	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	rexlimdva 2918	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
79	78	ralimdva 2834	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80	79	imp 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
81	23	mopnuni 21448	. . . . . . . . . . . . . . . . . 18
82	18, 81	syl 17	. . . . . . . . . . . . . . . . 17
83	82	raleqdv 3032	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
84	83	ad3antrrr 735	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	80, 84	mpbid 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
86		eqid 2423	. . . . . . . . . . . . . . 15
87		fveq2 5879	. . . . . . . . . . . . . . . . . 18
88		fveq2 5879	. . . . . . . . . . . . . . . . . 18
89	87, 88	oveq12d 6321	. . . . . . . . . . . . . . . . 17
90	89	eqeq2d 2437	. . . . . . . . . . . . . . . 16
91	87	oveq1d 6318	. . . . . . . . . . . . . . . . . . 19
92	88, 88	oveq12d 6321	. . . . . . . . . . . . . . . . . . 19
93	91, 92	breq12d 4434	. . . . . . . . . . . . . . . . . 18
94	87	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
95	94	oveq1d 6318	. . . . . . . . . . . . . . . . . . 19
96	95	breq1d 4431	. . . . . . . . . . . . . . . . . 18
97	93, 96	imbi12d 322	. . . . . . . . . . . . . . . . 17
98	97	ralbidv 2865	. . . . . . . . . . . . . . . 16
99	90, 98	anbi12d 716	. . . . . . . . . . . . . . 15 $/\$ $/\$
100	86, 99	cmpcovf 20398	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	17, 85, 100	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	ex 436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
103		elinel2 3653	. . . . . . . . . . . . . 14
104		simpll 759	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	anim1i 571	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106		frn 5750	. . . . . . . . . . . . . . . . . . . . . . . 24
107		rnss 5080	. . . . . . . . . . . . . . . . . . . . . . . 24
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
109		rnxpss 5286	. . . . . . . . . . . . . . . . . . . . . . 23
110	108, 109	syl6ss 3477	. . . . . . . . . . . . . . . . . . . . . 22
111	110	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112		simplr 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ffun 5746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
114		vex 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	114	fundmen 7648	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116	115	ensymd 7625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
117	113, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		fdm 5748	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	117, 118	breqtrd 4446	. . . . . . . . . . . . . . . . . . . . . . . . 25
120		enfii 7793	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
121	119, 120	sylan2 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
122		rnfi 7861	. . . . . . . . . . . . . . . . . . . . . . . 24
123		rnfi 7861	. . . . . . . . . . . . . . . . . . . . . . . 24
124	121, 122, 123	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	112, 124	sylan 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
126	118	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
127		eqtr 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
128	82, 127	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
129		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130	129	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131	128, 130	eqnetrrd 2719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
132		unieq 4225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		uni0 4244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	syl6eq 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	necon3i 2665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	131, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	126, 137	eqnetrd 2718	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
139		dm0rn0 5068	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	necon3bii 2693	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142		relxp 4959	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143		relss 4939	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	106, 142, 143	mpisyl 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145		relrn0 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	145	necon3bid 2683	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147	144, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
148	147	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	141, 148	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
150	149	adantllr 724	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151		rpssre 11314	. . . . . . . . . . . . . . . . . . . . . . 23
152	111, 151	syl6ss 3477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		ltso 9716	. . . . . . . . . . . . . . . . . . . . . . 23
154		fiinfcl 8021	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ inf
155	153, 154	mpan 675	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ inf
156	125, 150, 152, 155	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ inf
157	111, 156	sseldd 3466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ inf
158	105, 157	sylanl1 655	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ inf
159	158	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
160	82	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
161	160	anim1i 571	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163		simpl 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$
164	127	eleq2d 2493	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
165		eluni2 4221	. . . . . . . . . . . . . . . . . . . . . . 23
166	164, 165	syl6bb 265	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
167	166	biimpa 487	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
168	162, 163, 167	syl2an 480	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		nfv 1752	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
170		nfra1 2807	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
171	169, 170	nfan 1985	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172		nfv 1752	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
173	171, 172	nfan 1985	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1752	. . . . . . . . . . . . . . . . . . . . 21 inf
175		rspa 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
176		oveq2 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
177	176	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
178		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180	179	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
181	177, 180	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
182	181	rspcva 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
183		oveq2 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	44	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	185	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188	187	rspcva 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
189	182, 188	anim12i 569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
190	189	anandirs 839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
191		prth 574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
193	192	adantrl 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
194	193	ad4ant23 1236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
195		simpll 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	195	anim1i 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	anim1i 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	110, 151	syl6ss 3477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
199	198	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
200		0re 9645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
201		rpge0 11316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
202	201	rgen 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
203		ssralv 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
204	110, 202, 203	mpisyl 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
205		breq1 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
206	205	ralbidv 2865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	206	rspcev 3183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
208	200, 204, 207	sylancr 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
209	208	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
210	144	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
211		ffn 5744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
212		fnfvelrn 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
213	211, 212	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		2ndrn 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
215	210, 213, 214	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
216		infrelb 10598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ inf
217	199, 209, 215, 216	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
218	217	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ inf
219	218	ad2ant2r 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
220	18	ad3antrrr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
221		xmetcl 21338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
222	221	3expb 1207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
223	220, 222	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		simplr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
226		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
227		ne0i 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
228	215, 227	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
229		infrecl 10592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ inf
230	199, 228, 209, 229	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ inf
231	230	rexrd 9692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
232	225, 226, 231	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
233		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
234	233	ffvelrnda 6035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
235		xp2nd 6836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
237	236	rpxrd 11344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
238	237	ad2ant2r 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239		xrltletr 11456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ inf $/\$ inf $/\$ inf
240	224, 232, 238, 239	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$ inf
241	219, 240	mpan2d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
242	241	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
243	18	ad6antr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244		simpllr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		ffvelrn 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
246		xp1st 6835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
248	244, 226, 247	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
250	249	ad3antlr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251		xmetcl 21338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
252	243, 248, 250, 251	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253	252	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	245, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
255	225, 254	sylan 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	255	ad2ant2r 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$