Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem5 Structured version   Unicode version

Theorem subfacp1lem5 24872
 Description: Lemma for subfacp1 24874. In subfacp1lem6 24873 we cut up the set of all derangements on first according to the value at , and then by whether or not . In this lemma, we show that the subset of all derangements with for fixed is in bijection with derangements of , because pre-composing with the function swaps and and turns the function into a bijection with and for all other , so dropping the point at yields a derangement on the remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d
subfac.n
subfacp1lem.a
subfacp1lem1.n
subfacp1lem1.m
subfacp1lem1.x
subfacp1lem1.k
subfacp1lem5.b
subfacp1lem5.f
subfacp1lem5.c
Assertion
Ref Expression
subfacp1lem5
Distinct variable groups:   ,,,,,   ,,,,   ,,,,,   ,,,,   ,,   ,,   ,   ,,,,   ,,,,   ,,,
Allowed substitution hints:   (,,)   ()   (,,)   (,,,)   (,)   ()   ()   ()

Proof of Theorem subfacp1lem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subfacp1lem.a . . . . . . . 8
2 fzfi 11313 . . . . . . . . 9
3 deranglem 24854 . . . . . . . . 9
42, 3ax-mp 8 . . . . . . . 8
51, 4eqeltri 2508 . . . . . . 7
6 subfacp1lem5.b . . . . . . . 8
7 ssrab2 3430 . . . . . . . 8
86, 7eqsstri 3380 . . . . . . 7
9 ssfi 7331 . . . . . . 7
105, 8, 9mp2an 655 . . . . . 6
1110elexi 2967 . . . . 5
1211a1i 11 . . . 4
13 subfacp1lem5.c . . . . . . 7
14 fzfi 11313 . . . . . . . 8
15 deranglem 24854 . . . . . . . 8
1614, 15ax-mp 8 . . . . . . 7
1713, 16eqeltri 2508 . . . . . 6
1817elexi 2967 . . . . 5
1918a1i 11 . . . 4
20 derang.d . . . . . . . . . . . . 13
21 subfac.n . . . . . . . . . . . . 13
22 subfacp1lem1.n . . . . . . . . . . . . 13
23 subfacp1lem1.m . . . . . . . . . . . . 13
24 subfacp1lem1.x . . . . . . . . . . . . 13
25 subfacp1lem1.k . . . . . . . . . . . . 13
26 subfacp1lem5.f . . . . . . . . . . . . 13
27 f1oi 5715 . . . . . . . . . . . . . 14
2827a1i 11 . . . . . . . . . . . . 13
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 24868 . . . . . . . . . . . 12
3029simp1d 970 . . . . . . . . . . 11
3130adantr 453 . . . . . . . . . 10
32 simpr 449 . . . . . . . . . . . . . 14
33 fveq1 5729 . . . . . . . . . . . . . . . . 17
3433eqeq1d 2446 . . . . . . . . . . . . . . . 16
35 fveq1 5729 . . . . . . . . . . . . . . . . 17
3635neeq1d 2616 . . . . . . . . . . . . . . . 16
3734, 36anbi12d 693 . . . . . . . . . . . . . . 15
3837, 6elrab2 3096 . . . . . . . . . . . . . 14
3932, 38sylib 190 . . . . . . . . . . . . 13
4039simpld 447 . . . . . . . . . . . 12
41 vex 2961 . . . . . . . . . . . . 13
42 f1oeq1 5667 . . . . . . . . . . . . . 14
43 fveq1 5729 . . . . . . . . . . . . . . . 16
4443neeq1d 2616 . . . . . . . . . . . . . . 15
4544ralbidv 2727 . . . . . . . . . . . . . 14
4642, 45anbi12d 693 . . . . . . . . . . . . 13
4741, 46, 1elab2 3087 . . . . . . . . . . . 12
4840, 47sylib 190 . . . . . . . . . . 11
4948simpld 447 . . . . . . . . . 10
50 f1oco 5700 . . . . . . . . . 10
5131, 49, 50syl2anc 644 . . . . . . . . 9
52 f1of1 5675 . . . . . . . . 9
53 df-f1 5461 . . . . . . . . . 10
5453simprbi 452 . . . . . . . . 9
5551, 52, 543syl 19 . . . . . . . 8
56 f1ofn 5677 . . . . . . . . . . 11
57 fnresdm 5556 . . . . . . . . . . 11
58 f1oeq1 5667 . . . . . . . . . . 11
5951, 56, 57, 584syl 20 . . . . . . . . . 10
6051, 59mpbird 225 . . . . . . . . 9
61 f1ofo 5683 . . . . . . . . 9
6260, 61syl 16 . . . . . . . 8
63 1ex 9088 . . . . . . . . . . 11
6463, 63f1osn 5717 . . . . . . . . . 10
6551, 56syl 16 . . . . . . . . . . . . 13
6622peano2nnd 10019 . . . . . . . . . . . . . . . 16
67 nnuz 10523 . . . . . . . . . . . . . . . 16
6866, 67syl6eleq 2528 . . . . . . . . . . . . . . 15
69 eluzfz1 11066 . . . . . . . . . . . . . . 15
7068, 69syl 16 . . . . . . . . . . . . . 14
7170adantr 453 . . . . . . . . . . . . 13
72 fnressn 5920 . . . . . . . . . . . . 13
7365, 71, 72syl2anc 644 . . . . . . . . . . . 12
74 f1of 5676 . . . . . . . . . . . . . . . . 17
7549, 74syl 16 . . . . . . . . . . . . . . . 16
76 fvco3 5802 . . . . . . . . . . . . . . . 16
7775, 71, 76syl2anc 644 . . . . . . . . . . . . . . 15
7839simprd 451 . . . . . . . . . . . . . . . . 17
7978simpld 447 . . . . . . . . . . . . . . . 16
8079fveq2d 5734 . . . . . . . . . . . . . . 15
8129simp3d 972 . . . . . . . . . . . . . . . 16
8281adantr 453 . . . . . . . . . . . . . . 15
8377, 80, 823eqtrd 2474 . . . . . . . . . . . . . 14
8483opeq2d 3993 . . . . . . . . . . . . 13
8584sneqd 3829 . . . . . . . . . . . 12
8673, 85eqtrd 2470 . . . . . . . . . . 11
87 f1oeq1 5667 . . . . . . . . . . 11
8886, 87syl 16 . . . . . . . . . 10
8964, 88mpbiri 226 . . . . . . . . 9
90 f1ofo 5683 . . . . . . . . 9
9189, 90syl 16 . . . . . . . 8
92 resdif 5698 . . . . . . . 8
9355, 62, 91, 92syl3anc 1185 . . . . . . 7
94 fzsplit 11079 . . . . . . . . . . . 12
9570, 94syl 16 . . . . . . . . . . 11
96 1z 10313 . . . . . . . . . . . . 13
97 fzsn 11096 . . . . . . . . . . . . 13
9896, 97ax-mp 8 . . . . . . . . . . . 12
99 1p1e2 10096 . . . . . . . . . . . . 13
10099oveq1i 6093 . . . . . . . . . . . 12
10198, 100uneq12i 3501 . . . . . . . . . . 11
10295, 101syl6req 2487 . . . . . . . . . 10
10370snssd 3945 . . . . . . . . . . 11
104 incom 3535 . . . . . . . . . . . 12
105 1lt2 10144 . . . . . . . . . . . . . . 15
106 1re 9092 . . . . . . . . . . . . . . . 16
107 2re 10071 . . . . . . . . . . . . . . . 16
108106, 107ltnlei 9196 . . . . . . . . . . . . . . 15
109105, 108mpbi 201 . . . . . . . . . . . . . 14
110 elfzle1 11062 . . . . . . . . . . . . . 14
111109, 110mto 170 . . . . . . . . . . . . 13
112 disjsn 3870 . . . . . . . . . . . . 13
113111, 112mpbir 202 . . . . . . . . . . . 12
114104, 113eqtri 2458 . . . . . . . . . . 11
115 uneqdifeq 3718 . . . . . . . . . . 11
116103, 114, 115sylancl 645 . . . . . . . . . 10
117102, 116mpbid 203 . . . . . . . . 9
118117adantr 453 . . . . . . . 8
119 reseq2 5143 . . . . . . . . . 10
120 f1oeq1 5667 . . . . . . . . . 10
121119, 120syl 16 . . . . . . . . 9
122 f1oeq2 5668 . . . . . . . . 9
123 f1oeq3 5669 . . . . . . . . 9
124121, 122, 1233bitrd 272 . . . . . . . 8
125118, 124syl 16 . . . . . . 7
12693, 125mpbid 203 . . . . . 6
12775adantr 453 . . . . . . . . 9
128 fzp1ss 11100 . . . . . . . . . . . 12
12996, 128ax-mp 8 . . . . . . . . . . 11
130100, 129eqsstr3i 3381 . . . . . . . . . 10
131 simpr 449 . . . . . . . . . 10
132130, 131sseldi 3348 . . . . . . . . 9
133 fvco3 5802 . . . . . . . . 9
134127, 132, 133syl2anc 644 . . . . . . . 8
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 24871 . . . . . . . . . . . 12
136135fveq1d 5732 . . . . . . . . . . 11
137136ad2antrr 708 . . . . . . . . . 10
13878simprd 451 . . . . . . . . . . . . . . 15
139138, 82neeqtrrd 2627 . . . . . . . . . . . . . 14
140139adantr 453 . . . . . . . . . . . . 13
141 fveq2 5730 . . . . . . . . . . . . . 14
142 fveq2 5730 . . . . . . . . . . . . . 14
143141, 142neeq12d 2618 . . . . . . . . . . . . 13
144140, 143syl5ibrcom 215 . . . . . . . . . . . 12
145130sseli 3346 . . . . . . . . . . . . . . . 16
14648simprd 451 . . . . . . . . . . . . . . . . 17
147146r19.21bi 2806 . . . . . . . . . . . . . . . 16
148145, 147sylan2 462 . . . . . . . . . . . . . . 15
149148adantrr 699 . . . . . . . . . . . . . 14
15025eleq2i 2502 . . . . . . . . . . . . . . . . 17
151 eldifsn 3929 . . . . . . . . . . . . . . . . 17
152150, 151bitri 242 . . . . . . . . . . . . . . . 16
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 24869 . . . . . . . . . . . . . . . . 17
154 fvresi 5926 . . . . . . . . . . . . . . . . . 18
155154adantl 454 . . . . . . . . . . . . . . . . 17
156153, 155eqtrd 2470 . . . . . . . . . . . . . . . 16
157152, 156sylan2br 464 . . . . . . . . . . . . . . 15
158157adantlr 697 . . . . . . . . . . . . . 14
159149, 158neeqtrrd 2627 . . . . . . . . . . . . 13
160159expr 600 . . . . . . . . . . . 12
161144, 160pm2.61dne 2683 . . . . . . . . . . 11
162161necomd 2689 . . . . . . . . . 10
163137, 162eqnetrd 2621 . . . . . . . . 9
16431adantr 453 . . . . . . . . . . 11
165 ffvelrn 5870 . . . . . . . . . . . 12
16675, 145, 165syl2an 465 . . . . . . . . . . 11
167 f1ocnvfv 6018 . . . . . . . . . . 11
168164, 166, 167syl2anc 644 . . . . . . . . . 10
169168necon3d 2641 . . . . . . . . 9
170163, 169mpd 15 . . . . . . . 8
171134, 170eqnetrd 2621 . . . . . . 7
172171ralrimiva 2791 . . . . . 6
173 f1of 5676 . . . . . . . . . . . . 13
17427, 173ax-mp 8 . . . . . . . . . . . 12
175 difexg 4353 . . . . . . . . . . . . . 14
17614, 175ax-mp 8 . . . . . . . . . . . . 13
17725, 176eqeltri 2508 . . . . . . . . . . . 12
178 fex 5971 . . . . . . . . . . . 12
179174, 177, 178mp2an 655 . . . . . . . . . . 11
180 prex 4408 . . . . . . . . . . 11
181179, 180unex 4709 . . . . . . . . . 10
18226, 181eqeltri 2508 . . . . . . . . 9
183182, 41coex 5415 . . . . . . . 8
184183resex 5188 . . . . . . 7
185 f1oeq1 5667 . . . . . . . 8
186 fveq1 5729 . . . . . . . . . . 11
187 fvres 5747 . . . . . . . . . . 11
188186, 187sylan9eq 2490 . . . . . . . . . 10
189188neeq1d 2616 . . . . . . . . 9
190189ralbidva 2723 . . . . . . . 8
191185, 190anbi12d 693 . . . . . . 7
192184, 191, 13elab2 3087 . . . . . 6
193126, 172, 192sylanbrc 647 . . . . 5
194193ex 425 . . . 4
19530adantr 453 . . . . . . . 8
196 simpr 449 . . . . . . . . . . . 12
197 vex 2961 . . . . . . . . . . . . 13
198 f1oeq1 5667 . . . . . . . . . . . . . 14
199 fveq1 5729 . . . . . . . . . . . . . . . 16
200199neeq1d 2616 . . . . . . . . . . . . . . 15
201200ralbidv 2727 . . . . . . . . . . . . . 14
202198, 201anbi12d 693 . . . . . . . . . . . . 13
203197, 202, 13elab2 3087 . . . . . . . . . . . 12
204196, 203sylib 190 . . . . . . . . . . 11
205204simpld 447 . . . . . . . . . 10
206 f1oun 5696 . . . . . . . . . . 11
207114, 114, 206mpanr12 668 . . . . . . . . . 10
20864, 205, 207sylancr 646 . . . . . . . . 9
209 f1oeq2 5668 . . . . . . . . . . . 12
210 f1oeq3 5669 . . . . . . . . . . . 12
211209, 210bitrd 246 . . . . . . . . . . 11
212102, 211syl 16 . . . . . . . . . 10
213212biimpa 472 . . . . . . . . 9
214208, 213syldan 458 . . . . . . . 8
215 f1oco 5700 . . . . . . . 8
216195, 214, 215syl2anc 644 . . . . . . 7
217 f1of 5676 . . . . . . . . . . 11
218214, 217syl 16 . . . . . . . . . 10
219 fvco3 5802 . . . . . . . . . 10
220218, 219sylan 459 . . . . . . . . 9
221136ad2antrr 708 . . . . . . . . . . 11
222 simpr 449 . . . . . . . . . . . . . 14
223102ad2antrr 708 . . . . . . . . . . . . . 14
224222, 223eleqtrrd 2515 . . . . . . . . . . . . 13
225 elun 3490 . . . . . . . . . . . . 13
226224, 225sylib 190 . . . . . . . . . . . 12
227 nelne2 2696 . . . . . . . . . . . . . . . . . 18
22823, 111, 227sylancl 645 . . . . . . . . . . . . . . . . 17
229228adantr 453 . . . . . . . . . . . . . . . 16
23029simp2d 971 . . . . . . . . . . . . . . . . 17
231230adantr 453 . . . . . . . . . . . . . . . 16
232 f1ofun 5678 . . . . . . . . . . . . . . . . . . 19
233208, 232syl 16 . . . . . . . . . . . . . . . . . 18
234 ssun1 3512 . . . . . . . . . . . . . . . . . . 19
23563snid 3843 . . . . . . . . . . . . . . . . . . . 20
23663dmsnop 5346 . . . . . . . . . . . . . . . . . . . 20
237235, 236eleqtrri 2511 . . . . . . . . . . . . . . . . . . 19
238 funssfv 5748 . . . . . . . . . . . . . . . . . . 19
239234, 237, 238mp3an23 1272 . . . . . . . . . . . . . . . . . 18
240233, 239syl 16 . . . . . . . . . . . . . . . . 17
24163, 63fvsn 5928 . . . . . . . . . . . . . . . . 17
242240, 241syl6eq 2486 . . . . . . . . . . . . . . . 16
243229, 231, 2423netr4d 2630 . . . . . . . . . . . . . . 15
244 elsni 3840 . . . . . . . . . . . . . . . . 17
245244fveq2d 5734 . . . . . . . . . . . . . . . 16
246244fveq2d 5734 . . . . . . . . . . . . . . . 16
247245, 246neeq12d 2618 . . . . . . . . . . . . . . 15
248243, 247syl5ibrcom 215 . . . . . . . . . . . . . 14
249248imp 420 . . . . . . . . . . . . 13
250233adantr 453 . . . . . . . . . . . . . . . 16
251 ssun2 3513 . . . . . . . . . . . . . . . . 17
252251a1i 11 . . . . . . . . . . . . . . . 16
253 f1odm 5680 . . . . . . . . . . . . . . . . . . 19
254205, 253syl 16 . . . . . . . . . . . . . . . . . 18
255254eleq2d 2505 . . . . . . . . . . . . . . . . 17
256255biimpar 473 . . . . . . . . . . . . . . . 16
257 funssfv 5748 . . . . . . . . . . . . . . . 16
258250, 252, 256, 257syl3anc 1185 . . . . . . . . . . . . . . 15
259 f1of 5676 . . . . . . . . . . . . . . . . . . . . . 22
260205, 259syl 16 . . . . . . . . . . . . . . . . . . . . 21
26123adantr 453 . . . . . . . . . . . . . . . . . . . . 21
262260, 261ffvelrnd 5873 . . . . . . . . . . . . . . . . . . . 20
263 nelne2 2696 . . . . . . . . . . . . . . . . . . . 20
264262, 111, 263sylancl 645 . . . . . . . . . . . . . . . . . . 19
265264adantr 453 . . . . . . . . . . . . . . . . . 18
26681ad2antrr 708 . . . . . . . . . . . . . . . . . 18
267265, 266neeqtrrd 2627 . . . . . . . . . . . . . . . . 17
268 fveq2 5730 . . . . . . . . . . . . . . . . . 18
269268, 142neeq12d 2618 . . . . . . . . . . . . . . . . 17
270267, 269syl5ibrcom 215 . . . . . . . . . . . . . . . 16
271204simprd 451 . . . . . . . . . . . . . . . . . . . 20
272271r19.21bi 2806 . . . . . . . . . . . . . . . . . . 19
273272adantrr 699 . . . . . . . . . . . . . . . . . 18
274157adantlr 697 . . . . . . . . . . . . . . . . . 18
275273, 274neeqtrrd 2627 . . . . . . . . . . . . . . . . 17
276275expr 600 . . . . . . . . . . . . . . . 16
277270, 276pm2.61dne 2683 . . . . . . . . . . . . . . 15
278258, 277eqnetrd 2621 . . . . . . . . . . . . . 14
279278necomd 2689 . . . . . . . . . . . . 13
280249, 279jaodan 762 . . . . . . . . . . . 12
281226, 280syldan 458 . . . . . . . . . . 11
282221, 281eqnetrd 2621 . . . . . . . . . 10
283195adantr 453 . . . . . . . . . . . 12
284218ffvelrnda 5872 . . . . . . . . . . . 12
285 f1ocnvfv 6018 . . . . . . . . . . . 12
286283, 284, 285syl2anc 644 . . . . . . . . . . 11
287286necon3d 2641 . . . . . . . . . 10
288282, 287mpd 15 . . . . . . . . 9
289220, 288eqnetrd 2621 . . . . . . . 8
290289ralrimiva 2791 . . . . . . 7
291 snex 4407 . . . . . . . . . 10
292291, 197unex 4709 . . . . . . . . 9
293182, 292coex 5415 . . . . . . . 8
294 f1oeq1 5667 . . . . . . . . 9
295 fveq1 5729 . . . . . . . . . . 11
296295neeq1d 2616 . . . . . . . . . 10
297296ralbidv 2727 . . . . . . . . 9
298294, 297anbi12d 693 . . . . . . . 8
299293, 298, 1elab2 3087 . . . . . . 7
300216, 290, 299sylanbrc 647 . . . . . 6
30170adantr 453 . . . . . . . . 9
302 fvco3 5802 . . . . . . . . 9
303218, 301, 302syl2anc 644 . . . . . . . 8
304242fveq2d 5734 . . . . . . . 8
305303, 304, 2313eqtrd 2474 . . . . . . 7
306130, 23sseldi 3348 . . . . . . . . . . 11
307306adantr 453 . . . . . . . . . 10
308 fvco3 5802 . . . . . . . . . 10
309218, 307, 308syl2anc 644 . . . . . . . . 9
310251a1i 11 . . . . . . . . . . 11
311261, 254eleqtrrd 2515 . . . . . . . . . . 11
312 funssfv 5748 . . . . . . . . . . 11
313233, 310, 311, 312syl3anc 1185 . . . . . . . . . 10
314313fveq2d 5734 . . . . . . . . 9
315309, 314eqtrd 2470 . . . . . . . 8
316135fveq1d 5732 . . . . . . . . . . . 12
317316, 230eqtrd 2470 . . . . . . . . . . 11
318317adantr 453 . . . . . . . . . 10
319 id 21 . . . . . . . . . . . . . 14
320268, 319neeq12d 2618 . . . . . . . . . . . . 13
321320rspcv 3050 . . . . . . . . . . . 12
322261, 271, 321sylc 59 . . . . . . . . . . 11
323322necomd 2689 . . . . . . . . . 10
324318, 323eqnetrd 2621 . . . . . . . . 9
325130, 262sseldi 3348 . . . . . . . . . . 11
326 f1ocnvfv 6018 . . . . . . . . . . 11
327195, 325, 326syl2anc 644 . . . . . . . . . 10
328327necon3d 2641 . . . . . . . . 9
329324, 328mpd 15 . . . . . . . 8
330315, 329eqnetrd 2621 . . . . . . 7
331305, 330jca 520 . . . . . 6
332 fveq1 5729 . . . . . . . . 9
333332eqeq1d 2446 . . . . . . . 8
334 fveq1 5729 . . . . . . . . 9
335334neeq1d 2616 . . . . . . . 8
336333, 335anbi12d 693 . . . . . . 7
337336, 6elrab2 3096 . . . . . 6
338300, 331, 337sylanbrc 647 . . . . 5
339338ex 425 . . . 4
34030adantr 453 . . . . . . . 8
341 f1of1 5675 . . . . . . . 8
342340, 341syl 16 . . . . . . 7
343 f1of 5676 . . . . . . . . 9
344340, 343syl 16 . . . . . . . 8
34575adantrr 699 . . . . . . . 8
346 fco 5602 . . . . . . . 8
347344, 345, 346syl2anc 644 . . . . . . 7
348218adantrl 698 . . . . . . 7
349 cocan1 6026 . . . . . . 7
350342, 347, 348, 349syl3anc 1185 . . . . . 6
351 coass 5390 . . . . . . . 8
352135coeq1d 5036 . . . . . . . . . . . 12
353 f1ococnv1 5706 . . . . . . . . . . . . 13
35430, 353syl 16 . . . . . . . . . . . 12
355352, 354eqtr3d 2472 . . . . . . . . . . 11
356355adantr 453 . . . . . . . . . 10
357356coeq1d 5036 . . . . . . . . 9
358 fcoi2 5620 . . . . . . . . . 10
359345, 358syl 16 . . . . . . . . 9
360357, 359eqtrd 2470 . . . . . . . 8
361351, 360syl5eqr 2484 . . . . . . 7
362361eqeq1d 2446 . . . . . 6
36383adantrr 699 . . . . . . . . . . . . 13
364242adantrl 698 . . . . . . . . . . . . 13
365363, 364eqtr4d 2473 . . . . . . . . . . . 12
366 fveq2 5730 . . . . . . . . . . . . . 14
367 fveq2 5730 . . . . . . . . . . . . . 14
368366, 367eqeq12d 2452 . . . . . . . . . . . . 13
36963, 368ralsn 3851 . . . . . . . . . . . 12
370365, 369sylibr 205 . . . . . . . . . . 11
371370biantrurd 496 . . . . . . . . . 10
372 ralunb 3530 . . . . . . . . . 10
373371, 372syl6bbr 256 . . . . . . . . 9
374187adantl 454 . . . . . . . . . . . 12
375374eqcomd 2443 . . . . . . . . . . 11
376258adantlrl 702 . . . . . . . . . . 11
377375, 376eqeq12d 2452 . . . . . . . . . 10
378377ralbidva 2723 . . . . . . . . 9
379102adantr 453 . . . . . . . . . 10
380379raleqdv 2912 . . . . . . . . 9
381373, 378, 3803bitr3rd 277 . . . . . . . 8
38265adantrr 699 . . . . . . . . 9
383214adantrl 698 . . . . . . . . . 10