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

Theorem subfacp1lem6 24863
 Description: Lemma for subfacp1 24864. By induction, we cut up the set of all derangements on according to the possible values of (since ), and for each set for fixed , the subset of derangements with has size (by subfacp1lem3 24860), while the subset with has size (by subfacp1lem5 24862). Adding it all up yields the desired equation for the number of derangements on . (Contributed by Mario Carneiro, 22-Jan-2015.)
Hypotheses
Ref Expression
derang.d
subfac.n
subfacp1lem.a
Assertion
Ref Expression
subfacp1lem6
Distinct variable groups:   ,,,,   ,,,,   ,   ,,,
Allowed substitution hints:   (,,)   ()

Proof of Theorem subfacp1lem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2nn 10004 . . . . 5
21nnnn0d 10266 . . . 4
3 derang.d . . . . 5
4 subfac.n . . . . 5
53, 4subfacval 24851 . . . 4
62, 5syl 16 . . 3
7 fzfid 11304 . . . . 5
83derangval 24845 . . . . 5
97, 8syl 16 . . . 4
10 subfacp1lem.a . . . . 5
1110fveq2i 5723 . . . 4
129, 11syl6eqr 2485 . . 3
13 nnuz 10513 . . . . . . . . . . 11
141, 13syl6eleq 2525 . . . . . . . . . 10
15 eluzfz1 11056 . . . . . . . . . 10
1614, 15syl 16 . . . . . . . . 9
17 f1of 5666 . . . . . . . . . 10
1817adantr 452 . . . . . . . . 9
19 ffvelrn 5860 . . . . . . . . . 10
2019expcom 425 . . . . . . . . 9
2116, 18, 20syl2im 36 . . . . . . . 8
2221ss2abdv 3408 . . . . . . 7
23 fveq1 5719 . . . . . . . . 9
2423eleq1d 2501 . . . . . . . 8
2524cbvabv 2554 . . . . . . 7
2622, 10, 253sstr4g 3381 . . . . . 6
27 ssabral 3406 . . . . . 6
2826, 27sylib 189 . . . . 5
29 rabid2 2877 . . . . 5
3028, 29sylibr 204 . . . 4
3130fveq2d 5724 . . 3
326, 12, 313eqtrd 2471 . 2
33 elfz1end 11073 . . . 4
341, 33sylib 189 . . 3
35 eleq1 2495 . . . . . . 7
36 oveq2 6081 . . . . . . . . . . . . 13
37 1z 10303 . . . . . . . . . . . . . 14
38 fzsn 11086 . . . . . . . . . . . . . 14
3937, 38ax-mp 8 . . . . . . . . . . . . 13
4036, 39syl6eq 2483 . . . . . . . . . . . 12
4140eleq2d 2502 . . . . . . . . . . 11
42 fvex 5734 . . . . . . . . . . . 12
4342elsnc 3829 . . . . . . . . . . 11
4441, 43syl6bb 253 . . . . . . . . . 10
4544rabbidv 2940 . . . . . . . . 9
4645fveq2d 5724 . . . . . . . 8
47 oveq1 6080 . . . . . . . . . 10
48 1m1e0 10060 . . . . . . . . . 10
4947, 48syl6eq 2483 . . . . . . . . 9
5049oveq1d 6088 . . . . . . . 8
5146, 50eqeq12d 2449 . . . . . . 7
5235, 51imbi12d 312 . . . . . 6
5352imbi2d 308 . . . . 5
54 eleq1 2495 . . . . . . 7
55 oveq2 6081 . . . . . . . . . . 11
5655eleq2d 2502 . . . . . . . . . 10
5756rabbidv 2940 . . . . . . . . 9
5857fveq2d 5724 . . . . . . . 8
59 oveq1 6080 . . . . . . . . 9
6059oveq1d 6088 . . . . . . . 8
6158, 60eqeq12d 2449 . . . . . . 7
6254, 61imbi12d 312 . . . . . 6
6362imbi2d 308 . . . . 5
64 eleq1 2495 . . . . . . 7
65 oveq2 6081 . . . . . . . . . . 11
6665eleq2d 2502 . . . . . . . . . 10
6766rabbidv 2940 . . . . . . . . 9
6867fveq2d 5724 . . . . . . . 8
69 oveq1 6080 . . . . . . . . 9
7069oveq1d 6088 . . . . . . . 8
7168, 70eqeq12d 2449 . . . . . . 7
7264, 71imbi12d 312 . . . . . 6
7372imbi2d 308 . . . . 5
74 eleq1 2495 . . . . . . 7
75 oveq2 6081 . . . . . . . . . . 11
7675eleq2d 2502 . . . . . . . . . 10
7776rabbidv 2940 . . . . . . . . 9
7877fveq2d 5724 . . . . . . . 8
79 oveq1 6080 . . . . . . . . 9
8079oveq1d 6088 . . . . . . . 8
8178, 80eqeq12d 2449 . . . . . . 7
8274, 81imbi12d 312 . . . . . 6
8382imbi2d 308 . . . . 5
84 hash0 11638 . . . . . . 7
85 fveq2 5720 . . . . . . . . . . . . . . . 16
86 id 20 . . . . . . . . . . . . . . . 16
8785, 86neeq12d 2613 . . . . . . . . . . . . . . 15
8887rspcv 3040 . . . . . . . . . . . . . 14
8916, 88syl 16 . . . . . . . . . . . . 13
9089adantld 454 . . . . . . . . . . . 12
9190ss2abdv 3408 . . . . . . . . . . 11
92 df-ne 2600 . . . . . . . . . . . . 13
9323neeq1d 2611 . . . . . . . . . . . . 13
9492, 93syl5bbr 251 . . . . . . . . . . . 12
9594cbvabv 2554 . . . . . . . . . . 11
9691, 10, 953sstr4g 3381 . . . . . . . . . 10
97 ssabral 3406 . . . . . . . . . 10
9896, 97sylib 189 . . . . . . . . 9
99 rabeq0 3641 . . . . . . . . 9
10098, 99sylibr 204 . . . . . . . 8
101100fveq2d 5724 . . . . . . 7
102 nnnn0 10220 . . . . . . . . . . 11
1033, 4subfacf 24853 . . . . . . . . . . . 12
104103ffvelrni 5861 . . . . . . . . . . 11
105102, 104syl 16 . . . . . . . . . 10
106 nnm1nn0 10253 . . . . . . . . . . 11
107103ffvelrni 5861 . . . . . . . . . . 11
108106, 107syl 16 . . . . . . . . . 10
109105, 108nn0addcld 10270 . . . . . . . . 9
110109nn0cnd 10268 . . . . . . . 8
111110mul02d 9256 . . . . . . 7
11284, 101, 1113eqtr4a 2493 . . . . . 6
113112a1d 23 . . . . 5
114 simplr 732 . . . . . . . . . . . 12
115114, 13syl6eleq 2525 . . . . . . . . . . 11
116 peano2fzr 11061 . . . . . . . . . . 11
117115, 116sylancom 649 . . . . . . . . . 10
118117ex 424 . . . . . . . . 9
119118imim1d 71 . . . . . . . 8
120 oveq1 6080 . . . . . . . . . . 11
121 elfzp1 11089 . . . . . . . . . . . . . . . . 17
122115, 121syl 16 . . . . . . . . . . . . . . . 16
123122rabbidv 2940 . . . . . . . . . . . . . . 15
124 unrab 3604 . . . . . . . . . . . . . . 15
125123, 124syl6eqr 2485 . . . . . . . . . . . . . 14
126125fveq2d 5724 . . . . . . . . . . . . 13
127 fzfi 11303 . . . . . . . . . . . . . . . . 17
128 deranglem 24844 . . . . . . . . . . . . . . . . 17
129127, 128ax-mp 8 . . . . . . . . . . . . . . . 16
13010, 129eqeltri 2505 . . . . . . . . . . . . . . 15
131 ssrab2 3420 . . . . . . . . . . . . . . 15
132 ssfi 7321 . . . . . . . . . . . . . . 15
133130, 131, 132mp2an 654 . . . . . . . . . . . . . 14
134 ssrab2 3420 . . . . . . . . . . . . . . 15
135 ssfi 7321 . . . . . . . . . . . . . . 15
136130, 134, 135mp2an 654 . . . . . . . . . . . . . 14
137 inrab 3605 . . . . . . . . . . . . . . 15
138 fzp1disj 11097 . . . . . . . . . . . . . . . . . 18
13942elsnc 3829 . . . . . . . . . . . . . . . . . . . 20
140 inelcm 3674 . . . . . . . . . . . . . . . . . . . 20
141139, 140sylan2br 463 . . . . . . . . . . . . . . . . . . 19
142141necon2bi 2644 . . . . . . . . . . . . . . . . . 18
143138, 142ax-mp 8 . . . . . . . . . . . . . . . . 17
144143rgenw 2765 . . . . . . . . . . . . . . . 16
145 rabeq0 3641 . . . . . . . . . . . . . . . 16
146144, 145mpbir 201 . . . . . . . . . . . . . . 15
147137, 146eqtri 2455 . . . . . . . . . . . . . 14
148 hashun 11648 . . . . . . . . . . . . . 14
149133, 136, 147, 148mp3an 1279 . . . . . . . . . . . . 13
150126, 149syl6eq 2483 . . . . . . . . . . . 12
151 nncn 10000 . . . . . . . . . . . . . . . 16
152151ad2antlr 708 . . . . . . . . . . . . . . 15
153 ax-1cn 9040 . . . . . . . . . . . . . . . 16
154153a1i 11 . . . . . . . . . . . . . . 15
155152, 154, 154addsubd 9424 . . . . . . . . . . . . . 14
156155oveq1d 6088 . . . . . . . . . . . . 13
157 subcl 9297 . . . . . . . . . . . . . . 15
158152, 153, 157sylancl 644 . . . . . . . . . . . . . 14
159109ad2antrr 707 . . . . . . . . . . . . . . 15
160159nn0cnd 10268 . . . . . . . . . . . . . 14
161158, 154, 160adddird 9105 . . . . . . . . . . . . 13
162160mulid2d 9098 . . . . . . . . . . . . . . 15
163 exmidne 2604 . . . . . . . . . . . . . . . . . . . . . . . 24
164 orcom 377 . . . . . . . . . . . . . . . . . . . . . . . 24
165163, 164mpbi 200 . . . . . . . . . . . . . . . . . . . . . . 23
166165biantru 492 . . . . . . . . . . . . . . . . . . . . . 22
167 andi 838 . . . . . . . . . . . . . . . . . . . . . 22
168166, 167bitri 241 . . . . . . . . . . . . . . . . . . . . 21
169168a1i 11 . . . . . . . . . . . . . . . . . . . 20
170169rabbiia 2938 . . . . . . . . . . . . . . . . . . 19
171 unrab 3604 . . . . . . . . . . . . . . . . . . 19
172170, 171eqtr4i 2458 . . . . . . . . . . . . . . . . . 18
173172fveq2i 5723 . . . . . . . . . . . . . . . . 17
174 ssrab2 3420 . . . . . . . . . . . . . . . . . . 19
175 ssfi 7321 . . . . . . . . . . . . . . . . . . 19
176130, 174, 175mp2an 654 . . . . . . . . . . . . . . . . . 18
177 ssrab2 3420 . . . . . . . . . . . . . . . . . . 19
178 ssfi 7321 . . . . . . . . . . . . . . . . . . 19
179130, 177, 178mp2an 654 . . . . . . . . . . . . . . . . . 18
180 inrab 3605 . . . . . . . . . . . . . . . . . . 19
181 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
182181necon3ai 2638 . . . . . . . . . . . . . . . . . . . . . . 23
183182adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
184 imnan 412 . . . . . . . . . . . . . . . . . . . . . 22
185183, 184mpbi 200 . . . . . . . . . . . . . . . . . . . . 21
186185rgenw 2765 . . . . . . . . . . . . . . . . . . . 20
187 rabeq0 3641 . . . . . . . . . . . . . . . . . . . 20
188186, 187mpbir 201 . . . . . . . . . . . . . . . . . . 19
189180, 188eqtri 2455 . . . . . . . . . . . . . . . . . 18
190 hashun 11648 . . . . . . . . . . . . . . . . . 18
191176, 179, 189, 190mp3an 1279 . . . . . . . . . . . . . . . . 17
192173, 191eqtri 2455 . . . . . . . . . . . . . . . 16
193 simpll 731 . . . . . . . . . . . . . . . . . 18
194 nnne0 10024 . . . . . . . . . . . . . . . . . . . . . 22
195 0p1e1 10085 . . . . . . . . . . . . . . . . . . . . . . . . 25
196195eqeq2i 2445 . . . . . . . . . . . . . . . . . . . . . . . 24
197 0cn 9076 . . . . . . . . . . . . . . . . . . . . . . . . . 26
198 addcan2 9243 . . . . . . . . . . . . . . . . . . . . . . . . . 26
199197, 153, 198mp3an23 1271 . . . . . . . . . . . . . . . . . . . . . . . . 25
200151, 199syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
201196, 200syl5bbr 251 . . . . . . . . . . . . . . . . . . . . . . 23
202201necon3bbid 2632 . . . . . . . . . . . . . . . . . . . . . 22
203194, 202mpbird 224 . . . . . . . . . . . . . . . . . . . . 21
204203ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20
20514adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
206 elfzp12 11118 . . . . . . . . . . . . . . . . . . . . . . 23
207205, 206syl 16 . . . . . . . . . . . . . . . . . . . . . 22
208207biimpa 471 . . . . . . . . . . . . . . . . . . . . 21
209208ord 367 . . . . . . . . . . . . . . . . . . . 20
210204, 209mpd 15 . . . . . . . . . . . . . . . . . . 19
211 df-2 10050 . . . . . . . . . . . . . . . . . . . 20
212211oveq1i 6083 . . . . . . . . . . . . . . . . . . 19
213210, 212syl6eleqr 2526 . . . . . . . . . . . . . . . . . 18
214 ovex 6098 . . . . . . . . . . . . . . . . . 18
215 eqid 2435 . . . . . . . . . . . . . . . . . 18
216 fveq1 5719 . . . . . . . . . . . . . . . . . . . . 21
217216eqeq1d 2443 . . . . . . . . . . . . . . . . . . . 20
218 fveq1 5719 . . . . . . . . . . . . . . . . . . . . 21
219218neeq1d 2611 . . . . . . . . . . . . . . . . . . . 20
220217, 219anbi12d 692 . . . . . . . . . . . . . . . . . . 19
221220cbvrabv 2947 . . . . . . . . . . . . . . . . . 18
222 eqid 2435 . . . . . . . . . . . . . . . . . 18
223 f1oeq1 5657 . . . . . . . . . . . . . . . . . . . 20
224 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . 23
225 id 20 . . . . . . . . . . . . . . . . . . . . . . 23
226224, 225neeq12d 2613 . . . . . . . . . . . . . . . . . . . . . 22
227226cbvralv 2924 . . . . . . . . . . . . . . . . . . . . 21
228 fveq1 5719 . . . . . . . . . . . . . . . . . . . . . . 23
229228neeq1d 2611 . . . . . . . . . . . . . . . . . . . . . 22
230229ralbidv 2717 . . . . . . . . . . . . . . . . . . . . 21
231227, 230syl5bb 249 . . . . . . . . . . . . . . . . . . . 20
232223, 231anbi12d 692 . . . . . . . . . . . . . . . . . . 19
233232cbvabv 2554 . . . . . . . . . . . . . . . . . 18
2343, 4, 10, 193, 213, 214, 215, 221, 222, 233subfacp1lem5 24862 . . . . . . . . . . . . . . . . 17
235218eqeq1d 2443 . . . . . . . . . . . . . . . . . . . 20
236217, 235anbi12d 692 . . . . . . . . . . . . . . . . . . 19
237236cbvrabv 2947 . . . . . . . . . . . . . . . . . 18
238 f1oeq1 5657 . . . . . . . . . . . . . . . . . . . 20
239226cbvralv 2924 . . . . . . . . . . . . . . . . . . . . 21
240229ralbidv 2717 . . . . . . . . . . . . . . . . . . . . 21
241239, 240syl5bb 249 . . . . . . . . . . . . . . . . . . . 20
242238, 241anbi12d 692 . . . . . . . . . . . . . . . . . . 19
243242cbvabv 2554 . . . . . . . . . . . . . . . . . 18
2443, 4, 10, 193, 213, 214, 215, 237, 243subfacp1lem3 24860 . . . . . . . . . . . . . . . . 17
245234, 244oveq12d 6091 . . . . . . . . . . . . . . . 16
246192, 245syl5eq 2479 . . . . . . . . . . . . . . 15
247162, 246eqtr4d 2470 . . . . . . . . . . . . . 14
248247oveq2d 6089 . . . . . . . . . . . . 13
249156, 161, 2483eqtrd 2471 . . . . . . . . . . . 12
250150, 249eqeq12d 2449 . . . . . . . . . . 11
251120, 250syl5ibr 213 . . . . . . . . . 10
252251ex 424 . . . . . . . . 9
253252a2d 24 . . . . . . . 8
254119, 253syld 42 . . . . . . 7
255254expcom 425 . . . . . 6
256255a2d 24 . . . . 5
25753, 63, 73, 83, 113, 256nnind 10010 . . . 4
2581, 257mpcom 34 . . 3
25934, 258mpd 15 . 2
260 nncn 10000 . . . 4
261 pncan 9303 . . . 4
262260, 153, 261sylancl 644 . . 3
263262oveq1d 6088 . 2
26432, 259, 2633eqtrd 2471 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1652   wcel 1725  cab 2421   wne 2598  wral 2697  crab 2701   cdif 3309   cun 3310   cin 3311   wss 3312  c0 3620  csn 3806  cpr 3807  cop 3809   cmpt 4258   cid 4485   cres 4872  wf 5442  wf1o 5445  cfv 5446  (class class class)co 6073  cfn 7101  cc 8980  cc0 8982  c1 8983   caddc 8985   cmul 8987   cmin 9283  cn 9992  c2 10041  cn0 10213  cz 10274  cuz 10480  cfz 11035  chash 11610 This theorem is referenced by:  subfacp1  24864 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-card 7818  df-cda 8040  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-nn 9993  df-2 10050  df-n0 10214  df-z 10275  df-uz 10481  df-fz 11036  df-hash 11611
 Copyright terms: Public domain W3C validator