icccncfext - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > icccncfext		Structured version Visualization version Unicode version

Theorem icccncfext 40100

Description: A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
icccncfext.1
icccncfext.2
icccncfext.3
icccncfext.4
icccncfext.5
icccncfext.6
icccncfext.7
icccncfext.8
icccncfext.9	↾_t

**Assertion**
Ref	Expression
icccncfext	↾_t $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem icccncfext Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		icccncfext.2	. . . . . . . . . . . 12
2		retopon 22567	. . . . . . . . . . . 12 TopOn
3	1, 2	eqeltri 2697	. . . . . . . . . . 11 TopOn
4		icccncfext.5	. . . . . . . . . . . 12
5		icccncfext.6	. . . . . . . . . . . 12
6	4, 5	iccssred 39727	. . . . . . . . . . 11
7		resttopon 20965	. . . . . . . . . . 11 TopOn $/\$ ↾_t TopOn
8	3, 6, 7	sylancr 695	. . . . . . . . . 10 ↾_t TopOn
9		icccncfext.8	. . . . . . . . . . . 12
10		icccncfext.3	. . . . . . . . . . . 12
11	9, 10	jctir 561	. . . . . . . . . . 11 $/\$
12		istopon 20717	. . . . . . . . . . 11 TopOn $/\$
13	11, 12	sylibr 224	. . . . . . . . . 10 TopOn
14		icccncfext.9	. . . . . . . . . 10 ↾_t
15		cnf2 21053	. . . . . . . . . 10 ↾_t TopOn $/\$ TopOn $/\$ ↾_t
16	8, 13, 14, 15	syl3anc 1326	. . . . . . . . 9
17		ffn 6045	. . . . . . . . 9
18	16, 17	syl 17	. . . . . . . 8
19		dffn3 6054	. . . . . . . 8
20	18, 19	sylib 208	. . . . . . 7
21	20	ffvelrnda 6359	. . . . . 6 $/\$
22		fnfun 5988	. . . . . . . . . 10
23	18, 22	syl 17	. . . . . . . . 9
24	4	rexrd 10089	. . . . . . . . . . 11
25	5	rexrd 10089	. . . . . . . . . . 11
26		icccncfext.7	. . . . . . . . . . 11
27		lbicc2 12288	. . . . . . . . . . 11 $/\$ $/\$
28	24, 25, 26, 27	syl3anc 1326	. . . . . . . . . 10
29		fndm 5990	. . . . . . . . . . . 12
30	18, 29	syl 17	. . . . . . . . . . 11
31	30	eqcomd 2628	. . . . . . . . . 10
32	28, 31	eleqtrd 2703	. . . . . . . . 9
33		fvelrn 6352	. . . . . . . . 9 $/\$
34	23, 32, 33	syl2anc 693	. . . . . . . 8
35		ubicc2 12289	. . . . . . . . . . 11 $/\$ $/\$
36	24, 25, 26, 35	syl3anc 1326	. . . . . . . . . 10
37	36, 31	eleqtrd 2703	. . . . . . . . 9
38		fvelrn 6352	. . . . . . . . 9 $/\$
39	23, 37, 38	syl2anc 693	. . . . . . . 8
40	34, 39	ifcld 4131	. . . . . . 7
41	40	adantr 481	. . . . . 6 $/\$
42	21, 41	ifclda 4120	. . . . 5
43	42	adantr 481	. . . 4 $/\$
44		icccncfext.4	. . . . 5
45		nfv 1843	. . . . . . 7
46		nfcv 2764	. . . . . . 7
47		nfcv 2764	. . . . . . 7
48	45, 46, 47	nfif 4115	. . . . . 6
49		nfv 1843	. . . . . . 7
50		icccncfext.1	. . . . . . . 8
51		nfcv 2764	. . . . . . . 8
52	50, 51	nffv 6198	. . . . . . 7
53		nfv 1843	. . . . . . . 8
54		nfcv 2764	. . . . . . . . 9
55	50, 54	nffv 6198	. . . . . . . 8
56		nfcv 2764	. . . . . . . . 9
57	50, 56	nffv 6198	. . . . . . . 8
58	53, 55, 57	nfif 4115	. . . . . . 7
59	49, 52, 58	nfif 4115	. . . . . 6
60		eleq1 2689	. . . . . . 7
61		fveq2 6191	. . . . . . 7
62		breq1 4656	. . . . . . . 8
63	62	ifbid 4108	. . . . . . 7
64	60, 61, 63	ifbieq12d 4113	. . . . . 6
65	48, 59, 64	cbvmpt 4749	. . . . 5
66	44, 65	eqtri 2644	. . . 4
67	43, 66	fmptd 6385	. . 3
68	67	adantr 481	. . . . 5 $/\$
69		simplll 798	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$
70		simplr 792	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$ ↾_t
71	69, 70	jca 554	. . . . . . . . . 10 $/\$ $/\$ ↾_t $/\$ $/\$ ↾_t
72		ssid 3624	. . . . . . . . . . . . . 14
73	72	a1i 11	. . . . . . . . . . . . 13
74		frn 6053	. . . . . . . . . . . . . 14
75	16, 74	syl 17	. . . . . . . . . . . . 13
76		cnrest2 21090	. . . . . . . . . . . . 13 TopOn $/\$ $/\$ ↾_t ↾_t ↾_t
77	13, 73, 75, 76	syl3anc 1326	. . . . . . . . . . . 12 ↾_t ↾_t ↾_t
78	14, 77	mpbid 222	. . . . . . . . . . 11 ↾_t ↾_t
79	78	anim1i 592	. . . . . . . . . 10 $/\$ ↾_t ↾_t ↾_t $/\$ ↾_t
80		cnima 21069	. . . . . . . . . 10 ↾_t ↾_t $/\$ ↾_t ↾_t
81	71, 79, 80	3syl 18	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ ↾_t
82		retop 22565	. . . . . . . . . . . . . 14
83	1, 82	eqeltri 2697	. . . . . . . . . . . . 13
84	83	a1i 11	. . . . . . . . . . . 12
85		reex 10027	. . . . . . . . . . . . . 14
86	85	a1i 11	. . . . . . . . . . . . 13
87	86, 6	ssexd 4805	. . . . . . . . . . . 12
88	84, 87	jca 554	. . . . . . . . . . 11 $/\$
89	69, 88	syl 17	. . . . . . . . . 10 $/\$ $/\$ ↾_t $/\$ $/\$
90		elrest 16088	. . . . . . . . . 10 $/\$ ↾_t
91	89, 90	syl 17	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ ↾_t
92	81, 91	mpbid 222	. . . . . . . 8 $/\$ $/\$ ↾_t $/\$
93	69	3ad2ant1 1082	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$ $/\$ $/\$
94		simpllr 799	. . . . . . . . . . . 12 $/\$ $/\$ ↾_t $/\$
95	94	3ad2ant1 1082	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$ $/\$ $/\$
96		simp1r 1086	. . . . . . . . . . 11 $/\$ $/\$ ↾_t $/\$ $/\$ $/\$
97	93, 95, 96	jca31 557	. . . . . . . . . 10 $/\$ $/\$ ↾_t $/\$ $/\$ $/\$ $/\$ $/\$
98		simpll2 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		iooretop 22569	. . . . . . . . . . . . . . . . 17
100	99, 1	eleqtrri 2700	. . . . . . . . . . . . . . . 16
101		iooretop 22569	. . . . . . . . . . . . . . . . 17
102	101, 1	eleqtrri 2700	. . . . . . . . . . . . . . . 16
103		unopn 20708	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	83, 100, 102, 103	mp3an 1424	. . . . . . . . . . . . . . 15
105		unopn 20708	. . . . . . . . . . . . . . 15 $/\$ $/\$
106	83, 104, 105	mp3an13 1415	. . . . . . . . . . . . . 14
107	98, 106	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpl1l 1112	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110		simpl1r 1113	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
111	110	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112		simpll3 1102	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		difreicc 12304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $\$
114	4, 5, 113	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
115	114	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
116	115	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
117	116	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
118	117	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$
119		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$
120	118, 119	sylnib 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
121		imnan 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
122	120, 121	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
123	122	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
124	123	notnotrd 128	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
125	124	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
126	125	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
127		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
128	6	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
129	16	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
130	129	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
131	16, 28	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
132	131	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
133	16, 36	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
134	133	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
135	132, 134	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
136	130, 135	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
137	66	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
138	128, 136, 137	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
139		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
140	139	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
141	138, 140	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
142	141	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
143	127, 126, 142	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
144		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
145	143, 144	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
146	127, 18	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
147		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
149	126, 145, 148	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
150	149	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
151		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
152	150, 151	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
153		elin 3796	. . . . . . . . . . . . . . . . . . . 20 $/\$
154	152, 153	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	simpld 475	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
156	155	ex 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
157	156	orrd 393	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\/$
158	157	orcomd 403	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\/$
159		elun 3753	. . . . . . . . . . . . . . 15 $\/$
160	158, 159	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
161	109, 111, 112, 160	syl21anc 1325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162		imaundi 5545	. . . . . . . . . . . . . 14
163	109	simpld 475	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164		toponss 20731	. . . . . . . . . . . . . . . . . . 19 TopOn $/\$
165	3, 98, 164	sylancr 695	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	163, 165, 112	jca31 557	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		simplr 792	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169	44	funmpt2 5927	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
171	170	ad5antr 770	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
172		fvelima 6248	. . . . . . . . . . . . . . . . . . . . 21 $/\$
173	171, 172	sylancom 701	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
174		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . 24
175	174	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . 23
176	175	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177		simp1ll 1124	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		simp1lr 1125	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	180, 181, 182	jca31 557	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
185	184	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
186		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
187		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
188	186, 187	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
189	185, 188	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
190	189, 141	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
191	190	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
192	191	adantlllr 39199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
193		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
194		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
195		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
196		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
197	195, 196	elind 3798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
198		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
199	198	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
200	199	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
201	197, 200	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
202	201	adantlllr 39199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
203		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
204	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
205		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
207	203, 206	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
208	207	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
209	193, 194, 202, 208	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
210	192, 209	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
211	183, 210	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
212		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
213		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
214	212, 213	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
215		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
216		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
217		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
218	216, 217	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
219	214, 215, 218	jca31 557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
221		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
222	221	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
223	184, 187, 222	ifeq123d 39207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
224	223	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
225		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
226		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
227	226	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
228		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
229		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
230	228, 229	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
231	227, 230	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
232	220, 224, 225, 231	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
233	232, 227	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
234	233, 230	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
235	219, 234	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
236	235	adantl4r 787	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
237	211, 236	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
238	177, 178, 179, 237	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239	176, 238	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
240	239	rexlimdv3a 3033	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
241	173, 240	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
242	241	ex 450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
243	242	alrimiv 1855	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
244	166, 167, 168, 243	syl21anc 1325	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		dfss2 3591	. . . . . . . . . . . . . . . 16
246	244, 245	sylibr 224	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247		imaundi 5545	. . . . . . . . . . . . . . . . 17
248	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
249		fvelima 6248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
250	248, 249	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
251		simp1l 1085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
252		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
253		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
254	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	223	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
256		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
257	256	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
258		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
259	258	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
260	259	simprrd 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
261	260	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
262		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
263	256, 4, 262	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
264	261, 263	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
265	264	intn3an2d 1443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
266	4, 5	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
267	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
268		elicc2 12238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
269	267, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
270	265, 269	mtbird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
271	270	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
272	260	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
273	272	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
274	271, 273	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
275	131	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
276	274, 275	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
277	254, 255, 257, 276	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
278	277	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
279		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
280	274	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
281	278, 279, 280	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
282	251, 252, 253, 281	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
283	282	rexlimdv3a 3033	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
284	250, 283	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
285		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . 24
286	284, 285	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
287	286	ex 450	. . . . . . . . . . . . . . . . . . . . . 22
288	287	ssrdv 3609	. . . . . . . . . . . . . . . . . . . . 21
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
290		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
291	290	snssd 4340	. . . . . . . . . . . . . . . . . . . 20 $/\$
292	289, 291	sstrd 3613	. . . . . . . . . . . . . . . . . . 19 $/\$
293	292	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
294		fvelima 6248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
295	170, 294	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
296		simp1l 1085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
297		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
298		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
299	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
300	223	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
301		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
302	301	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
303	16	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
304	303	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
305	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
306	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
307	26	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
308		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
309	308	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
310	309	simprld 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
311	310	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
312	305, 306, 302, 307, 311	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
313	305, 302, 312	ltnsymd 10186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
314	313	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
315	133	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
316	314, 315	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
317	316	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
318	304, 317	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
319	299, 300, 302, 318	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
320	319	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
321		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
322	306, 302	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
323	311, 322	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
324	323	intn3an3d 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
325	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
326	325, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
327	324, 326	mtbird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
328	327	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
329	328, 314	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
330	329	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
331	320, 321, 330	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
332	296, 297, 298, 331	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
333	332	rexlimdv3a 3033	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
334	295, 333	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
335		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . 24
336	334, 335	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
337	336	ex 450	. . . . . . . . . . . . . . . . . . . . . 22
338	337	ssrdv 3609	. . . . . . . . . . . . . . . . . . . . 21
339	338	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
340		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
341	340	snssd 4340	. . . . . . . . . . . . . . . . . . . 20 $/\$
342	339, 341	sstrd 3613	. . . . . . . . . . . . . . . . . . 19 $/\$
343	342	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
344	293, 343	unssd 3789	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
345	247, 344	syl5eqss 3649	. . . . . . . . . . . . . . . 16 $/\$ $/\$
346	163, 167, 168, 345	syl21anc 1325	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
347	246, 346	unssd 3789	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
348	162, 347	syl5eqss 3649	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
349		eleq2 2690	. . . . . . . . . . . . . . 15
350		imaeq2 5462	. . . . . . . . . . . . . . . 16
351	350	sseq1d 3632	. . . . . . . . . . . . . . 15
352	349, 351	anbi12d 747	. . . . . . . . . . . . . 14 $/\$ $/\$
353	352	rspcev 3309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
354	107, 161, 348, 353	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
355	83	a1i 11	. . . . . . . . . . . . . . . 16
356		iooretop 22569	. . . . . . . . . . . . . . . . . 18
357	356, 1	eleqtrri 2700	. . . . . . . . . . . . . . . . 17
358		inopn 20704	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
359	83, 357, 358	mp3an13 1415	. . . . . . . . . . . . . . . 16
360	100	a1i 11	. . . . . . . . . . . . . . . 16
361		unopn 20708	. . . . . . . . . . . . . . . 16 $/\$ $/\$
362	355, 359, 360, 361	syl3anc 1326	. . . . . . . . . . . . . . 15
363	362	3ad2ant2 1083	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
364	363	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
365		simpll1 1100	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
366		simpll3 1102	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
367		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
368		simpll 790	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
369	266	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
370		eqimss 3657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
371	113, 370	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
372		difcom 4053	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
373	371, 372	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
374	369, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
375	374	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
376		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
377		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
378		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
379	378	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
380		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
381	380	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$
382	381	simprld 795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
383	382	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
384	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
385	384, 379	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
386	383, 385	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
387	386	intn3an3d 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
388	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
389		elicc2 12238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
390	388, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
391	387, 390	mtbird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
392	391	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
393	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
394	26	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
395	393, 384, 379, 394, 383	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
396	393, 379, 395	ltnsymd 10186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
397	396	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
398	392, 397	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
399	133	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
400	398, 399	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
401	379, 400, 137	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
402	401, 398	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
403	402	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
404	403	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
405		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
406	404, 405	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
407	406	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
408	407	stoic1a 1697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
409	408	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
410		ioran 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $/\$
411	377, 409, 410	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\/$
412		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
413	411, 412	sylnibr 319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
414	376, 413	eldifd 3585	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
415	375, 414	sseldd 3604	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
416	415	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
417		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
418		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
419		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
420		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
421	142	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
422		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
423	421, 422	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
424	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
425	424, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
426	420, 423, 425	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
427	417, 418, 419, 426	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
428		simplr 792	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
429	427, 428	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
430		elinel1 3799	. . . . . . . . . . . . . . . . . . . . 21
431	429, 430	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
432	368, 416, 431	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
433		simp-4l 806	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
434		simp-4r 807	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
435		simplr 792	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
436		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
437		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
438	36	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
439	437, 438	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
440	436, 439, 141	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
441	437	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
442	440, 441	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
443	442	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
444		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
445	25	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
446		pnfxr 10092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
447	446	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
448		rexr 10085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
449	448	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
450	445, 447, 449	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
451	450	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
452		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
453	452	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
454		mnfxr 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
455	454	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
456	455, 445, 449	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
457		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$
458	457	notbii 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
459	458	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
460	459	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
461		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
462	460, 461	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
463	456, 462	mpidan 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
464		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
465	463, 464	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
466	453, 465	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
467	466	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
468		pm4.56 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\/$
469	467, 468	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\/$
470		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
471	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
472	470, 471	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
473	472	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
474		leloe 10124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\/$
475	473, 474	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $\/$
476	469, 475	mtbird 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
477	5	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
478	477	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
479		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
480	478, 479	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
481	476, 480	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
482		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
483	482	ltpnfd 11955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
484	481, 483	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
485	451, 484, 380	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
486	444, 485, 402	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
487	443, 486	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
488	487	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
489	488	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
490		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
491	489, 490	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
492	491	stoic1a 1697	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
493	492	notnotrd 128	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
494	433, 434, 435, 493	syl21anc 1325	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
495	432, 494	elind 3798	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
496	495	ex 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
497	496	orrd 393	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\/$
498	497	orcomd 403	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\/$
499		elun 3753	. . . . . . . . . . . . . . 15 $\/$
500	498, 499	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
501	365, 366, 367, 500	syl21anc 1325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
502	108	simpld 475	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
503	502	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
504		simpll2 1101	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
505	3, 504, 164	sylancr 695	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
506	503, 505	jca 554	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
507		simplr 792	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
508		ffn 6045	. . . . . . . . . . . . . . . . . 18
509	67, 508	syl 17	. . . . . . . . . . . . . . . . 17
510	509	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
511		ssinss1 3841	. . . . . . . . . . . . . . . . 17
512	511	ad3antlr 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
513		ioossre 12235	. . . . . . . . . . . . . . . . 17
514	513	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
515		unima 39346	. . . . . . . . . . . . . . . 16 $/\$ $/\$
516	510, 512, 514, 515	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
517	169	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
518		fvelima 6248	. . . . . . . . . . . . . . . . . . . 20 $/\$
519	517, 518	sylancom 701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
520	175	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
521		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
522		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
523		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
524	277, 271, 273	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
525	524	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
526		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
527	525, 526	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
528	521, 522, 523, 527	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
529		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
530		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
531		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
532		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
533		elinel1 3799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
534	533	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
535		elinel2 3800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
536		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
537	535, 536	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
538	537	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
539	24	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
540	538	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
541		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
542	538, 541	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
543	454	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
544	543, 539, 540	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
545		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
546	545, 258	sylnib 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
547		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
548	546, 547	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
549	544, 548	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
550		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
551	549, 550	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
552	542, 551	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
553	539, 540, 552	xrnltled 10106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
554		simp1 1061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
555	535	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
556	536	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
557	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
558		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
559	558	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
560	559	simprrd 797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
561	560	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
562	556, 557, 561	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
563	554, 555, 562	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
564	266	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
565	564, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
566	538, 553, 563, 565	mpbir3and 1245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
567	534, 566	elind 3798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
568	530, 531, 532, 567	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
569		elinel2 3800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
570	569	anim2i 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
571	570	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
572	571, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
573	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
574		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
575	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
576	574, 575	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
577	576	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
578	205	simplbda 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
579	573, 577, 578	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
580	572, 579	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
581	580	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
582	529, 568, 581	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
583	528, 582	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
584	583	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
585	520, 584	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
586	585	3adant1r 1319	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
587	586	rexlimdv3a 3033	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
588	519, 587	mpd 15	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
589	588	ex 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
590	589	ssrdv 3609	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
591	292	ad4ant14 1293	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
592	590, 591	unssd 3789	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
593	516, 592	eqsstrd 3639	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
594	506, 366, 507, 593	syl21anc 1325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
595		eleq2 2690	. . . . . . . . . . . . . . 15
596		imaeq2 5462	. . . . . . . . . . . . . . . 16
597	596	sseq1d 3632	. . . . . . . . . . . . . . 15
598	595, 597	anbi12d 747	. . . . . . . . . . . . . 14 $/\$ $/\$
599	598	rspcev 3309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
600	364, 501, 594, 599	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
601	354, 600	pm2.61dan 832	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
602		simpll2 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
603		iooretop 22569	. . . . . . . . . . . . . . . . 17
604	603, 1	eleqtrri 2700	. . . . . . . . . . . . . . . 16
605		inopn 20704	. . . . . . . . . . . . . . . 16 $/\$ $/\$
606	83, 604, 605	mp3an13 1415	. . . . . . . . . . . . . . 15
607	102	a1i 11	. . . . . . . . . . . . . . 15
608		unopn 20708	. . . . . . . . . . . . . . 15 $/\$ $/\$
609	355, 606, 607, 608	syl3anc 1326	. . . . . . . . . . . . . 14
610	602, 609	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
611		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
612	611	simpld 475	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
613	612	simpld 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
614		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
615		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
616		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
617		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
618	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
619	455, 618, 449	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
620	619	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
621	452	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
622	621	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
623		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
624	620, 622, 623	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
625		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
626	625	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
627		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
628	627	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
629	626, 628	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
630	629, 524	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
631	617, 624, 630	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
632	631	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
633	632	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
634		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
635	633, 634	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
636		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
637	635, 636	pm2.65da 600	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
638	4	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
639	638	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
640		lenlt 10116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
641	639, 640	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
642	637, 641	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
643	611, 616, 642	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
644		ltpnf 11954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
645	644	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
646	450	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
647	380	notbii 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
648	647	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
649	648	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
650		imnan 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
651	649, 650	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
652	646, 651	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
653		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
654	652, 653	sylnib 318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
655		imnan 438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
656	654, 655	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
657	645, 656	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
658	472	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
659		lenlt 10116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
660	658, 659	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
661	657, 660	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
662	612, 661	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
663	266	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
664	663, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
665	615, 643, 662, 664	mpbir3and 1245	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
666	613, 614, 665, 426	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
667		simpllr 799	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
668	666, 667	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
669	668, 430	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
670		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
671	28	ancli 574	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
672		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
673	672	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
674		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
675	670, 674	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
676	673, 675	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
677	676, 141	vtoclg 3266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
678	4, 671, 677	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
679	670, 678	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
680	679	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
681		simplll 798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
682	619	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
683	452	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
684		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
685	681, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
686	449	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
687	24	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
688	644	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
689		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
690	446	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
691	687, 690, 686	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
692		elioo3g 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
693	692	notbii 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
694	693	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
695		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
696	694, 695	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
697	689, 691, 696	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
698		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
699	697, 698	sylnib 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
700		nan 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
701	699, 700	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
702	688, 701	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
703	686, 687, 702	xrnltled 10106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
704	703	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
705		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
706	705	necomd 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
707	706	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
708	684, 685, 704, 707	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
709	683, 708	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
710	682, 709, 623	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
711	681, 710, 630	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
712	680, 711	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
713	712	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
714	713	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
715		simpllr 799	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
716	714, 715	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
717		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
718	716, 717	condan 835	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
719	611, 616, 718	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
720	669, 719	elind 3798	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
721	720	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
722		pm5.6 951	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
723	721, 722	mpbi 220	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
724	723	orcomd 403	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
725		elun 3753	. . . . . . . . . . . . . . 15 $\/$
726	724, 725	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
727	726	3adantll2 39202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
728		simp1ll 1124	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
729	728	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
730		simpll3 1102	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
731		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
732	509	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$
733		ioossre 12235	. . . . . . . . . . . . . . . . . . 19
734	733	olci 406	. . . . . . . . . . . . . . . . . 18 $\/$
735		inss 3842	. . . . . . . . . . . . . . . . . 18 $\/$
736	734, 735	ax-mp 5	. . . . . . . . . . . . . . . . 17
737	736	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
738		ioossre 12235	. . . . . . . . . . . . . . . . 17
739	738	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
740		unima 39346	. . . . . . . . . . . . . . . 16 $/\$ $/\$
741	732, 737, 739, 740	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$
742		simpll 790	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
743	736	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . 26
744	743	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
745	742, 744, 450	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
746		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
747	743	ltpnfd 11955	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
748	747	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
749	746, 748	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
750	749	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
751	745, 750, 380	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
752	742, 751, 402	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
753	752	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
754		simpllr 799	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
755	753, 754	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
756	755	adantlllr 39199	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
757		simp-4l 806	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
758		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
759		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
760		simpll 790	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
761	743	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
762	761	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
763	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
764		elinel2 3800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
765	692	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
766	765	simprld 795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
767	764, 766	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
768	767	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
769	763, 761, 768	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
770	769	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
771		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
772	760, 762, 472	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
773	772, 659	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
774	771, 773	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
775	266	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
776	775, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
777	762, 770, 774, 776	mpbir3and 1245	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
778	760, 777, 141	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
779	757, 758, 759, 778	syl21anc 1325	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
780		elinel1 3799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
781	780	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
782	781, 777	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
783	782	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
784	783, 153	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
785	199	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
786	784, 785	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
787	18	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
788	787, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
789	786, 788	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
790	789	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
791	790	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
792	779, 791	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
793	756, 792	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
794	793	ralrimiva 2966	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
795		fndm 5990	. . . . . . . . . . . . . . . . . . . . . 22
796	509, 795	syl 17	. . . . . . . . . . . . . . . . . . . . 21
797	736, 796	syl5sseqr 3654	. . . . . . . . . . . . . . . . . . . 20
798	170, 797	jca 554	. . . . . . . . . . . . . . . . . . 19 $/\$
799	798	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
800		funimass4 6247	. . . . . . . . . . . . . . . . . 18 $/\$
801	799, 800	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
802	794, 801	mpbird 247	. . . . . . . . . . . . . . . 16 $/\$ $/\$
803	342	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$
804	802, 803	unssd 3789	. . . . . . . . . . . . . . 15 $/\$ $/\$
805	741, 804	eqsstrd 3639	. . . . . . . . . . . . . 14 $/\$ $/\$
806	729, 730, 731, 805	syl21anc 1325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
807		eleq2 2690	. . . . . . . . . . . . . . 15
808		imaeq2 5462	. . . . . . . . . . . . . . . 16
809	808	sseq1d 3632	. . . . . . . . . . . . . . 15
810	807, 809	anbi12d 747	. . . . . . . . . . . . . 14 $/\$ $/\$
811	810	rspcev 3309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
812	610, 727, 806, 811	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
813		simpll2 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
814		iooretop 22569	. . . . . . . . . . . . . . . 16
815	814, 1	eleqtrri 2700	. . . . . . . . . . . . . . 15
816		inopn 20704	. . . . . . . . . . . . . . 15 $/\$ $/\$
817	83, 815, 816	mp3an13 1415	. . . . . . . . . . . . . 14
818	813, 817	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
819		simp-4r 807	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
820	642	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
821		simpll 790	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
822	821, 408, 661	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
823	822	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
824		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
825	824, 266	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
826	825, 389	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
827	819, 820, 823, 826	mpbir3and 1245	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
828	827	adantllr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
829	824, 827, 141	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
830	829	adantllr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
831		simp-4r 807	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
832	830, 831	eqeltrrd 2702	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
833		simp-5l 808	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
834	833, 18	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
835	834, 147	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
836	828, 832, 835	mpbir2and 957	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
837		simpllr 799	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
838	836, 837	eleqtrd 2703	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
839	838, 430	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
840		simp-5r 809	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
841	833, 840, 828	jca31 557	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
842		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
843	832, 842	jca 554	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
844		nelneq 2725	. . . . . . . . . . . . . . . . 17 $/\$
845	674	necon3bi 2820	. . . . . . . . . . . . . . . . 17
846	843, 844, 845	3syl 18	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
847		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
848	832, 847	jca 554	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
849		nelneq 2725	. . . . . . . . . . . . . . . . 17 $/\$
850		fveq2 6191	. . . . . . . . . . . . . . . . . 18
851	850	necon3bi 2820	. . . . . . . . . . . . . . . . 17
852	848, 849, 851	3syl 18	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
853	618	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
854	445	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
855	448	ad4antlr 769	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
856	853, 854, 855	3jca 1242	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
857		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
858	4	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
859		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
860	266	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
861	860, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
862	139, 861	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
863	862	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
864	863	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
865	858, 859, 864	3jca 1242	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
866	865	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
867		leltne 10127	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
868	866, 867	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
869	857, 868	mpbird 247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
870	869	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
871		necom 2847	. . . . . . . . . . . . . . . . . . . . . 22
872	871	biimpi 206	. . . . . . . . . . . . . . . . . . . . 21
873	872	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
874	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
875	862	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
876	875	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
877	859, 874, 876	3jca 1242	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
878	877	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
879		leltne 10127	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
880	878, 879	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
881	873, 880	mpbird 247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
882	881	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
883	870, 882	jca 554	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
884		elioo3g 12204	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
885	856, 883, 884	sylanbrc 698	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
886	841, 846, 852, 885	syl21anc 1325	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
887	839, 886	elind 3798	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
888	887	3adantll2 39202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
889	169	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
890		fvelima 6248	. . . . . . . . . . . . . . . . . . . 20 $/\$
891	889, 890	sylancom 701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
892		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
893		simp1l 1085	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
894		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
895		ioossicc 12259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
896	894, 895	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
897	896	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . 26
898	897	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
899	893, 898, 141	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
900		sslin 3839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
901	895, 900	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
902	901	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
903	902	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
904	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
905	903, 904	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
906	905	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
907	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
908	907, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
909	906, 908	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
910	909	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
911	910	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
912	899, 911	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
913	892, 912	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
914	913	3exp 1264	. . . . . . . . . . . . . . . . . . . . 21 $/\$
915	914	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
916	915	rexlimdv 3030	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
917	891, 916	mpd 15	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
918	917	ralrimiva 2966	. . . . . . . . . . . . . . . . 17 $/\$
919		dfss3 3592	. . . . . . . . . . . . . . . . 17
920	918, 919	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$
921	920	ad4ant14 1293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
922	921	3adant2 1080	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
923	922	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
924		eleq2 2690	. . . . . . . . . . . . . . 15
925		imaeq2 5462	. . . . . . . . . . . . . . . 16
926	925	sseq1d 3632	. . . . . . . . . . . . . . 15
927	924, 926	anbi12d 747	. . . . . . . . . . . . . 14 $/\$ $/\$
928	927	rspcev 3309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
929	818, 888, 923, 928	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
930	812, 929	pm2.61dan 832	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
931	601, 930	pm2.61dan 832	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
932	97, 931	syld3an1 1372	. . . . . . . . 9 $/\$ $/\$ ↾_t $/\$ $/\$ $/\$ $/\$
933	932	rexlimdv3a 3033	. . . . . . . 8 $/\$ $/\$ ↾_t $/\$ $/\$
934	92, 933	mpd 15	. . . . . . 7 $/\$ $/\$ ↾_t $/\$ $/\$
935	934	ex 450	. . . . . 6 $/\$ $/\$ ↾_t $/\$
936	935	ralrimiva 2966	. . . . 5 $/\$ ↾_t $/\$
937	3	a1i 11	. . . . . 6 $/\$ TopOn
938		resttopon 20965	. . . . . . . 8 TopOn $/\$ ↾_t TopOn
939	13, 75, 938	syl2anc 693	. . . . . . 7 ↾_t TopOn
940	939	adantr 481	. . . . . 6 $/\$ ↾_t TopOn
941		iscnp 21041	. . . . . 6 TopOn $/\$ ↾_t TopOn $/\$ ↾_t $/\$ ↾_t $/\$
942	937, 940, 470, 941	syl3anc 1326	. . . . 5 $/\$ ↾_t $/\$ ↾_t $/\$
943	68, 936, 942	mpbir2and 957	. . . 4 $/\$ ↾_t
944	943	ralrimiva 2966	. . 3 ↾_t
945		cncnp 21084	. . . 4 TopOn $/\$ ↾_t TopOn ↾_t $/\$ ↾_t
946	3, 939, 945	sylancr 695	. . 3 ↾_t $/\$ ↾_t
947	67, 944, 946	mpbir2and 957	. 2 ↾_t
948		fnssres 6004	. . . 4 $/\$
949	509, 6, 948	syl2anc 693	. . 3
950		fvres 6207	. . . . 5
951	950	adantl 482	. . . 4 $/\$
952	951, 141	eqtrd 2656	. . 3 $/\$
953	949, 18, 952	eqfnfvd 6314	. 2
954	947, 953	jca 554	1 ↾_t $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wal 1481

wceq 1483

wcel 1990

wnfc 2751

wne 2794

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

cif 4086

csn 4177

cuni 4436 class class class wbr 4653

cmpt 4729

ccnv 5113

cdm 5114

crn 5115

cres 5116

cima 5117

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cr 9935

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cioo 12175

cicc 12178 ↾_t crest 16081

ctg 16098

ctop 20698 TopOnctopon 20715

ccn 21028

ccnp 21029

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-rep 4771 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-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 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-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-ioo 12179 df-icc 12182 df-rest 16083 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-cn 21031 df-cnp 21032

This theorem is referenced by: itgsubsticclem 40191

W3C validator