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 33444

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 4657	. . . . . . . . . . 11
2	1	imbi2d 330	. . . . . . . . . 10
3	2	2ralbidv 2989	. . . . . . . . 9
4	3	rexbidv 3052	. . . . . . . 8
5	4	cbvralv 3171	. . . . . . 7
6		r19.12 3063	. . . . . . . 8
7	6	ralimi 2952	. . . . . . 7
8	5, 7	sylbi 207	. . . . . 6
9		rphalfcl 11858	. . . . . . . . 9
10		breq2 4657	. . . . . . . . . . . . . . . 16
11	10	imbi2d 330	. . . . . . . . . . . . . . 15
12	11	ralbidv 2986	. . . . . . . . . . . . . 14
13	12	rexbidv 3052	. . . . . . . . . . . . 13
14	13	ralbidv 2986	. . . . . . . . . . . 12
15	14	rspcva 3307	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 592	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11858	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 22305	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1265	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11875	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 554	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 22216	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1265	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
35	21, 34	sylan2 491	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
36	35	ad4ant23 1297	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
37		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
38	37	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
39	38	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
40	39	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . 25
41	40	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . 24
42		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
43	42	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
46	45	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	43, 46	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . . . . 24
49	41, 48	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	biimpar 502	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
51	50	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
52		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54	52, 53	op1std 7178	. . . . . . . . . . . . . . . . . . . . . . . . . 26
55	52, 53	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	54, 55	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25
57	56	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24
58	57	biantrurd 529	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
59	54	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
60	55, 55	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	59, 60	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . 25
62	54	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
63	62	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
64	63	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	61, 64	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . 24
66	65	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . 23
67	58, 66	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
68	67	rspcev 3309	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
69	36, 51, 68	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . 22
71		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . 24
72	71	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
73	72	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
74	70, 73	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
75	74	rspcev 3309	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
76	27, 33, 69, 75	syl12anc 1324	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	76	ex 450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	rexlimdva 3031	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
79	78	ralimdva 2962	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
80	79	imp 445	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
81	23	mopnuni 22246	. . . . . . . . . . . . . . . . . 18
82	18, 81	syl 17	. . . . . . . . . . . . . . . . 17
83	82	raleqdv 3144	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
84	83	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	80, 84	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
86		eqid 2622	. . . . . . . . . . . . . . 15
87		fveq2 6191	. . . . . . . . . . . . . . . . . 18
88		fveq2 6191	. . . . . . . . . . . . . . . . . 18
89	87, 88	oveq12d 6668	. . . . . . . . . . . . . . . . 17
90	89	eqeq2d 2632	. . . . . . . . . . . . . . . 16
91	87	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
92	88, 88	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
93	91, 92	breq12d 4666	. . . . . . . . . . . . . . . . . 18
94	87	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
95	94	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
96	95	breq1d 4663	. . . . . . . . . . . . . . . . . 18
97	93, 96	imbi12d 334	. . . . . . . . . . . . . . . . 17
98	97	ralbidv 2986	. . . . . . . . . . . . . . . 16
99	90, 98	anbi12d 747	. . . . . . . . . . . . . . 15 $/\$ $/\$
100	86, 99	cmpcovf 21194	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	17, 85, 100	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	ex 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
103		elinel2 3800	. . . . . . . . . . . . . 14
104		simpll 790	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
105	104	anim1i 592	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . 24
107		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . 24
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
109		rnxpss 5566	. . . . . . . . . . . . . . . . . . . . . . 23
110	108, 109	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . 22
111	110	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113		ffun 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
114		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	114	fundmen 8030	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116	115	ensymd 8007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
117	113, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119	117, 118	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25
120		enfii 8177	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
121	119, 120	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
122		rnfi 8249	. . . . . . . . . . . . . . . . . . . . . . . 24
123		rnfi 8249	. . . . . . . . . . . . . . . . . . . . . . . 24
124	121, 122, 123	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	112, 124	sylan 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
126	118	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
127		eqtr 2641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
128	82, 127	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
129		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130	129	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131	128, 130	eqnetrrd 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
132		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		uni0 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	necon3i 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	131, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
137	136	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	126, 137	eqnetrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
139		dm0rn0 5342	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	necon3bii 2846	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142		relxp 5227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143		relss 5206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	106, 142, 143	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145		relrn0 5383	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	145	necon3bid 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147	144, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
148	147	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
149	141, 148	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
150	149	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151		rpssre 11843	. . . . . . . . . . . . . . . . . . . . . . 23
152	111, 151	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		ltso 10118	. . . . . . . . . . . . . . . . . . . . . . 23
154		fiinfcl 8407	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ inf
155	153, 154	mpan 706	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ inf
156	125, 150, 152, 155	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ inf
157	111, 156	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ inf
158	105, 157	sylanl1 682	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ inf
159	158	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
160	82	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
161	160	anim1i 592	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	161	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$
164	127	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
165		eluni2 4440	. . . . . . . . . . . . . . . . . . . . . . 23
166	164, 165	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
167	166	biimpa 501	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
168	162, 163, 167	syl2an 494	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
170		nfra1 2941	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
171	169, 170	nfan 1828	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172		nfv 1843	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
173	171, 172	nfan 1828	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 inf
175		rspa 2930	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
176		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
177	176	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
178		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180	179	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
181	177, 180	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
182	181	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
183		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185	44	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	185	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188	187	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
189	182, 188	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
190	189	anandirs 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
191		prth 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
193	192	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
194	193	ad4ant23 1297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
195		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	195	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	110, 151	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
199	198	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
200		0re 10040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
201		rpge0 11845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
202	201	rgen 2922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
203		ssralv 3666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
204	110, 202, 203	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
205		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
206	205	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	206	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
208	200, 204, 207	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
209	208	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
210	144	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
211		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
212		fnfvelrn 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
213	211, 212	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		2ndrn 7216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
215	210, 213, 214	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
216		infrelb 11008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ inf
217	199, 209, 215, 216	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
218	217	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ inf
219	218	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
220	18	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
221		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
222	221	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
223	220, 222	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
226		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
227		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
228	215, 227	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
229		infrecl 11005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ inf
230	199, 228, 209, 229	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ inf
231	230	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ inf
232	225, 226, 231	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
233		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
234	233	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
235		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
237	236	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
238	237	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239		xrltletr 11988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ inf $/\$ inf $/\$ inf
240	224, 232, 238, 239	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$ inf
241	219, 240	mpan2d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
242	241	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
243	18	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
246		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
248	244, 226, 247	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
250	249	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
252	243, 248, 250, 251	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
253	252	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254	245, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
255	225, 254	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	255	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	256	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
258		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
259	18	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
260	225, 247	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261	255	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
262		elbl 22193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$
263	259, 260, 261, 262	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
264	258, 263	sylan9bbr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
265	264	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
266	265	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
267	266	impr 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
268	267	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
269	163	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
270		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
271	243, 248, 269, 270	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
272	254	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
273	244, 226, 272	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
274		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
275	271, 273, 274	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
276	268, 275	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
277	225	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
278	277, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
279		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
280	259, 278, 279, 270	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
281		xmetge0 22149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
282	259, 278, 279, 281	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
283		xrrege0 12005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$
284	283	an4s 869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$
285	284	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	280, 282, 285	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
287	286	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
288	257, 276, 287	mp2and 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
290		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
291	224, 238, 290	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
292		xmetge0 22149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
293	292	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
294	220, 293	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$
295	294	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
296	236	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
297	296	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
298		xrrege0 12005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$
299	298	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
300	224, 297, 299	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
301	295, 300	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
302	291, 301	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
303	302	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
304	303	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
305	289, 304	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
306	305	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
307	256, 256	rpaddcld 11887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
308	307	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
309	308	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
310		xmettri 22156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
311	243, 248, 250, 269, 310	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
312	311	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
313		rexadd 12063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
314	289, 304, 313	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
315	312, 314	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	257	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
317	268	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
318		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
319	289, 304, 316, 316, 317, 318	lt2addd 10650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
320	253, 306, 309, 315, 319	xrlelttrd 11991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
321	320	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
322	254	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
323	322, 254	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
324	244, 226, 323	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
325	271, 273, 308, 268, 324	xrlttrd 11990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
326	321, 325	jctild 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
327	242, 326	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$
328		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
329		heicant.d	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
330		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
331		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
332	330, 331	anim12dan 882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
333		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
334	333	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
335	329, 332, 334	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
336	335	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
337	328, 336	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
338	337	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
339	329	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
340		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
341	340, 278	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
342		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
343	342	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
344	343	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$
345	344	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
346		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
347	339, 341, 345, 346	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
348	9	rpxrd 11873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
349	348	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
350		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
351	347, 349, 350	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
352		xmetge0 22149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
353	339, 341, 345, 352	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
354	9	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
355	354	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
356		xrrege0 12005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$
357	356	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
358	347, 355, 357	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
359	353, 358	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
360	351, 359	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
361	360	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
362	361	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
363	342	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
364	363	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$ $/\$
365	364	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
366		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
367	339, 341, 365, 366	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
368		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
369	367, 349, 368	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
370		xmetge0 22149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
371	339, 341, 365, 370	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
372		xrrege0 12005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$
373	372	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
374	367, 355, 373	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
375	371, 374	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
376	369, 375	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
377	376	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
378	377	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
379		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
380	362, 378, 379	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
381	380	anandis 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
382	381	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
383		rpxr 11840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	383	ad6antlr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
385		xmettri 22156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
386	339, 345, 365, 341, 385	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
387	386	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
388	387	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
389		xmetsym 22152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
390	339, 345, 341, 389	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
391	390	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
392	391	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
393	392	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
394		rexadd 12063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
395	362, 378, 394	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
396	395	anandis 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
397	393, 396	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
398	388, 397	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
399		lt2add 10513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
400	399	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
401	355, 355, 400	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
402	360, 376, 401	syl2and 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
403	402	pm2.43d 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
404	403	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
405	404	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
406		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
407	406	2halvesd 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
408	407	ad6antlr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
409	405, 408	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
410	338, 382, 384, 398, 409	xrlelttrd 11991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
411	410	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
412	327, 411	imim12d 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
413	197, 412	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
414	413	adantlrr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
415	194, 414	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
416	415	exp32 631	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
417	175, 416	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
418	417	expr 643	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
419	418	pm2.43d 53	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
420	419	an32s 846	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
421	173, 174, 420	rexlimd 3026	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
422	168, 421	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
423	422	ralrimivva 2971	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ inf
424		breq2 4657	. . . . . . . . . . . . . . . . . . . . 21 inf inf
425	424	imbi1d 331	. . . . . . . . . . . . . . . . . . . 20 inf inf
426	425	2ralbidv 2989	. . . . . . . . . . . . . . . . . . 19 inf inf
427	426	rspcev 3309	. . . . . . . . . . . . . . . . . 18 inf $/\$ inf
428	159, 423, 427	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
429	428	expl 648	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
430	429	exlimdv 1861	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
431	430	expimpd 629	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
432	103, 431	sylan2 491	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
433	432	rexlimdva 3031	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
434	102, 433	syld 47	. . . . . . . . . . 11 $/\$ $/\$
435	15, 434	syl5 34	. . . . . . . . . 10 $/\$ $/\$ $/\$
436	435	exp4b 632	. . . . . . . . 9 $/\$
437	9, 436	mpdi 45	. . . . . . . 8 $/\$
438	437	ralrimiv 2965	. . . . . . 7 $/\$
439		r19.21v 2960	. . . . . . 7
440	438, 439	sylib 208	. . . . . 6 $/\$
441	8, 440	impbid2 216	. . . . 5 $/\$
442		ralcom 3098	. . . . 5
443	441, 442	syl6bb 276	. . . 4 $/\$
444	443	pm5.32da 673	. . 3 $/\$ $/\$
445		eqid 2622	. . . 4 metUnif metUnif
446		eqid 2622	. . . 4 metUnif metUnif
447		heicant.y	. . . 4
448		xmetpsmet 22153	. . . . 5 PsMet
449	18, 448	syl 17	. . . 4 PsMet
450		xmetpsmet 22153	. . . . 5 PsMet
451	329, 450	syl 17	. . . 4 PsMet
452	445, 446, 129, 447, 449, 451	metucn 22376	. . 3 metUnif Cn_umetUnif $/\$
453		eqid 2622	. . . . 5
454	23, 453	metcn 22348	. . . 4 $/\$ $/\$
455	18, 329, 454	syl2anc 693	. . 3 $/\$
456	444, 452, 455	3bitr4d 300	. 2 metUnif Cn_umetUnif
457	456	eqrdv 2620	1 metUnif Cn_umetUnif

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

cin 3573

wss 3574

c0 3915

cpw 4158

cop 4183

cuni 4436 class class class wbr 4653

wor 5034

cxp 5112

cdm 5114

crn 5115

wrel 5119

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

c1st 7166

c2nd 7167

cen 7952

cfn 7955 infcinf 8347

cr 9935

cc0 9936

caddc 9939

cxr 10073

clt 10074

cle 10075

cdiv 10684

c2 11070

crp 11832

cxad 11944 PsMetcpsmet 19730

cxmt 19731

cbl 19733

cmopn 19736 metUnifcmetu 19737

ccn 21028

ccmp 21189 Cn_ucucn 22079

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ico 12181 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-metu 19745 df-top 20699 df-topon 20716 df-bases 20750 df-cn 21031 df-cnp 21032 df-cmp 21190 df-fil 21650 df-ust 22004 df-ucn 22080

This theorem is referenced by: (None)

W3C validator