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 31955

Description: Lemma for poimir 31985 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 5733	. . . . . . . . . . . . . . 15 ..^
3	1, 2	syl 17	. . . . . . . . . . . . . 14
4	3	adantr 467	. . . . . . . . . . . . 13 $/\$
5		1ex 9643	. . . . . . . . . . . . . . . . 17
6		fnconstg 5776	. . . . . . . . . . . . . . . . 17
7	5, 6	ax-mp 5	. . . . . . . . . . . . . . . 16
8		c0ex 9642	. . . . . . . . . . . . . . . . 17
9		fnconstg 5776	. . . . . . . . . . . . . . . . 17
10	8, 9	ax-mp 5	. . . . . . . . . . . . . . . 16
11	7, 10	pm3.2i 457	. . . . . . . . . . . . . . 15 $/\$
12		poimirlem3.5	. . . . . . . . . . . . . . . . 17
13		dff1o3 5825	. . . . . . . . . . . . . . . . . 18 $/\$
14	13	simprbi 466	. . . . . . . . . . . . . . . . 17
15		imain 5664	. . . . . . . . . . . . . . . . 17
16	12, 14, 15	3syl 18	. . . . . . . . . . . . . . . 16
17		elfznn0 11894	. . . . . . . . . . . . . . . . . . . . 21
18	17	nn0red 10933	. . . . . . . . . . . . . . . . . . . 20
19	18	ltp1d 10544	. . . . . . . . . . . . . . . . . . 19
20		fzdisj 11833	. . . . . . . . . . . . . . . . . . 19
21	19, 20	syl 17	. . . . . . . . . . . . . . . . . 18
22	21	imaeq2d 5171	. . . . . . . . . . . . . . . . 17
23		ima0 5186	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eq 2503	. . . . . . . . . . . . . . . 16
25	16, 24	sylan9req 2508	. . . . . . . . . . . . . . 15 $/\$
26		fnun 5687	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	11, 25, 26	sylancr 670	. . . . . . . . . . . . . 14 $/\$
28		imaundi 5251	. . . . . . . . . . . . . . . 16
29		nn0p1nn 10916	. . . . . . . . . . . . . . . . . . . . . 22
30		nnuz 11201	. . . . . . . . . . . . . . . . . . . . . 22
31	29, 30	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . 21
32	17, 31	syl 17	. . . . . . . . . . . . . . . . . . . 20
33		elfzuz3 11804	. . . . . . . . . . . . . . . . . . . 20
34		fzsplit2 11831	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	32, 33, 34	syl2anc 667	. . . . . . . . . . . . . . . . . . 19
36	35	eqcomd 2459	. . . . . . . . . . . . . . . . . 18
37	36	imaeq2d 5171	. . . . . . . . . . . . . . . . 17
38		f1ofo 5826	. . . . . . . . . . . . . . . . . 18
39		foima 5803	. . . . . . . . . . . . . . . . . 18
40	12, 38, 39	3syl 18	. . . . . . . . . . . . . . . . 17
41	37, 40	sylan9eqr 2509	. . . . . . . . . . . . . . . 16 $/\$
42	28, 41	syl5eqr 2501	. . . . . . . . . . . . . . 15 $/\$
43	42	fneq2d 5672	. . . . . . . . . . . . . 14 $/\$
44	27, 43	mpbid 214	. . . . . . . . . . . . 13 $/\$
45		ovex 6323	. . . . . . . . . . . . . 14
46	45	a1i 11	. . . . . . . . . . . . 13 $/\$
47		inidm 3643	. . . . . . . . . . . . 13
48		eqidd 2454	. . . . . . . . . . . . 13 $/\$ $/\$
49		eqidd 2454	. . . . . . . . . . . . 13 $/\$ $/\$
50	4, 44, 46, 46, 47, 48, 49	offval 6543	. . . . . . . . . . . 12 $/\$
51		poimirlem4.2	. . . . . . . . . . . . . . . . . . . 20
52		nn0p1nn 10916	. . . . . . . . . . . . . . . . . . . 20
53	51, 52	syl 17	. . . . . . . . . . . . . . . . . . 19
54	53	nnzd 11046	. . . . . . . . . . . . . . . . . 18
55		uzid 11180	. . . . . . . . . . . . . . . . . 18
56		peano2uz 11219	. . . . . . . . . . . . . . . . . 18
57	54, 55, 56	3syl 18	. . . . . . . . . . . . . . . . 17
58		poimirlem4.3	. . . . . . . . . . . . . . . . . 18
59	51	nn0zd 11045	. . . . . . . . . . . . . . . . . . 19
60		poimir.0	. . . . . . . . . . . . . . . . . . . 20
61	60	nnzd 11046	. . . . . . . . . . . . . . . . . . 19
62		zltp1le 10993	. . . . . . . . . . . . . . . . . . . 20 $/\$
63		peano2z 10985	. . . . . . . . . . . . . . . . . . . . 21
64		eluz 11179	. . . . . . . . . . . . . . . . . . . . 21 $/\$
65	63, 64	sylan 474	. . . . . . . . . . . . . . . . . . . 20 $/\$
66	62, 65	bitr4d 260	. . . . . . . . . . . . . . . . . . 19 $/\$
67	59, 61, 66	syl2anc 667	. . . . . . . . . . . . . . . . . 18
68	58, 67	mpbid 214	. . . . . . . . . . . . . . . . 17
69		fzsplit2 11831	. . . . . . . . . . . . . . . . 17 $/\$
70	57, 68, 69	syl2anc 667	. . . . . . . . . . . . . . . 16
71		fzsn 11847	. . . . . . . . . . . . . . . . . 18
72	54, 71	syl 17	. . . . . . . . . . . . . . . . 17
73	72	uneq1d 3589	. . . . . . . . . . . . . . . 16
74	70, 73	eqtrd 2487	. . . . . . . . . . . . . . 15
75	74	xpeq1d 4860	. . . . . . . . . . . . . 14
76		xpundir 4891	. . . . . . . . . . . . . . 15
77		ovex 6323	. . . . . . . . . . . . . . . . 17
78	77, 8	xpsn 6071	. . . . . . . . . . . . . . . 16
79	78	uneq1i 3586	. . . . . . . . . . . . . . 15
80	76, 79	eqtri 2475	. . . . . . . . . . . . . 14
81	75, 80	syl6eq 2503	. . . . . . . . . . . . 13
82	81	adantr 467	. . . . . . . . . . . 12 $/\$
83	50, 82	uneq12d 3591	. . . . . . . . . . 11 $/\$
84		unass 3593	. . . . . . . . . . 11
85	83, 84	syl6eqr 2505	. . . . . . . . . 10 $/\$
86	51	nn0red 10933	. . . . . . . . . . . . . . . . . . . . 21
87	86	ltp1d 10544	. . . . . . . . . . . . . . . . . . . 20
88	53	nnred 10631	. . . . . . . . . . . . . . . . . . . . 21
89	86, 88	ltnled 9787	. . . . . . . . . . . . . . . . . . . 20
90	87, 89	mpbid 214	. . . . . . . . . . . . . . . . . . 19
91		elfzle2 11810	. . . . . . . . . . . . . . . . . . 19
92	90, 91	nsyl 125	. . . . . . . . . . . . . . . . . 18
93		disjsn 4034	. . . . . . . . . . . . . . . . . 18
94	92, 93	sylibr 216	. . . . . . . . . . . . . . . . 17
95		eqid 2453	. . . . . . . . . . . . . . . . . . 19
96	77, 8	fsn 6066	. . . . . . . . . . . . . . . . . . 19
97	95, 96	mpbir 213	. . . . . . . . . . . . . . . . . 18
98		fun 5751	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ ..^
99	97, 98	mpanl2 688	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
100	1, 94, 99	syl2anc 667	. . . . . . . . . . . . . . . 16 ..^
101		1z 10974	. . . . . . . . . . . . . . . . . . 19
102		nn0uz 11200	. . . . . . . . . . . . . . . . . . . . 21
103		1m1e0 10685	. . . . . . . . . . . . . . . . . . . . . 22
104	103	fveq2i 5873	. . . . . . . . . . . . . . . . . . . . 21
105	102, 104	eqtr4i 2478	. . . . . . . . . . . . . . . . . . . 20
106	51, 105	syl6eleq 2541	. . . . . . . . . . . . . . . . . . 19
107		fzsuc2 11860	. . . . . . . . . . . . . . . . . . 19 $/\$
108	101, 106, 107	sylancr 670	. . . . . . . . . . . . . . . . . 18
109	108	eqcomd 2459	. . . . . . . . . . . . . . . . 17
110		poimirlem4.1	. . . . . . . . . . . . . . . . . . . 20
111		lbfzo0 11962	. . . . . . . . . . . . . . . . . . . 20 ..^
112	110, 111	sylibr 216	. . . . . . . . . . . . . . . . . . 19 ..^
113	112	snssd 4120	. . . . . . . . . . . . . . . . . 18 ..^
114		ssequn2 3609	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
115	113, 114	sylib 200	. . . . . . . . . . . . . . . . 17 ..^ ..^
116	109, 115	feq23d 5728	. . . . . . . . . . . . . . . 16 ..^ ..^
117	100, 116	mpbid 214	. . . . . . . . . . . . . . 15 ..^
118		ffn 5733	. . . . . . . . . . . . . . 15 ..^
119	117, 118	syl 17	. . . . . . . . . . . . . 14
120	119	adantr 467	. . . . . . . . . . . . 13 $/\$
121		fnconstg 5776	. . . . . . . . . . . . . . . . 17
122	5, 121	ax-mp 5	. . . . . . . . . . . . . . . 16
123		fnconstg 5776	. . . . . . . . . . . . . . . . 17
124	8, 123	ax-mp 5	. . . . . . . . . . . . . . . 16
125	122, 124	pm3.2i 457	. . . . . . . . . . . . . . 15 $/\$
126	77, 77	f1osn 5857	. . . . . . . . . . . . . . . . . . 19
127		f1oun 5838	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
128	126, 127	mpanl2 688	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	12, 94, 94, 128	syl12anc 1267	. . . . . . . . . . . . . . . . 17
130		dff1o3 5825	. . . . . . . . . . . . . . . . . 18 $/\$
131	130	simprbi 466	. . . . . . . . . . . . . . . . 17
132		imain 5664	. . . . . . . . . . . . . . . . 17
133	129, 131, 132	3syl 18	. . . . . . . . . . . . . . . 16
134		fzdisj 11833	. . . . . . . . . . . . . . . . . . 19
135	19, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	imaeq2d 5171	. . . . . . . . . . . . . . . . 17
137		ima0 5186	. . . . . . . . . . . . . . . . 17
138	136, 137	syl6eq 2503	. . . . . . . . . . . . . . . 16
139	133, 138	sylan9req 2508	. . . . . . . . . . . . . . 15 $/\$
140		fnun 5687	. . . . . . . . . . . . . . 15 $/\$ $/\$
141	125, 139, 140	sylancr 670	. . . . . . . . . . . . . 14 $/\$
142		f1ofo 5826	. . . . . . . . . . . . . . . . . . 19
143		foima 5803	. . . . . . . . . . . . . . . . . . 19
144	129, 142, 143	3syl 18	. . . . . . . . . . . . . . . . . 18
145	108	imaeq2d 5171	. . . . . . . . . . . . . . . . . 18
146	144, 145, 108	3eqtr4d 2497	. . . . . . . . . . . . . . . . 17
147		peano2uz 11219	. . . . . . . . . . . . . . . . . . . 20
148	33, 147	syl 17	. . . . . . . . . . . . . . . . . . 19
149		fzsplit2 11831	. . . . . . . . . . . . . . . . . . 19 $/\$
150	32, 148, 149	syl2anc 667	. . . . . . . . . . . . . . . . . 18
151	150	imaeq2d 5171	. . . . . . . . . . . . . . . . 17
152	146, 151	sylan9req 2508	. . . . . . . . . . . . . . . 16 $/\$
153		imaundi 5251	. . . . . . . . . . . . . . . 16
154	152, 153	syl6eq 2503	. . . . . . . . . . . . . . 15 $/\$
155	154	fneq2d 5672	. . . . . . . . . . . . . 14 $/\$
156	141, 155	mpbird 236	. . . . . . . . . . . . 13 $/\$
157		ovex 6323	. . . . . . . . . . . . . 14
158	157	a1i 11	. . . . . . . . . . . . 13 $/\$
159		inidm 3643	. . . . . . . . . . . . 13
160		eqidd 2454	. . . . . . . . . . . . 13 $/\$ $/\$
161		eqidd 2454	. . . . . . . . . . . . 13 $/\$ $/\$
162	120, 156, 158, 158, 159, 160, 161	offval 6543	. . . . . . . . . . . 12 $/\$
163	77	a1i 11	. . . . . . . . . . . . 13 $/\$
164	8	a1i 11	. . . . . . . . . . . . 13 $/\$
165	109	adantr 467	. . . . . . . . . . . . 13 $/\$
166		fveq2 5870	. . . . . . . . . . . . . . . . 17
167	77	snid 3998	. . . . . . . . . . . . . . . . . . . 20
168	77, 8	fnsn 5638	. . . . . . . . . . . . . . . . . . . . 21
169		fvun2 5942	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
170	168, 169	mp3an2 1354	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
171	167, 170	mpanr2 691	. . . . . . . . . . . . . . . . . . 19 $/\$
172	3, 94, 171	syl2anc 667	. . . . . . . . . . . . . . . . . 18
173	77, 8	fvsn 6102	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2503	. . . . . . . . . . . . . . . . 17
175	166, 174	sylan9eqr 2509	. . . . . . . . . . . . . . . 16 $/\$
176	175	adantlr 722	. . . . . . . . . . . . . . 15 $/\$ $/\$
177		fveq2 5870	. . . . . . . . . . . . . . . 16
178		imadmrn 5181	. . . . . . . . . . . . . . . . . . . . . . . 24
179	77, 77	xpsn 6071	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	imaeq1i 5168	. . . . . . . . . . . . . . . . . . . . . . . . 25
181		dmxpid 5057	. . . . . . . . . . . . . . . . . . . . . . . . . 26
182	181	imaeq2i 5169	. . . . . . . . . . . . . . . . . . . . . . . . 25
183	180, 182	eqtri 2475	. . . . . . . . . . . . . . . . . . . . . . . 24
184		rnxpid 5273	. . . . . . . . . . . . . . . . . . . . . . . 24
185	178, 183, 184	3eqtr3ri 2484	. . . . . . . . . . . . . . . . . . . . . . 23
186		eluzp1p1 11191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
187		eluzfz2 11814	. . . . . . . . . . . . . . . . . . . . . . . . . 26
188	33, 186, 187	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
189	188	snssd 4120	. . . . . . . . . . . . . . . . . . . . . . . 24
190		imass2 5207	. . . . . . . . . . . . . . . . . . . . . . . 24
191	189, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
192	185, 191	syl5eqss 3478	. . . . . . . . . . . . . . . . . . . . . 22
193		ssel 3428	. . . . . . . . . . . . . . . . . . . . . 22
194	192, 167, 193	mpisyl 21	. . . . . . . . . . . . . . . . . . . . 21
195		elun2 3604	. . . . . . . . . . . . . . . . . . . . 21
196	194, 195	syl 17	. . . . . . . . . . . . . . . . . . . 20
197		imaundir 5252	. . . . . . . . . . . . . . . . . . . 20
198	196, 197	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . 19
199	198	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
200		fvun2 5942	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
201	122, 124, 200	mp3an12 1356	. . . . . . . . . . . . . . . . . 18 $/\$
202	139, 199, 201	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$
203	8	fvconst2 6125	. . . . . . . . . . . . . . . . . . 19
204	198, 203	syl 17	. . . . . . . . . . . . . . . . . 18
205	204	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
206	202, 205	eqtrd 2487	. . . . . . . . . . . . . . . 16 $/\$
207	177, 206	sylan9eqr 2509	. . . . . . . . . . . . . . 15 $/\$ $/\$
208	176, 207	oveq12d 6313	. . . . . . . . . . . . . 14 $/\$ $/\$
209		00id 9813	. . . . . . . . . . . . . 14
210	208, 209	syl6eq 2503	. . . . . . . . . . . . 13 $/\$ $/\$
211	163, 164, 165, 210	fmptapd 6093	. . . . . . . . . . . 12 $/\$
212	3, 94	jca 535	. . . . . . . . . . . . . . . . 17 $/\$
213		fvun1 5941	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	168, 213	mp3an2 1354	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
215	214	anassrs 654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
216	212, 215	sylan 474	. . . . . . . . . . . . . . . 16 $/\$
217	216	adantlr 722	. . . . . . . . . . . . . . 15 $/\$ $/\$
218		fvres 5884	. . . . . . . . . . . . . . . . 17
219	218	eqcomd 2459	. . . . . . . . . . . . . . . 16
220		resundir 5122	. . . . . . . . . . . . . . . . . 18
221		relxp 4945	. . . . . . . . . . . . . . . . . . . . . . 23
222		dmxpss 5271	. . . . . . . . . . . . . . . . . . . . . . . . 25
223		imassrn 5182	. . . . . . . . . . . . . . . . . . . . . . . . 25
224	222, 223	sstri 3443	. . . . . . . . . . . . . . . . . . . . . . . 24
225		f1of 5819	. . . . . . . . . . . . . . . . . . . . . . . . 25
226		frn 5740	. . . . . . . . . . . . . . . . . . . . . . . . 25
227	12, 225, 226	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24
228	224, 227	syl5ss 3445	. . . . . . . . . . . . . . . . . . . . . . 23
229		relssres 5145	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
230	221, 228, 229	sylancr 670	. . . . . . . . . . . . . . . . . . . . . 22
231	230	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$
232		imassrn 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
233	77	rnsnop 5320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
234	232, 233	sseqtri 3466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
235		ssrin 3659	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	234, 235	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
237		incom 3627	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237, 94	syl5eq 2499	. . . . . . . . . . . . . . . . . . . . . . . . 25
239	236, 238	syl5sseq 3482	. . . . . . . . . . . . . . . . . . . . . . . 24
240		ss0 3767	. . . . . . . . . . . . . . . . . . . . . . . 24
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
242		fnconstg 5776	. . . . . . . . . . . . . . . . . . . . . . . 24
243		fnresdisj 5691	. . . . . . . . . . . . . . . . . . . . . . . 24
244	5, 242, 243	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23
245	241, 244	sylib 200	. . . . . . . . . . . . . . . . . . . . . 22
246	245	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$
247	231, 246	uneq12d 3591	. . . . . . . . . . . . . . . . . . . 20 $/\$
248		imaundir 5252	. . . . . . . . . . . . . . . . . . . . . . . 24
249	248	xpeq1i 4857	. . . . . . . . . . . . . . . . . . . . . . 23
250		xpundir 4891	. . . . . . . . . . . . . . . . . . . . . . 23
251	249, 250	eqtri 2475	. . . . . . . . . . . . . . . . . . . . . 22
252	251	reseq1i 5104	. . . . . . . . . . . . . . . . . . . . 21
253		resundir 5122	. . . . . . . . . . . . . . . . . . . . 21
254	252, 253	eqtr2i 2476	. . . . . . . . . . . . . . . . . . . 20
255		un0 3761	. . . . . . . . . . . . . . . . . . . 20
256	247, 254, 255	3eqtr3g 2510	. . . . . . . . . . . . . . . . . . 19 $/\$
257		f1odm 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
258	12, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	258	ineq2d 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
260	259	reseq2d 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
261		f1orel 5822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
262		resindm 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263	12, 261, 262	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264	260, 263	eqtr3d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
265	35	ineq2d 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
266		fzssp1 11848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
267		dfss1 3639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
268	266, 267	mpbi 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
270		incom 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
271	270, 135	syl5eq 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
272	269, 271	uneq12d 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273		uncom 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
274		indi 3691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
275	273, 274	eqtr4i 2478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
276		un0 3761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
277	272, 275, 276	3eqtr3g 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
278	265, 277	eqtrd 2487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
279	278	reseq2d 5108