poimirlem31 - Mathbox for Brendan Leahy

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

Theorem poimirlem31 31891

Description: Lemma for poimir 31893, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 31890 and poimirlem28 31888. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimir.i
poimir.r
poimir.1	↾_t
poimir.2	$/\$ $/\$ $/\$
poimirlem31.p
poimirlem31.3
poimirlem31.4	$/\$ ..^
poimirlem31.5	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
poimirlem31	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem poimirlem31 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpri 4014	. . . 4 $\/$
2		simprr 765	. . . . . . 7 $/\$ $/\$
3		1eluzge0 11204	. . . . . . . . . . 11
4		fzss1 11839	. . . . . . . . . . 11
5	3, 4	ax-mp 5	. . . . . . . . . 10
6	5	sseli 3461	. . . . . . . . 9
7	6	anim2i 572	. . . . . . . 8 $/\$ $/\$
8		eleq1 2495	. . . . . . . . . . . . 13
9	8	anbi2d 709	. . . . . . . . . . . 12 $/\$ $/\$
10	9	anbi2d 709	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
11		eqeq1 2427	. . . . . . . . . . . 12 $/\$ $/\$
12	11	rexbidv 2940	. . . . . . . . . . 11 $/\$ $/\$
13	10, 12	imbi12d 322	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		poimirlem31.5	. . . . . . . . . 10 $/\$ $/\$ $/\$
15	13, 14	chvarv 2069	. . . . . . . . 9 $/\$ $/\$ $/\$
16		elfzle1 11804	. . . . . . . . . . . . 13
17		1re 9644	. . . . . . . . . . . . . 14
18		elfzelz 11802	. . . . . . . . . . . . . . 15
19	18	zred 11042	. . . . . . . . . . . . . 14
20		lenlt 9714	. . . . . . . . . . . . . 14 $/\$
21	17, 19, 20	sylancr 668	. . . . . . . . . . . . 13
22	16, 21	mpbid 214	. . . . . . . . . . . 12
23		elsni 4022	. . . . . . . . . . . . 13
24		0lt1 10138	. . . . . . . . . . . . 13
25	23, 24	syl6eqbr 4459	. . . . . . . . . . . 12
26	22, 25	nsyl 125	. . . . . . . . . . 11
27		ltso 9716	. . . . . . . . . . . . . . 15
28		snfi 7655	. . . . . . . . . . . . . . . . 17
29		fzfi 12186	. . . . . . . . . . . . . . . . . 18
30		rabfi 7800	. . . . . . . . . . . . . . . . . 18 $/\$
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$
32		unfi 7842	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33	28, 31, 32	mp2an 677	. . . . . . . . . . . . . . . 16 $/\$
34		c0ex 9639	. . . . . . . . . . . . . . . . . 18
35	34	snid 4025	. . . . . . . . . . . . . . . . 17
36		elun1 3634	. . . . . . . . . . . . . . . . 17 $/\$
37		ne0i 3768	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	35, 36, 37	mp2b 10	. . . . . . . . . . . . . . . 16 $/\$
39		0re 9645	. . . . . . . . . . . . . . . . . 18
40		snssi 4142	. . . . . . . . . . . . . . . . . 18
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17
42		ssrab2 3547	. . . . . . . . . . . . . . . . . 18 $/\$
43	18	ssriv 3469	. . . . . . . . . . . . . . . . . . 19
44		zssre 10946	. . . . . . . . . . . . . . . . . . 19
45	43, 44	sstri 3474	. . . . . . . . . . . . . . . . . 18
46	42, 45	sstri 3474	. . . . . . . . . . . . . . . . 17 $/\$
47	41, 46	unssi 3642	. . . . . . . . . . . . . . . 16 $/\$
48	33, 38, 47	3pm3.2i 1184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
49		fisupcl 7989	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	27, 48, 49	mp2an 677	. . . . . . . . . . . . . 14 $/\$ $/\$
51		eleq1 2495	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
52	50, 51	mpbiri 237	. . . . . . . . . . . . 13 $/\$ $/\$
53		elun 3607	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$
54	52, 53	sylib 200	. . . . . . . . . . . 12 $/\$ $\/$ $/\$
55		oveq2 6311	. . . . . . . . . . . . . . . 16
56	55	raleqdv 3032	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	elrab 3230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
58		elfzuz 11798	. . . . . . . . . . . . . . . 16
59		eluzfz2 11809	. . . . . . . . . . . . . . . 16
60	58, 59	syl 17	. . . . . . . . . . . . . . 15
61		simpl 459	. . . . . . . . . . . . . . . 16 $/\$
62	61	ralimi 2819	. . . . . . . . . . . . . . 15 $/\$
63		fveq2 5879	. . . . . . . . . . . . . . . . 17
64	63	breq2d 4433	. . . . . . . . . . . . . . . 16
65	64	rspcva 3181	. . . . . . . . . . . . . . 15 $/\$
66	60, 62, 65	syl2an 480	. . . . . . . . . . . . . 14 $/\$ $/\$
67	57, 66	sylbi 199	. . . . . . . . . . . . 13 $/\$
68	67	orim2i 521	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
69	54, 68	syl 17	. . . . . . . . . . 11 $/\$ $\/$
70		orel1 384	. . . . . . . . . . 11 $\/$
71	26, 69, 70	syl2im 40	. . . . . . . . . 10 $/\$
72	71	reximdv 2900	. . . . . . . . 9 $/\$
73	15, 72	syl5 34	. . . . . . . 8 $/\$ $/\$
74	7, 73	sylan2i 660	. . . . . . 7 $/\$ $/\$
75	2, 74	mpcom 38	. . . . . 6 $/\$ $/\$
76		breq 4423	. . . . . . 7
77	76	rexbidv 2940	. . . . . 6
78	75, 77	syl5ibrcom 226	. . . . 5 $/\$ $/\$
79		poimir.0	. . . . . . . . . . . . . . . 16
80	79	nnzd 11041	. . . . . . . . . . . . . . 15
81		elfzm1b 11874	. . . . . . . . . . . . . . 15 $/\$
82	18, 80, 81	syl2anr 481	. . . . . . . . . . . . . 14 $/\$
83	82	biimpd 211	. . . . . . . . . . . . 13 $/\$
84	83	ex 436	. . . . . . . . . . . 12
85	84	pm2.43d 51	. . . . . . . . . . 11
86	79	nncnd 10627	. . . . . . . . . . . . . . 15
87		npcan1 10046	. . . . . . . . . . . . . . 15
88	86, 87	syl 17	. . . . . . . . . . . . . 14
89		nnm1nn0 10913	. . . . . . . . . . . . . . . . 17
90	79, 89	syl 17	. . . . . . . . . . . . . . . 16
91	90	nn0zd 11040	. . . . . . . . . . . . . . 15
92		uzid 11175	. . . . . . . . . . . . . . 15
93		peano2uz 11214	. . . . . . . . . . . . . . 15
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . 14
95	88, 94	eqeltrrd 2512	. . . . . . . . . . . . 13
96		fzss2 11840	. . . . . . . . . . . . 13
97	95, 96	syl 17	. . . . . . . . . . . 12
98	97	sseld 3464	. . . . . . . . . . 11
99	85, 98	syld 46	. . . . . . . . . 10
100	99	anim2d 568	. . . . . . . . 9 $/\$ $/\$
101	100	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$
102		ovex 6331	. . . . . . . . 9
103		eleq1 2495	. . . . . . . . . . . 12
104	103	anbi2d 709	. . . . . . . . . . 11 $/\$ $/\$
105	104	anbi2d 709	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
106		eqeq1 2427	. . . . . . . . . . 11 $/\$ $/\$
107	106	rexbidv 2940	. . . . . . . . . 10 $/\$ $/\$
108	105, 107	imbi12d 322	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	102, 108, 14	vtocl 3134	. . . . . . . 8 $/\$ $/\$ $/\$
110	101, 109	syldan 473	. . . . . . 7 $/\$ $/\$ $/\$
111		eleq1 2495	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
112	50, 111	mpbiri 237	. . . . . . . . . . . . . . 15 $/\$ $/\$
113		elun 3607	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
114	102	elsnc 4021	. . . . . . . . . . . . . . . . 17
115		oveq2 6311	. . . . . . . . . . . . . . . . . . 19
116	115	raleqdv 3032	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
117	116	elrab 3230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	114, 117	orbi12i 524	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $\/$ $/\$ $/\$
119	113, 118	bitri 253	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $/\$
120	112, 119	sylib 200	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$
121	120	a1i 11	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
122		ltm1 10447	. . . . . . . . . . . . . . . . . 18
123		peano2rem 9943	. . . . . . . . . . . . . . . . . . 19
124		ltnle 9715	. . . . . . . . . . . . . . . . . . 19 $/\$
125	123, 124	mpancom 674	. . . . . . . . . . . . . . . . . 18
126	122, 125	mpbid 214	. . . . . . . . . . . . . . . . 17
127	19, 126	syl 17	. . . . . . . . . . . . . . . 16
128		breq2 4425	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	128	notbid 296	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	127, 129	syl5ibcom 224	. . . . . . . . . . . . . . 15 $/\$ $/\$
131		elun2 3635	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132		fimaxre2 10554	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
133	47, 33, 132	mp2an 677	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	47, 38, 133	3pm3.2i 1184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
135	134	suprubii 10584	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
136	131, 135	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
137	136	con3i 141	. . . . . . . . . . . . . . . 16 $/\$ $/\$
138		ianor 491	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
139	138, 57	xchnxbir 311	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
140	137, 139	sylib 200	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$
141	130, 140	syl6 35	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
142		pm2.63 796	. . . . . . . . . . . . . . 15 $\/$ $/\$ $\/$ $/\$ $/\$
143	142	orcs 396	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
144	141, 143	syld 46	. . . . . . . . . . . . 13 $/\$ $/\$
145	121, 144	jcad 536	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
146		andir 877	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
147		1p0e1 10724	. . . . . . . . . . . . . . . . . 18
148	18	zcnd 11043	. . . . . . . . . . . . . . . . . . . 20
149		ax-1cn 9599	. . . . . . . . . . . . . . . . . . . . 21
150		0cn 9637	. . . . . . . . . . . . . . . . . . . . 21
151		subadd 9880	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
152	149, 150, 151	mp3an23 1353	. . . . . . . . . . . . . . . . . . . 20
153	148, 152	syl 17	. . . . . . . . . . . . . . . . . . 19
154	153	biimpa 487	. . . . . . . . . . . . . . . . . 18 $/\$
155	147, 154	syl5reqr 2479	. . . . . . . . . . . . . . . . 17 $/\$
156		1z 10969	. . . . . . . . . . . . . . . . . . . . . 22
157		fzsn 11842	. . . . . . . . . . . . . . . . . . . . . 22
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
159		oveq2 6311	. . . . . . . . . . . . . . . . . . . . 21
160		sneq 4007	. . . . . . . . . . . . . . . . . . . . 21
161	158, 159, 160	3eqtr4a 2490	. . . . . . . . . . . . . . . . . . . 20
162	161	raleqdv 3032	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	162	notbid 296	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	163	biimpd 211	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
165	155, 164	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
166	165	expimpd 607	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167		ralun 3649	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
168		npcan1 10046	. . . . . . . . . . . . . . . . . . . . . . . . 25
169	148, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
170	169, 58	eqeltrd 2511	. . . . . . . . . . . . . . . . . . . . . . 23
171		peano2zm 10982	. . . . . . . . . . . . . . . . . . . . . . . . 25
172		uzid 11175	. . . . . . . . . . . . . . . . . . . . . . . . 25
173		peano2uz 11214	. . . . . . . . . . . . . . . . . . . . . . . . 25
174	18, 171, 172, 173	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
175	169, 174	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . . . . . 23
176		fzsplit2 11826	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
177	170, 175, 176	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . 22
178	169	oveq1d 6318	. . . . . . . . . . . . . . . . . . . . . . . 24
179		fzsn 11842	. . . . . . . . . . . . . . . . . . . . . . . . 25
180	18, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
181	178, 180	eqtrd 2464	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	uneq2d 3621	. . . . . . . . . . . . . . . . . . . . . 22
183	177, 182	eqtrd 2464	. . . . . . . . . . . . . . . . . . . . 21
184	183	raleqdv 3032	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
185	167, 184	syl5ibr 225	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
186	185	expdimp 439	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
187	186	con3d 139	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
188	187	adantrl 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	expimpd 607	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
190	166, 189	jaod 382	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
191	146, 190	syl5bi 221	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
192		fveq2 5879	. . . . . . . . . . . . . . . . . 18
193	192	neeq1d 2702	. . . . . . . . . . . . . . . . 17
194	64, 193	anbi12d 716	. . . . . . . . . . . . . . . 16 $/\$ $/\$
195	194	ralsng 4032	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	195	notbid 296	. . . . . . . . . . . . . 14 $/\$ $/\$
197		ianor 491	. . . . . . . . . . . . . . 15 $/\$ $\/$
198		nne 2625	. . . . . . . . . . . . . . . 16
199	198	orbi2i 522	. . . . . . . . . . . . . . 15 $\/$ $\/$
200	197, 199	bitri 253	. . . . . . . . . . . . . 14 $/\$ $\/$
201	196, 200	syl6bb 265	. . . . . . . . . . . . 13 $/\$ $\/$
202	191, 201	sylibd 218	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
203	145, 202	syld 46	. . . . . . . . . . 11 $/\$ $\/$
204	203	ad2antlr 732	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\/$
205		poimir.1	. . . . . . . . . . . . . . . . . . 19 ↾_t
206		poimir.r	. . . . . . . . . . . . . . . . . . . . . 22
207		retop 21774	. . . . . . . . . . . . . . . . . . . . . . . 24
208	207	fconst6 5788	. . . . . . . . . . . . . . . . . . . . . . 23
209		pttop 20589	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	29, 208, 209	mp2an 677	. . . . . . . . . . . . . . . . . . . . . 22
211	206, 210	eqeltri 2507	. . . . . . . . . . . . . . . . . . . . 21
212		poimir.i	. . . . . . . . . . . . . . . . . . . . . 22
213		reex 9632	. . . . . . . . . . . . . . . . . . . . . . 23
214		unitssre 11781	. . . . . . . . . . . . . . . . . . . . . . 23
215		mapss 7520	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
216	213, 214, 215	mp2an 677	. . . . . . . . . . . . . . . . . . . . . 22
217	212, 216	eqsstri 3495	. . . . . . . . . . . . . . . . . . . . 21
218		uniretop 21775	. . . . . . . . . . . . . . . . . . . . . . . 24
219	206, 218	ptuniconst 20605	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
220	29, 207, 219	mp2an 677	. . . . . . . . . . . . . . . . . . . . . 22
221	220	restuni 20170	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ↾_t
222	211, 217, 221	mp2an 677	. . . . . . . . . . . . . . . . . . . 20 ↾_t
223	222, 220	cnf 20254	. . . . . . . . . . . . . . . . . . 19 ↾_t
224	205, 223	syl 17	. . . . . . . . . . . . . . . . . 18
225	224	ad2antrr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
226		simplr 761	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
227		elfzelz 11802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
228	227	zred 11042	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
230		nnre 10618	. . . . . . . . . . . . . . . . . . . . . . . . . 26
231	230	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
232		nnne0 10644	. . . . . . . . . . . . . . . . . . . . . . . . . 26
233	232	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
234	229, 231, 233	redivcld 10437	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
235		elfzle1 11804	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	228, 235	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
237		nnrp 11313	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237	rpregt0d 11349	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
239		divge0 10476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
240	236, 238, 239	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
241		elfzle2 11805	. . . . . . . . . . . . . . . . . . . . . . . . . 26
242	241	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
243		1red 9660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	237	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
245	229, 243, 244	ledivmuld 11393	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
246		nncn 10619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
247	246	mulid1d 9662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
248	247	breq2d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
249	248	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
250	245, 249	bitrd 257	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
251	242, 250	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
252	39, 17	elicc2i 11702	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
253	234, 240, 251, 252	syl3anbrc 1190	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
254	253	ancoms 455	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
255		elsni 4022	. . . . . . . . . . . . . . . . . . . . . . . 24
256	255	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . 23
257	256	eleq1d 2492	. . . . . . . . . . . . . . . . . . . . . 22
258	254, 257	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . 21 $/\$
259	258	impr 624	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
260	226, 259	sylan 474	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
261		elun 3607	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
262