poimirlem3 - Mathbox for Brendan Leahy

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

Theorem poimirlem3 32007

Description: Lemma for poimir 32037 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 5739	. . . . . . . . . . . . . . 15 ..^
3	1, 2	syl 17	. . . . . . . . . . . . . 14
4	3	adantr 472	. . . . . . . . . . . . 13 $/\$
5		1ex 9656	. . . . . . . . . . . . . . . . 17
6		fnconstg 5784	. . . . . . . . . . . . . . . . 17
7	5, 6	ax-mp 5	. . . . . . . . . . . . . . . 16
8		c0ex 9655	. . . . . . . . . . . . . . . . 17
9		fnconstg 5784	. . . . . . . . . . . . . . . . 17
10	8, 9	ax-mp 5	. . . . . . . . . . . . . . . 16
11	7, 10	pm3.2i 462	. . . . . . . . . . . . . . 15 $/\$
12		poimirlem3.5	. . . . . . . . . . . . . . . . 17
13		dff1o3 5834	. . . . . . . . . . . . . . . . . 18 $/\$
14	13	simprbi 471	. . . . . . . . . . . . . . . . 17
15		imain 5669	. . . . . . . . . . . . . . . . 17
16	12, 14, 15	3syl 18	. . . . . . . . . . . . . . . 16
17		elfznn0 11913	. . . . . . . . . . . . . . . . . . . . 21
18	17	nn0red 10950	. . . . . . . . . . . . . . . . . . . 20
19	18	ltp1d 10559	. . . . . . . . . . . . . . . . . . 19
20		fzdisj 11852	. . . . . . . . . . . . . . . . . . 19
21	19, 20	syl 17	. . . . . . . . . . . . . . . . . 18
22	21	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
23		ima0 5189	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eq 2521	. . . . . . . . . . . . . . . 16
25	16, 24	sylan9req 2526	. . . . . . . . . . . . . . 15 $/\$
26		fnun 5692	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	11, 25, 26	sylancr 676	. . . . . . . . . . . . . 14 $/\$
28		imaundi 5254	. . . . . . . . . . . . . . . 16
29		nn0p1nn 10933	. . . . . . . . . . . . . . . . . . . . . 22
30		nnuz 11218	. . . . . . . . . . . . . . . . . . . . . 22
31	29, 30	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . 21
32	17, 31	syl 17	. . . . . . . . . . . . . . . . . . . 20
33		elfzuz3 11823	. . . . . . . . . . . . . . . . . . . 20
34		fzsplit2 11850	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	32, 33, 34	syl2anc 673	. . . . . . . . . . . . . . . . . . 19
36	35	eqcomd 2477	. . . . . . . . . . . . . . . . . 18
37	36	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
38		f1ofo 5835	. . . . . . . . . . . . . . . . . 18
39		foima 5811	. . . . . . . . . . . . . . . . . 18
40	12, 38, 39	3syl 18	. . . . . . . . . . . . . . . . 17
41	37, 40	sylan9eqr 2527	. . . . . . . . . . . . . . . 16 $/\$
42	28, 41	syl5eqr 2519	. . . . . . . . . . . . . . 15 $/\$
43	42	fneq2d 5677	. . . . . . . . . . . . . 14 $/\$
44	27, 43	mpbid 215	. . . . . . . . . . . . 13 $/\$
45		ovex 6336	. . . . . . . . . . . . . 14
46	45	a1i 11	. . . . . . . . . . . . 13 $/\$
47		inidm 3632	. . . . . . . . . . . . 13
48		eqidd 2472	. . . . . . . . . . . . 13 $/\$ $/\$
49		eqidd 2472	. . . . . . . . . . . . 13 $/\$ $/\$
50	4, 44, 46, 46, 47, 48, 49	offval 6557	. . . . . . . . . . . 12 $/\$
51		poimirlem4.2	. . . . . . . . . . . . . . . . . . . 20
52		nn0p1nn 10933	. . . . . . . . . . . . . . . . . . . 20
53	51, 52	syl 17	. . . . . . . . . . . . . . . . . . 19
54	53	nnzd 11062	. . . . . . . . . . . . . . . . . 18
55		uzid 11197	. . . . . . . . . . . . . . . . . 18
56		peano2uz 11235	. . . . . . . . . . . . . . . . . 18
57	54, 55, 56	3syl 18	. . . . . . . . . . . . . . . . 17
58		poimirlem4.3	. . . . . . . . . . . . . . . . . 18
59	51	nn0zd 11061	. . . . . . . . . . . . . . . . . . 19
60		poimir.0	. . . . . . . . . . . . . . . . . . . 20
61	60	nnzd 11062	. . . . . . . . . . . . . . . . . . 19
62		zltp1le 11010	. . . . . . . . . . . . . . . . . . . 20 $/\$
63		peano2z 11002	. . . . . . . . . . . . . . . . . . . . 21
64		eluz 11196	. . . . . . . . . . . . . . . . . . . . 21 $/\$
65	63, 64	sylan 479	. . . . . . . . . . . . . . . . . . . 20 $/\$
66	62, 65	bitr4d 264	. . . . . . . . . . . . . . . . . . 19 $/\$
67	59, 61, 66	syl2anc 673	. . . . . . . . . . . . . . . . . 18
68	58, 67	mpbid 215	. . . . . . . . . . . . . . . . 17
69		fzsplit2 11850	. . . . . . . . . . . . . . . . 17 $/\$
70	57, 68, 69	syl2anc 673	. . . . . . . . . . . . . . . 16
71		fzsn 11866	. . . . . . . . . . . . . . . . . 18
72	54, 71	syl 17	. . . . . . . . . . . . . . . . 17
73	72	uneq1d 3578	. . . . . . . . . . . . . . . 16
74	70, 73	eqtrd 2505	. . . . . . . . . . . . . . 15
75	74	xpeq1d 4862	. . . . . . . . . . . . . 14
76		xpundir 4893	. . . . . . . . . . . . . . 15
77		ovex 6336	. . . . . . . . . . . . . . . . 17
78	77, 8	xpsn 6082	. . . . . . . . . . . . . . . 16
79	78	uneq1i 3575	. . . . . . . . . . . . . . 15
80	76, 79	eqtri 2493	. . . . . . . . . . . . . 14
81	75, 80	syl6eq 2521	. . . . . . . . . . . . 13
82	81	adantr 472	. . . . . . . . . . . 12 $/\$
83	50, 82	uneq12d 3580	. . . . . . . . . . 11 $/\$
84		unass 3582	. . . . . . . . . . 11
85	83, 84	syl6eqr 2523	. . . . . . . . . 10 $/\$
86	51	nn0red 10950	. . . . . . . . . . . . . . . . . . . . 21
87	86	ltp1d 10559	. . . . . . . . . . . . . . . . . . . 20
88	53	nnred 10646	. . . . . . . . . . . . . . . . . . . . 21
89	86, 88	ltnled 9799	. . . . . . . . . . . . . . . . . . . 20
90	87, 89	mpbid 215	. . . . . . . . . . . . . . . . . . 19
91		elfzle2 11829	. . . . . . . . . . . . . . . . . . 19
92	90, 91	nsyl 125	. . . . . . . . . . . . . . . . . 18
93		disjsn 4023	. . . . . . . . . . . . . . . . . 18
94	92, 93	sylibr 217	. . . . . . . . . . . . . . . . 17
95		eqid 2471	. . . . . . . . . . . . . . . . . . 19
96	77, 8	fsn 6077	. . . . . . . . . . . . . . . . . . 19
97	95, 96	mpbir 214	. . . . . . . . . . . . . . . . . 18
98		fun 5758	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ ..^
99	97, 98	mpanl2 695	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
100	1, 94, 99	syl2anc 673	. . . . . . . . . . . . . . . 16 ..^
101		1z 10991	. . . . . . . . . . . . . . . . . . 19
102		nn0uz 11217	. . . . . . . . . . . . . . . . . . . . 21
103		1m1e0 10700	. . . . . . . . . . . . . . . . . . . . . 22
104	103	fveq2i 5882	. . . . . . . . . . . . . . . . . . . . 21
105	102, 104	eqtr4i 2496	. . . . . . . . . . . . . . . . . . . 20
106	51, 105	syl6eleq 2559	. . . . . . . . . . . . . . . . . . 19
107		fzsuc2 11879	. . . . . . . . . . . . . . . . . . 19 $/\$
108	101, 106, 107	sylancr 676	. . . . . . . . . . . . . . . . . 18
109	108	eqcomd 2477	. . . . . . . . . . . . . . . . 17
110		poimirlem4.1	. . . . . . . . . . . . . . . . . . . 20
111		lbfzo0 11983	. . . . . . . . . . . . . . . . . . . 20 ..^
112	110, 111	sylibr 217	. . . . . . . . . . . . . . . . . . 19 ..^
113	112	snssd 4108	. . . . . . . . . . . . . . . . . 18 ..^
114		ssequn2 3598	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
115	113, 114	sylib 201	. . . . . . . . . . . . . . . . 17 ..^ ..^
116	109, 115	feq23d 5734	. . . . . . . . . . . . . . . 16 ..^ ..^
117	100, 116	mpbid 215	. . . . . . . . . . . . . . 15 ..^
118		ffn 5739	. . . . . . . . . . . . . . 15 ..^
119	117, 118	syl 17	. . . . . . . . . . . . . 14
120	119	adantr 472	. . . . . . . . . . . . 13 $/\$
121		fnconstg 5784	. . . . . . . . . . . . . . . . 17
122	5, 121	ax-mp 5	. . . . . . . . . . . . . . . 16
123		fnconstg 5784	. . . . . . . . . . . . . . . . 17
124	8, 123	ax-mp 5	. . . . . . . . . . . . . . . 16
125	122, 124	pm3.2i 462	. . . . . . . . . . . . . . 15 $/\$
126	77, 77	f1osn 5866	. . . . . . . . . . . . . . . . . . 19
127		f1oun 5847	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
128	126, 127	mpanl2 695	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	12, 94, 94, 128	syl12anc 1290	. . . . . . . . . . . . . . . . 17
130		dff1o3 5834	. . . . . . . . . . . . . . . . . 18 $/\$
131	130	simprbi 471	. . . . . . . . . . . . . . . . 17
132		imain 5669	. . . . . . . . . . . . . . . . 17
133	129, 131, 132	3syl 18	. . . . . . . . . . . . . . . 16
134		fzdisj 11852	. . . . . . . . . . . . . . . . . . 19
135	19, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
137		ima0 5189	. . . . . . . . . . . . . . . . 17
138	136, 137	syl6eq 2521	. . . . . . . . . . . . . . . 16
139	133, 138	sylan9req 2526	. . . . . . . . . . . . . . 15 $/\$
140		fnun 5692	. . . . . . . . . . . . . . 15 $/\$ $/\$
141	125, 139, 140	sylancr 676	. . . . . . . . . . . . . 14 $/\$
142		f1ofo 5835	. . . . . . . . . . . . . . . . . . 19
143		foima 5811	. . . . . . . . . . . . . . . . . . 19
144	129, 142, 143	3syl 18	. . . . . . . . . . . . . . . . . 18
145	108	imaeq2d 5174	. . . . . . . . . . . . . . . . . 18
146	144, 145, 108	3eqtr4d 2515	. . . . . . . . . . . . . . . . 17
147		peano2uz 11235	. . . . . . . . . . . . . . . . . . . 20
148	33, 147	syl 17	. . . . . . . . . . . . . . . . . . 19
149		fzsplit2 11850	. . . . . . . . . . . . . . . . . . 19 $/\$
150	32, 148, 149	syl2anc 673	. . . . . . . . . . . . . . . . . 18
151	150	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
152	146, 151	sylan9req 2526	. . . . . . . . . . . . . . . 16 $/\$
153		imaundi 5254	. . . . . . . . . . . . . . . 16
154	152, 153	syl6eq 2521	. . . . . . . . . . . . . . 15 $/\$
155	154	fneq2d 5677	. . . . . . . . . . . . . 14 $/\$
156	141, 155	mpbird 240	. . . . . . . . . . . . 13 $/\$
157		ovex 6336	. . . . . . . . . . . . . 14
158	157	a1i 11	. . . . . . . . . . . . 13 $/\$
159		inidm 3632	. . . . . . . . . . . . 13
160		eqidd 2472	. . . . . . . . . . . . 13 $/\$ $/\$
161		eqidd 2472	. . . . . . . . . . . . 13 $/\$ $/\$
162	120, 156, 158, 158, 159, 160, 161	offval 6557	. . . . . . . . . . . 12 $/\$
163	77	a1i 11	. . . . . . . . . . . . 13 $/\$
164	8	a1i 11	. . . . . . . . . . . . 13 $/\$
165	109	adantr 472	. . . . . . . . . . . . 13 $/\$
166		fveq2 5879	. . . . . . . . . . . . . . . . 17
167	77	snid 3988	. . . . . . . . . . . . . . . . . . . 20
168	77, 8	fnsn 5642	. . . . . . . . . . . . . . . . . . . . 21
169		fvun2 5952	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
170	168, 169	mp3an2 1378	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
171	167, 170	mpanr2 698	. . . . . . . . . . . . . . . . . . 19 $/\$
172	3, 94, 171	syl2anc 673	. . . . . . . . . . . . . . . . . 18
173	77, 8	fvsn 6113	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2521	. . . . . . . . . . . . . . . . 17
175	166, 174	sylan9eqr 2527	. . . . . . . . . . . . . . . 16 $/\$
176	175	adantlr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		fveq2 5879	. . . . . . . . . . . . . . . 16
178		imadmrn 5184	. . . . . . . . . . . . . . . . . . . . . . . 24
179	77, 77	xpsn 6082	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	imaeq1i 5171	. . . . . . . . . . . . . . . . . . . . . . . . 25
181		dmxpid 5060	. . . . . . . . . . . . . . . . . . . . . . . . . 26
182	181	imaeq2i 5172	. . . . . . . . . . . . . . . . . . . . . . . . 25
183	180, 182	eqtri 2493	. . . . . . . . . . . . . . . . . . . . . . . 24
184		rnxpid 5276	. . . . . . . . . . . . . . . . . . . . . . . 24
185	178, 183, 184	3eqtr3ri 2502	. . . . . . . . . . . . . . . . . . . . . . 23
186		eluzp1p1 11208	. . . . . . . . . . . . . . . . . . . . . . . . . 26
187		eluzfz2 11833	. . . . . . . . . . . . . . . . . . . . . . . . . 26
188	33, 186, 187	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
189	188	snssd 4108	. . . . . . . . . . . . . . . . . . . . . . . 24
190		imass2 5210	. . . . . . . . . . . . . . . . . . . . . . . 24
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
192	185, 191	syl5eqss 3462	. . . . . . . . . . . . . . . . . . . . . 22
193		ssel 3412	. . . . . . . . . . . . . . . . . . . . . 22
194	192, 167, 193	mpisyl 21	. . . . . . . . . . . . . . . . . . . . 21
195		elun2 3593	. . . . . . . . . . . . . . . . . . . . 21
196	194, 195	syl 17	. . . . . . . . . . . . . . . . . . . 20
197		imaundir 5255	. . . . . . . . . . . . . . . . . . . 20
198	196, 197	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . 19
199	198	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$
200		fvun2 5952	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
201	122, 124, 200	mp3an12 1380	. . . . . . . . . . . . . . . . . 18 $/\$
202	139, 199, 201	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$
203	8	fvconst2 6136	. . . . . . . . . . . . . . . . . . 19
204	198, 203	syl 17	. . . . . . . . . . . . . . . . . 18
205	204	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
206	202, 205	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$
207	177, 206	sylan9eqr 2527	. . . . . . . . . . . . . . 15 $/\$ $/\$
208	176, 207	oveq12d 6326	. . . . . . . . . . . . . 14 $/\$ $/\$
209		00id 9826	. . . . . . . . . . . . . 14
210	208, 209	syl6eq 2521	. . . . . . . . . . . . 13 $/\$ $/\$
211	163, 164, 165, 210	fmptapd 6104	. . . . . . . . . . . 12 $/\$
212	3, 94	jca 541	. . . . . . . . . . . . . . . . 17 $/\$
213		fvun1 5951	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	168, 213	mp3an2 1378	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
215	214	anassrs 660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
216	212, 215	sylan 479	. . . . . . . . . . . . . . . 16 $/\$
217	216	adantlr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$
218		fvres 5893	. . . . . . . . . . . . . . . . 17
219	218	eqcomd 2477	. . . . . . . . . . . . . . . 16
220		resundir 5125	. . . . . . . . . . . . . . . . . 18
221		relxp 4947	. . . . . . . . . . . . . . . . . . . . . . 23
222		dmxpss 5274	. . . . . . . . . . . . . . . . . . . . . . . . 25
223		imassrn 5185	. . . . . . . . . . . . . . . . . . . . . . . . 25
224	222, 223	sstri 3427	. . . . . . . . . . . . . . . . . . . . . . . 24
225		f1of 5828	. . . . . . . . . . . . . . . . . . . . . . . . 25
226		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . . 25
227	12, 225, 226	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24
228	224, 227	syl5ss 3429	. . . . . . . . . . . . . . . . . . . . . . 23
229		relssres 5148	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
230	221, 228, 229	sylancr 676	. . . . . . . . . . . . . . . . . . . . . 22
231	230	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
232		imassrn 5185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
233	77	rnsnop 5324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
234	232, 233	sseqtri 3450	. . . . . . . . . . . . . . . . . . . . . . . . . 26
235		ssrin 3648	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	234, 235	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
237		incom 3616	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237, 94	syl5eq 2517	. . . . . . . . . . . . . . . . . . . . . . . . 25
239	236, 238	syl5sseq 3466	. . . . . . . . . . . . . . . . . . . . . . . 24
240		ss0 3768	. . . . . . . . . . . . . . . . . . . . . . . 24
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
242		fnconstg 5784	. . . . . . . . . . . . . . . . . . . . . . . 24
243		fnresdisj 5696	. . . . . . . . . . . . . . . . . . . . . . . 24
244	5, 242, 243	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23
245	241, 244	sylib 201	. . . . . . . . . . . . . . . . . . . . . 22
246	245	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
247	231, 246	uneq12d 3580	. . . . . . . . . . . . . . . . . . . 20 $/\$
248		imaundir 5255	. . . . . . . . . . . . . . . . . . . . . . . 24
249	248	xpeq1i 4859	. . . . . . . . . . . . . . . . . . . . . . 23
250		xpundir 4893	. . . . . . . . . . . . . . . . . . . . . . 23
251	249, 250	eqtri 2493	. . . . . . . . . . . . . . . . . . . . . 22
252	251	reseq1i 5107	. . . . . . . . . . . . . . . . . . . . 21
253		resundir 5125	. . . . . . . . . . . . . . . . . . . . 21
254	252, 253	eqtr2i 2494	. . . . . . . . . . . . . . . . . . . 20
255		un0 3762	. . . . . . . . . . . . . . . . . . . 20
256	247, 254, 255	3eqtr3g 2528	. . . . . . . . . . . . . . . . . . 19 $/\$
257		f1odm 5832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
258	12, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	258	ineq2d 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
260	259	reseq2d 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
261		f1orel 5831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
262		resindm 5155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263	12, 261, 262	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264	260, 263	eqtr3d 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
265	35	ineq2d 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
266		fzssp1 11867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
267		dfss1 3628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
268	266, 267	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
270		incom 3616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
271	270, 135	syl5eq 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
272	269, 271	uneq12d 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273		uncom 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
274		indi 3680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
275	273, 274	eqtr4i 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
276		un0 3762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
277	272, 275, 276	3eqtr3g 2528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
278	265, 277	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
279	278	reseq2d 51