poimirlem3 - Mathbox for Brendan Leahy

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

Theorem poimirlem3 31857

Description: Lemma for poimir 31887 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem4.1
poimirlem4.2
poimirlem4.3
poimirlem3.4	..^
poimirlem3.5

**Assertion**
Ref	Expression
poimirlem3	..^ $/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem poimirlem3 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimirlem3.4	. . . . . . . . . . . . . . 15 ..^
2		ffn 5743	. . . . . . . . . . . . . . 15 ..^
3	1, 2	syl 17	. . . . . . . . . . . . . 14
4	3	adantr 466	. . . . . . . . . . . . 13 $/\$
5		1ex 9639	. . . . . . . . . . . . . . . . 17
6		fnconstg 5785	. . . . . . . . . . . . . . . . 17
7	5, 6	ax-mp 5	. . . . . . . . . . . . . . . 16
8		c0ex 9638	. . . . . . . . . . . . . . . . 17
9		fnconstg 5785	. . . . . . . . . . . . . . . . 17
10	8, 9	ax-mp 5	. . . . . . . . . . . . . . . 16
11	7, 10	pm3.2i 456	. . . . . . . . . . . . . . 15 $/\$
12		poimirlem3.5	. . . . . . . . . . . . . . . . 17
13		dff1o3 5834	. . . . . . . . . . . . . . . . . 18 $/\$
14	13	simprbi 465	. . . . . . . . . . . . . . . . 17
15		imain 5674	. . . . . . . . . . . . . . . . 17
16	12, 14, 15	3syl 18	. . . . . . . . . . . . . . . 16
17		elfznn0 11888	. . . . . . . . . . . . . . . . . . . . 21
18	17	nn0red 10927	. . . . . . . . . . . . . . . . . . . 20
19	18	ltp1d 10538	. . . . . . . . . . . . . . . . . . 19
20		fzdisj 11827	. . . . . . . . . . . . . . . . . . 19
21	19, 20	syl 17	. . . . . . . . . . . . . . . . . 18
22	21	imaeq2d 5184	. . . . . . . . . . . . . . . . 17
23		ima0 5199	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eq 2479	. . . . . . . . . . . . . . . 16
25	16, 24	sylan9req 2484	. . . . . . . . . . . . . . 15 $/\$
26		fnun 5697	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	11, 25, 26	sylancr 667	. . . . . . . . . . . . . 14 $/\$
28		imaundi 5264	. . . . . . . . . . . . . . . 16
29		nn0p1nn 10910	. . . . . . . . . . . . . . . . . . . . . 22
30		nnuz 11195	. . . . . . . . . . . . . . . . . . . . . 22
31	29, 30	syl6eleq 2520	. . . . . . . . . . . . . . . . . . . . 21
32	17, 31	syl 17	. . . . . . . . . . . . . . . . . . . 20
33		elfzuz3 11798	. . . . . . . . . . . . . . . . . . . 20
34		fzsplit2 11825	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	32, 33, 34	syl2anc 665	. . . . . . . . . . . . . . . . . . 19
36	35	eqcomd 2430	. . . . . . . . . . . . . . . . . 18
37	36	imaeq2d 5184	. . . . . . . . . . . . . . . . 17
38		f1ofo 5835	. . . . . . . . . . . . . . . . . 18
39		foima 5812	. . . . . . . . . . . . . . . . . 18
40	12, 38, 39	3syl 18	. . . . . . . . . . . . . . . . 17
41	37, 40	sylan9eqr 2485	. . . . . . . . . . . . . . . 16 $/\$
42	28, 41	syl5eqr 2477	. . . . . . . . . . . . . . 15 $/\$
43	42	fneq2d 5682	. . . . . . . . . . . . . 14 $/\$
44	27, 43	mpbid 213	. . . . . . . . . . . . 13 $/\$
45		ovex 6330	. . . . . . . . . . . . . 14
46	45	a1i 11	. . . . . . . . . . . . 13 $/\$
47		inidm 3671	. . . . . . . . . . . . 13
48		eqidd 2423	. . . . . . . . . . . . 13 $/\$ $/\$
49		eqidd 2423	. . . . . . . . . . . . 13 $/\$ $/\$
50	4, 44, 46, 46, 47, 48, 49	offval 6549	. . . . . . . . . . . 12 $/\$
51		poimirlem4.2	. . . . . . . . . . . . . . . . . . . 20
52		nn0p1nn 10910	. . . . . . . . . . . . . . . . . . . 20
53	51, 52	syl 17	. . . . . . . . . . . . . . . . . . 19
54	53	nnzd 11040	. . . . . . . . . . . . . . . . . 18
55		uzid 11174	. . . . . . . . . . . . . . . . . 18
56		peano2uz 11213	. . . . . . . . . . . . . . . . . 18
57	54, 55, 56	3syl 18	. . . . . . . . . . . . . . . . 17
58		poimirlem4.3	. . . . . . . . . . . . . . . . . 18
59	51	nn0zd 11039	. . . . . . . . . . . . . . . . . . 19
60		poimir.0	. . . . . . . . . . . . . . . . . . . 20
61	60	nnzd 11040	. . . . . . . . . . . . . . . . . . 19
62		zltp1le 10987	. . . . . . . . . . . . . . . . . . . 20 $/\$
63		peano2z 10979	. . . . . . . . . . . . . . . . . . . . 21
64		eluz 11173	. . . . . . . . . . . . . . . . . . . . 21 $/\$
65	63, 64	sylan 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
66	62, 65	bitr4d 259	. . . . . . . . . . . . . . . . . . 19 $/\$
67	59, 61, 66	syl2anc 665	. . . . . . . . . . . . . . . . . 18
68	58, 67	mpbid 213	. . . . . . . . . . . . . . . . 17
69		fzsplit2 11825	. . . . . . . . . . . . . . . . 17 $/\$
70	57, 68, 69	syl2anc 665	. . . . . . . . . . . . . . . 16
71		fzsn 11841	. . . . . . . . . . . . . . . . . 18
72	54, 71	syl 17	. . . . . . . . . . . . . . . . 17
73	72	uneq1d 3619	. . . . . . . . . . . . . . . 16
74	70, 73	eqtrd 2463	. . . . . . . . . . . . . . 15
75	74	xpeq1d 4873	. . . . . . . . . . . . . 14
76		xpundir 4904	. . . . . . . . . . . . . . 15
77		ovex 6330	. . . . . . . . . . . . . . . . 17
78	77, 8	xpsn 6078	. . . . . . . . . . . . . . . 16
79	78	uneq1i 3616	. . . . . . . . . . . . . . 15
80	76, 79	eqtri 2451	. . . . . . . . . . . . . 14
81	75, 80	syl6eq 2479	. . . . . . . . . . . . 13
82	81	adantr 466	. . . . . . . . . . . 12 $/\$
83	50, 82	uneq12d 3621	. . . . . . . . . . 11 $/\$
84		unass 3623	. . . . . . . . . . 11
85	83, 84	syl6eqr 2481	. . . . . . . . . 10 $/\$
86	51	nn0red 10927	. . . . . . . . . . . . . . . . . . . . 21
87	86	ltp1d 10538	. . . . . . . . . . . . . . . . . . . 20
88	53	nnred 10625	. . . . . . . . . . . . . . . . . . . . 21
89	86, 88	ltnled 9783	. . . . . . . . . . . . . . . . . . . 20
90	87, 89	mpbid 213	. . . . . . . . . . . . . . . . . . 19
91		elfzle2 11804	. . . . . . . . . . . . . . . . . . 19
92	90, 91	nsyl 124	. . . . . . . . . . . . . . . . . 18
93		disjsn 4057	. . . . . . . . . . . . . . . . . 18
94	92, 93	sylibr 215	. . . . . . . . . . . . . . . . 17
95		eqid 2422	. . . . . . . . . . . . . . . . . . 19
96	77, 8	fsn 6073	. . . . . . . . . . . . . . . . . . 19
97	95, 96	mpbir 212	. . . . . . . . . . . . . . . . . 18
98		fun 5760	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ ..^
99	97, 98	mpanl2 685	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
100	1, 94, 99	syl2anc 665	. . . . . . . . . . . . . . . 16 ..^
101		1z 10968	. . . . . . . . . . . . . . . . . . 19
102		nn0uz 11194	. . . . . . . . . . . . . . . . . . . . 21
103		1m1e0 10679	. . . . . . . . . . . . . . . . . . . . . 22
104	103	fveq2i 5881	. . . . . . . . . . . . . . . . . . . . 21
105	102, 104	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . 20
106	51, 105	syl6eleq 2520	. . . . . . . . . . . . . . . . . . 19
107		fzsuc2 11854	. . . . . . . . . . . . . . . . . . 19 $/\$
108	101, 106, 107	sylancr 667	. . . . . . . . . . . . . . . . . 18
109	108	eqcomd 2430	. . . . . . . . . . . . . . . . 17
110		poimirlem4.1	. . . . . . . . . . . . . . . . . . . 20
111		lbfzo0 11956	. . . . . . . . . . . . . . . . . . . 20 ..^
112	110, 111	sylibr 215	. . . . . . . . . . . . . . . . . . 19 ..^
113	112	snssd 4142	. . . . . . . . . . . . . . . . . 18 ..^
114		ssequn2 3639	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
115	113, 114	sylib 199	. . . . . . . . . . . . . . . . 17 ..^ ..^
116	109, 115	feq23d 5738	. . . . . . . . . . . . . . . 16 ..^ ..^
117	100, 116	mpbid 213	. . . . . . . . . . . . . . 15 ..^
118		ffn 5743	. . . . . . . . . . . . . . 15 ..^
119	117, 118	syl 17	. . . . . . . . . . . . . 14
120	119	adantr 466	. . . . . . . . . . . . 13 $/\$
121		fnconstg 5785	. . . . . . . . . . . . . . . . 17
122	5, 121	ax-mp 5	. . . . . . . . . . . . . . . 16
123		fnconstg 5785	. . . . . . . . . . . . . . . . 17
124	8, 123	ax-mp 5	. . . . . . . . . . . . . . . 16
125	122, 124	pm3.2i 456	. . . . . . . . . . . . . . 15 $/\$
126	77, 77	f1osn 5865	. . . . . . . . . . . . . . . . . . 19
127		f1oun 5847	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
128	126, 127	mpanl2 685	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	12, 94, 94, 128	syl12anc 1262	. . . . . . . . . . . . . . . . 17
130		dff1o3 5834	. . . . . . . . . . . . . . . . . 18 $/\$
131	130	simprbi 465	. . . . . . . . . . . . . . . . 17
132		imain 5674	. . . . . . . . . . . . . . . . 17
133	129, 131, 132	3syl 18	. . . . . . . . . . . . . . . 16
134		fzdisj 11827	. . . . . . . . . . . . . . . . . . 19
135	19, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	imaeq2d 5184	. . . . . . . . . . . . . . . . 17
137		ima0 5199	. . . . . . . . . . . . . . . . 17
138	136, 137	syl6eq 2479	. . . . . . . . . . . . . . . 16
139	133, 138	sylan9req 2484	. . . . . . . . . . . . . . 15 $/\$
140		fnun 5697	. . . . . . . . . . . . . . 15 $/\$ $/\$
141	125, 139, 140	sylancr 667	. . . . . . . . . . . . . 14 $/\$
142		f1ofo 5835	. . . . . . . . . . . . . . . . . . 19
143		foima 5812	. . . . . . . . . . . . . . . . . . 19
144	129, 142, 143	3syl 18	. . . . . . . . . . . . . . . . . 18
145	108	imaeq2d 5184	. . . . . . . . . . . . . . . . . 18
146	144, 145, 108	3eqtr4d 2473	. . . . . . . . . . . . . . . . 17
147		peano2uz 11213	. . . . . . . . . . . . . . . . . . . 20
148	33, 147	syl 17	. . . . . . . . . . . . . . . . . . 19
149		fzsplit2 11825	. . . . . . . . . . . . . . . . . . 19 $/\$
150	32, 148, 149	syl2anc 665	. . . . . . . . . . . . . . . . . 18
151	150	imaeq2d 5184	. . . . . . . . . . . . . . . . 17
152	146, 151	sylan9req 2484	. . . . . . . . . . . . . . . 16 $/\$
153		imaundi 5264	. . . . . . . . . . . . . . . 16
154	152, 153	syl6eq 2479	. . . . . . . . . . . . . . 15 $/\$
155	154	fneq2d 5682	. . . . . . . . . . . . . 14 $/\$
156	141, 155	mpbird 235	. . . . . . . . . . . . 13 $/\$
157		ovex 6330	. . . . . . . . . . . . . 14
158	157	a1i 11	. . . . . . . . . . . . 13 $/\$
159		inidm 3671	. . . . . . . . . . . . 13
160		eqidd 2423	. . . . . . . . . . . . 13 $/\$ $/\$
161		eqidd 2423	. . . . . . . . . . . . 13 $/\$ $/\$
162	120, 156, 158, 158, 159, 160, 161	offval 6549	. . . . . . . . . . . 12 $/\$
163	77	a1i 11	. . . . . . . . . . . . 13 $/\$
164	8	a1i 11	. . . . . . . . . . . . 13 $/\$
165	109	adantr 466	. . . . . . . . . . . . 13 $/\$
166		fveq2 5878	. . . . . . . . . . . . . . . . 17
167	77	snid 4024	. . . . . . . . . . . . . . . . . . . 20
168	77, 8	fnsn 5651	. . . . . . . . . . . . . . . . . . . . 21
169		fvun2 5950	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
170	168, 169	mp3an2 1348	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
171	167, 170	mpanr2 688	. . . . . . . . . . . . . . . . . . 19 $/\$
172	3, 94, 171	syl2anc 665	. . . . . . . . . . . . . . . . . 18
173	77, 8	fvsn 6109	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2479	. . . . . . . . . . . . . . . . 17
175	166, 174	sylan9eqr 2485	. . . . . . . . . . . . . . . 16 $/\$
176	175	adantlr 719	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		fveq2 5878	. . . . . . . . . . . . . . . 16
178		imadmrn 5194	. . . . . . . . . . . . . . . . . . . . . . . 24
179	77, 77	xpsn 6078	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	imaeq1i 5181	. . . . . . . . . . . . . . . . . . . . . . . . 25
181		dmxpid 5070	. . . . . . . . . . . . . . . . . . . . . . . . . 26
182	181	imaeq2i 5182	. . . . . . . . . . . . . . . . . . . . . . . . 25
183	180, 182	eqtri 2451	. . . . . . . . . . . . . . . . . . . . . . . 24
184		rnxpid 5286	. . . . . . . . . . . . . . . . . . . . . . . 24
185	178, 183, 184	3eqtr3ri 2460	. . . . . . . . . . . . . . . . . . . . . . 23
186		eluzp1p1 11185	. . . . . . . . . . . . . . . . . . . . . . . . . 26
187		eluzfz2 11808	. . . . . . . . . . . . . . . . . . . . . . . . . 26
188	33, 186, 187	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
189	188	snssd 4142	. . . . . . . . . . . . . . . . . . . . . . . 24
190		imass2 5220	. . . . . . . . . . . . . . . . . . . . . . . 24
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
192	185, 191	syl5eqss 3508	. . . . . . . . . . . . . . . . . . . . . 22
193		ssel 3458	. . . . . . . . . . . . . . . . . . . . . 22
194	192, 167, 193	mpisyl 22	. . . . . . . . . . . . . . . . . . . . 21
195		elun2 3634	. . . . . . . . . . . . . . . . . . . . 21
196	194, 195	syl 17	. . . . . . . . . . . . . . . . . . . 20
197		imaundir 5265	. . . . . . . . . . . . . . . . . . . 20
198	196, 197	syl6eleqr 2521	. . . . . . . . . . . . . . . . . . 19
199	198	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
200		fvun2 5950	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
201	122, 124, 200	mp3an12 1350	. . . . . . . . . . . . . . . . . 18 $/\$
202	139, 199, 201	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$
203	8	fvconst2 6132	. . . . . . . . . . . . . . . . . . 19
204	198, 203	syl 17	. . . . . . . . . . . . . . . . . 18
205	204	adantl 467	. . . . . . . . . . . . . . . . 17 $/\$
206	202, 205	eqtrd 2463	. . . . . . . . . . . . . . . 16 $/\$
207	177, 206	sylan9eqr 2485	. . . . . . . . . . . . . . 15 $/\$ $/\$
208	176, 207	oveq12d 6320	. . . . . . . . . . . . . 14 $/\$ $/\$
209		00id 9809	. . . . . . . . . . . . . 14
210	208, 209	syl6eq 2479	. . . . . . . . . . . . 13 $/\$ $/\$
211	163, 164, 165, 210	fmptapd 6100	. . . . . . . . . . . 12 $/\$
212	3, 94	jca 534	. . . . . . . . . . . . . . . . 17 $/\$
213		fvun1 5949	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	168, 213	mp3an2 1348	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
215	214	anassrs 652	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
216	212, 215	sylan 473	. . . . . . . . . . . . . . . 16 $/\$
217	216	adantlr 719	. . . . . . . . . . . . . . 15 $/\$ $/\$
218		fvres 5892	. . . . . . . . . . . . . . . . 17
219	218	eqcomd 2430	. . . . . . . . . . . . . . . 16
220		resundir 5135	. . . . . . . . . . . . . . . . . 18
221		relxp 4958	. . . . . . . . . . . . . . . . . . . . . . 23
222		dmxpss 5284	. . . . . . . . . . . . . . . . . . . . . . . . 25
223		imassrn 5195	. . . . . . . . . . . . . . . . . . . . . . . . 25
224	222, 223	sstri 3473	. . . . . . . . . . . . . . . . . . . . . . . 24
225		f1of 5828	. . . . . . . . . . . . . . . . . . . . . . . . 25
226		frn 5749	. . . . . . . . . . . . . . . . . . . . . . . . 25
227	12, 225, 226	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24
228	224, 227	syl5ss 3475	. . . . . . . . . . . . . . . . . . . . . . 23
229		relssres 5158	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
230	221, 228, 229	sylancr 667	. . . . . . . . . . . . . . . . . . . . . 22
231	230	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$
232		imassrn 5195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
233	77	rnsnop 5333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
234	232, 233	sseqtri 3496	. . . . . . . . . . . . . . . . . . . . . . . . . 26
235		ssrin 3687	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	234, 235	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
237		incom 3655	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237, 94	syl5eq 2475	. . . . . . . . . . . . . . . . . . . . . . . . 25
239	236, 238	syl5sseq 3512	. . . . . . . . . . . . . . . . . . . . . . . 24
240		ss0 3793	. . . . . . . . . . . . . . . . . . . . . . . 24
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
242		fnconstg 5785	. . . . . . . . . . . . . . . . . . . . . . . 24
243		fnresdisj 5701	. . . . . . . . . . . . . . . . . . . . . . . 24
244	5, 242, 243	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23
245	241, 244	sylib 199	. . . . . . . . . . . . . . . . . . . . . 22
246	245	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$
247	231, 246	uneq12d 3621	. . . . . . . . . . . . . . . . . . . 20 $/\$
248		imaundir 5265	. . . . . . . . . . . . . . . . . . . . . . . 24
249	248	xpeq1i 4870	. . . . . . . . . . . . . . . . . . . . . . 23
250		xpundir 4904	. . . . . . . . . . . . . . . . . . . . . . 23
251	249, 250	eqtri 2451	. . . . . . . . . . . . . . . . . . . . . 22
252	251	reseq1i 5117	. . . . . . . . . . . . . . . . . . . . 21
253		resundir 5135	. . . . . . . . . . . . . . . . . . . . 21
254	252, 253	eqtr2i 2452	. . . . . . . . . . . . . . . . . . . 20
255		un0 3787	. . . . . . . . . . . . . . . . . . . 20
256	247, 254, 255	3eqtr3g 2486	. . . . . . . . . . . . . . . . . . 19 $/\$
257		f1odm 5832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
258	12, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	258	ineq2d 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
260	259	reseq2d 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
261		f1orel 5831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
262		resindm 5165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263	12, 261, 262	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264	260, 263	eqtr3d 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
265	35	ineq2d 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
266		fzssp1 11842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
267		dfss1 3667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
268	266, 267	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
270		incom 3655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
271	270, 135	syl5eq 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
272	269, 271	uneq12d 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273		uncom 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
274		indi 3719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
275	273, 274	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
276		un0 3787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
277	272, 275, 276	3eqtr3g 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
278	265, 277	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
279	278	reseq2d 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . 27