poimirlem31 - Mathbox for Brendan Leahy

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

Theorem poimirlem31 32035

Description: Lemma for poimir 32037, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 32034 and poimirlem28 32032. 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 3976	. . . 4 $\/$
2		simprr 774	. . . . . . 7 $/\$ $/\$
3		1eluzge0 11226	. . . . . . . . . . 11
4		fzss1 11863	. . . . . . . . . . 11
5	3, 4	ax-mp 5	. . . . . . . . . 10
6	5	sseli 3414	. . . . . . . . 9
7	6	anim2i 579	. . . . . . . 8 $/\$ $/\$
8		eleq1 2537	. . . . . . . . . . . . 13
9	8	anbi2d 718	. . . . . . . . . . . 12 $/\$ $/\$
10	9	anbi2d 718	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
11		eqeq1 2475	. . . . . . . . . . . 12 $/\$ $/\$
12	11	rexbidv 2892	. . . . . . . . . . 11 $/\$ $/\$
13	10, 12	imbi12d 327	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		poimirlem31.5	. . . . . . . . . 10 $/\$ $/\$ $/\$
15	13, 14	chvarv 2120	. . . . . . . . 9 $/\$ $/\$ $/\$
16		elfzle1 11828	. . . . . . . . . . . . 13
17		1re 9660	. . . . . . . . . . . . . 14
18		elfzelz 11826	. . . . . . . . . . . . . . 15
19	18	zred 11063	. . . . . . . . . . . . . 14
20		lenlt 9730	. . . . . . . . . . . . . 14 $/\$
21	17, 19, 20	sylancr 676	. . . . . . . . . . . . 13
22	16, 21	mpbid 215	. . . . . . . . . . . 12
23		elsni 3985	. . . . . . . . . . . . 13
24		0lt1 10157	. . . . . . . . . . . . 13
25	23, 24	syl6eqbr 4433	. . . . . . . . . . . 12
26	22, 25	nsyl 125	. . . . . . . . . . 11
27		ltso 9732	. . . . . . . . . . . . . . 15
28		snfi 7668	. . . . . . . . . . . . . . . . 17
29		fzfi 12223	. . . . . . . . . . . . . . . . . 18
30		rabfi 7814	. . . . . . . . . . . . . . . . . 18 $/\$
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$
32		unfi 7856	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33	28, 31, 32	mp2an 686	. . . . . . . . . . . . . . . 16 $/\$
34		c0ex 9655	. . . . . . . . . . . . . . . . . 18
35	34	snid 3988	. . . . . . . . . . . . . . . . 17
36		elun1 3592	. . . . . . . . . . . . . . . . 17 $/\$
37		ne0i 3728	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	35, 36, 37	mp2b 10	. . . . . . . . . . . . . . . 16 $/\$
39		0re 9661	. . . . . . . . . . . . . . . . . 18
40		snssi 4107	. . . . . . . . . . . . . . . . . 18
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17
42		ssrab2 3500	. . . . . . . . . . . . . . . . . 18 $/\$
43	18	ssriv 3422	. . . . . . . . . . . . . . . . . . 19
44		zssre 10968	. . . . . . . . . . . . . . . . . . 19
45	43, 44	sstri 3427	. . . . . . . . . . . . . . . . . 18
46	42, 45	sstri 3427	. . . . . . . . . . . . . . . . 17 $/\$
47	41, 46	unssi 3600	. . . . . . . . . . . . . . . 16 $/\$
48	33, 38, 47	3pm3.2i 1208	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
49		fisupcl 8003	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	27, 48, 49	mp2an 686	. . . . . . . . . . . . . 14 $/\$ $/\$
51		eleq1 2537	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
52	50, 51	mpbiri 241	. . . . . . . . . . . . 13 $/\$ $/\$
53		elun 3565	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$
54	52, 53	sylib 201	. . . . . . . . . . . 12 $/\$ $\/$ $/\$
55		oveq2 6316	. . . . . . . . . . . . . . . 16
56	55	raleqdv 2979	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	elrab 3184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
58		elfzuz 11822	. . . . . . . . . . . . . . . 16
59		eluzfz2 11833	. . . . . . . . . . . . . . . 16
60	58, 59	syl 17	. . . . . . . . . . . . . . 15
61		simpl 464	. . . . . . . . . . . . . . . 16 $/\$
62	61	ralimi 2796	. . . . . . . . . . . . . . 15 $/\$
63		fveq2 5879	. . . . . . . . . . . . . . . . 17
64	63	breq2d 4407	. . . . . . . . . . . . . . . 16
65	64	rspcva 3134	. . . . . . . . . . . . . . 15 $/\$
66	60, 62, 65	syl2an 485	. . . . . . . . . . . . . 14 $/\$ $/\$
67	57, 66	sylbi 200	. . . . . . . . . . . . 13 $/\$
68	67	orim2i 527	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
69	54, 68	syl 17	. . . . . . . . . . 11 $/\$ $\/$
70		orel1 389	. . . . . . . . . . 11 $\/$
71	26, 69, 70	syl2im 38	. . . . . . . . . 10 $/\$
72	71	reximdv 2857	. . . . . . . . 9 $/\$
73	15, 72	syl5 32	. . . . . . . 8 $/\$ $/\$
74	7, 73	sylan2i 667	. . . . . . 7 $/\$ $/\$
75	2, 74	mpcom 36	. . . . . 6 $/\$ $/\$
76		breq 4397	. . . . . . 7
77	76	rexbidv 2892	. . . . . 6
78	75, 77	syl5ibrcom 230	. . . . 5 $/\$ $/\$
79		poimir.0	. . . . . . . . . . . . . . . 16
80	79	nnzd 11062	. . . . . . . . . . . . . . 15
81		elfzm1b 11898	. . . . . . . . . . . . . . 15 $/\$
82	18, 80, 81	syl2anr 486	. . . . . . . . . . . . . 14 $/\$
83	82	biimpd 212	. . . . . . . . . . . . 13 $/\$
84	83	ex 441	. . . . . . . . . . . 12
85	84	pm2.43d 49	. . . . . . . . . . 11
86	79	nncnd 10647	. . . . . . . . . . . . . . 15
87		npcan1 10065	. . . . . . . . . . . . . . 15
88	86, 87	syl 17	. . . . . . . . . . . . . 14
89		nnm1nn0 10935	. . . . . . . . . . . . . . . . 17
90	79, 89	syl 17	. . . . . . . . . . . . . . . 16
91	90	nn0zd 11061	. . . . . . . . . . . . . . 15
92		uzid 11197	. . . . . . . . . . . . . . 15
93		peano2uz 11235	. . . . . . . . . . . . . . 15
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . 14
95	88, 94	eqeltrrd 2550	. . . . . . . . . . . . 13
96		fzss2 11864	. . . . . . . . . . . . 13
97	95, 96	syl 17	. . . . . . . . . . . 12
98	97	sseld 3417	. . . . . . . . . . 11
99	85, 98	syld 44	. . . . . . . . . 10
100	99	anim2d 575	. . . . . . . . 9 $/\$ $/\$
101	100	imp 436	. . . . . . . 8 $/\$ $/\$ $/\$
102		ovex 6336	. . . . . . . . 9
103		eleq1 2537	. . . . . . . . . . . 12
104	103	anbi2d 718	. . . . . . . . . . 11 $/\$ $/\$
105	104	anbi2d 718	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
106		eqeq1 2475	. . . . . . . . . . 11 $/\$ $/\$
107	106	rexbidv 2892	. . . . . . . . . 10 $/\$ $/\$
108	105, 107	imbi12d 327	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	102, 108, 14	vtocl 3086	. . . . . . . 8 $/\$ $/\$ $/\$
110	101, 109	syldan 478	. . . . . . 7 $/\$ $/\$ $/\$
111		eleq1 2537	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
112	50, 111	mpbiri 241	. . . . . . . . . . . . . . 15 $/\$ $/\$
113		elun 3565	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
114	102	elsnc 3984	. . . . . . . . . . . . . . . . 17
115		oveq2 6316	. . . . . . . . . . . . . . . . . . 19
116	115	raleqdv 2979	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
117	116	elrab 3184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	114, 117	orbi12i 530	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $\/$ $/\$ $/\$
119	113, 118	bitri 257	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$ $/\$
120	112, 119	sylib 201	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$
121	120	a1i 11	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$
122		ltm1 10467	. . . . . . . . . . . . . . . . . 18
123		peano2rem 9961	. . . . . . . . . . . . . . . . . . 19
124		ltnle 9731	. . . . . . . . . . . . . . . . . . 19 $/\$
125	123, 124	mpancom 682	. . . . . . . . . . . . . . . . . 18
126	122, 125	mpbid 215	. . . . . . . . . . . . . . . . 17
127	19, 126	syl 17	. . . . . . . . . . . . . . . 16
128		breq2 4399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	128	notbid 301	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	127, 129	syl5ibcom 228	. . . . . . . . . . . . . . 15 $/\$ $/\$
131		elun2 3593	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132		fimaxre2 10574	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
133	47, 33, 132	mp2an 686	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	47, 38, 133	3pm3.2i 1208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
135	134	suprubii 10604	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
136	131, 135	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
137	136	con3i 142	. . . . . . . . . . . . . . . 16 $/\$ $/\$
138		ianor 496	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$ $/\$
139	138, 57	xchnxbir 316	. . . . . . . . . . . . . . . 16 $/\$ $\/$ $/\$
140	137, 139	sylib 201	. . . . . . . . . . . . . . 15 $/\$ $\/$ $/\$
141	130, 140	syl6 33	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
142		pm2.63 805	. . . . . . . . . . . . . . 15 $\/$ $/\$ $\/$ $/\$ $/\$
143	142	orcs 401	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
144	141, 143	syld 44	. . . . . . . . . . . . 13 $/\$ $/\$
145	121, 144	jcad 542	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
146		andir 885	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
147		1p0e1 10744	. . . . . . . . . . . . . . . . . 18
148	18	zcnd 11064	. . . . . . . . . . . . . . . . . . . 20
149		ax-1cn 9615	. . . . . . . . . . . . . . . . . . . . 21
150		0cn 9653	. . . . . . . . . . . . . . . . . . . . 21
151		subadd 9898	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
152	149, 150, 151	mp3an23 1382	. . . . . . . . . . . . . . . . . . . 20
153	148, 152	syl 17	. . . . . . . . . . . . . . . . . . 19
154	153	biimpa 492	. . . . . . . . . . . . . . . . . 18 $/\$
155	147, 154	syl5reqr 2520	. . . . . . . . . . . . . . . . 17 $/\$
156		1z 10991	. . . . . . . . . . . . . . . . . . . . . 22
157		fzsn 11866	. . . . . . . . . . . . . . . . . . . . . 22
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
159		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21
160		sneq 3969	. . . . . . . . . . . . . . . . . . . . 21
161	158, 159, 160	3eqtr4a 2531	. . . . . . . . . . . . . . . . . . . 20
162	161	raleqdv 2979	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
163	162	notbid 301	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
164	163	biimpd 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
165	155, 164	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
166	165	expimpd 614	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
167		ralun 3607	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
168		npcan1 10065	. . . . . . . . . . . . . . . . . . . . . . . . 25
169	148, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
170	169, 58	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . 23
171		peano2zm 11004	. . . . . . . . . . . . . . . . . . . . . . . . 25
172		uzid 11197	. . . . . . . . . . . . . . . . . . . . . . . . 25
173		peano2uz 11235	. . . . . . . . . . . . . . . . . . . . . . . . 25
174	18, 171, 172, 173	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24
175	169, 174	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . . . . . 23
176		fzsplit2 11850	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
177	170, 175, 176	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22
178	169	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . 24
179		fzsn 11866	. . . . . . . . . . . . . . . . . . . . . . . . 25
180	18, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
181	178, 180	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	uneq2d 3579	. . . . . . . . . . . . . . . . . . . . . 22
183	177, 182	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . 21
184	183	raleqdv 2979	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
185	167, 184	syl5ibr 229	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
186	185	expdimp 444	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
187	186	con3d 140	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
188	187	adantrl 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
189	188	expimpd 614	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
190	166, 189	jaod 387	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
191	146, 190	syl5bi 225	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
192		fveq2 5879	. . . . . . . . . . . . . . . . . 18
193	192	neeq1d 2702	. . . . . . . . . . . . . . . . 17
194	64, 193	anbi12d 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$
195	194	ralsng 3997	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	195	notbid 301	. . . . . . . . . . . . . 14 $/\$ $/\$
197		ianor 496	. . . . . . . . . . . . . . 15 $/\$ $\/$
198		nne 2647	. . . . . . . . . . . . . . . 16
199	198	orbi2i 528	. . . . . . . . . . . . . . 15 $\/$ $\/$
200	197, 199	bitri 257	. . . . . . . . . . . . . 14 $/\$ $\/$
201	196, 200	syl6bb 269	. . . . . . . . . . . . 13 $/\$ $\/$
202	191, 201	sylibd 222	. . . . . . . . . . . 12 $\/$ $/\$ $/\$ $/\$ $/\$ $\/$
203	145, 202	syld 44	. . . . . . . . . . 11 $/\$ $\/$
204	203	ad2antlr 741	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\/$
205		poimir.1	. . . . . . . . . . . . . . . . . . 19 ↾_t
206		poimir.r	. . . . . . . . . . . . . . . . . . . . . 22
207		retop 21860	. . . . . . . . . . . . . . . . . . . . . . . 24
208	207	fconst6 5786	. . . . . . . . . . . . . . . . . . . . . . 23
209		pttop 20674	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
210	29, 208, 209	mp2an 686	. . . . . . . . . . . . . . . . . . . . . 22
211	206, 210	eqeltri 2545	. . . . . . . . . . . . . . . . . . . . 21
212		poimir.i	. . . . . . . . . . . . . . . . . . . . . 22
213		reex 9648	. . . . . . . . . . . . . . . . . . . . . . 23
214		unitssre 11805	. . . . . . . . . . . . . . . . . . . . . . 23
215		mapss 7532	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
216	213, 214, 215	mp2an 686	. . . . . . . . . . . . . . . . . . . . . 22
217	212, 216	eqsstri 3448	. . . . . . . . . . . . . . . . . . . . 21
218		uniretop 21861	. . . . . . . . . . . . . . . . . . . . . . . 24
219	206, 218	ptuniconst 20690	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
220	29, 207, 219	mp2an 686	. . . . . . . . . . . . . . . . . . . . . 22
221	220	restuni 20255	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ↾_t
222	211, 217, 221	mp2an 686	. . . . . . . . . . . . . . . . . . . 20 ↾_t
223	222, 220	cnf 20339	. . . . . . . . . . . . . . . . . . 19 ↾_t
224	205, 223	syl 17	. . . . . . . . . . . . . . . . . 18
225	224	ad2antrr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
226		simplr 770	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
227		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
228	227	zred 11063	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
230		nnre 10638	. . . . . . . . . . . . . . . . . . . . . . . . . 26
231	230	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
232		nnne0 10664	. . . . . . . . . . . . . . . . . . . . . . . . . 26
233	232	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
234	229, 231, 233	redivcld 10457	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
235		elfzle1 11828	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	228, 235	jca 541	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
237		nnrp 11334	. . . . . . . . . . . . . . . . . . . . . . . . . 26
238	237	rpregt0d 11370	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
239		divge0 10496	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
240	236, 238, 239	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
241		elfzle2 11829	. . . . . . . . . . . . . . . . . . . . . . . . . 26
242	241	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
243		1red 9676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	237	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
245	229, 243, 244	ledivmuld 11414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
246		nncn 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
247	246	mulid1d 9678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
248	247	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
249	248	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
250	245, 249	bitrd 261	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
251	242, 250	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
252	39, 17	elicc2i 11725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
253	234, 240, 251, 252	syl3anbrc 1214	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
254	253	ancoms 460	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
255		elsni 3985	. . . . . . . . . . . . . . . . . . . . . . . 24
256	255	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . 23
257	256	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . 22
258	254, 257	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . 21 $/\$
259	258	impr 631	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
260	226, 259	sylan 479	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
261		elun 3565	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$