Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  birthdaylem2 Structured version   Unicode version

Theorem birthdaylem2 23813
 Description: For general and , count the fraction of injective functions from to . (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
birthday.s
birthday.t
Assertion
Ref Expression
birthdaylem2
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem birthdaylem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 birthday.t . . . . . . 7
21fveq2i 5821 . . . . . 6
3 fzfi 12128 . . . . . . 7
4 fzfi 12128 . . . . . . 7
5 hashf1 12561 . . . . . . 7
63, 4, 5mp2an 676 . . . . . 6
72, 6eqtri 2444 . . . . 5
8 elfznn0 11831 . . . . . . . . 9
98adantl 467 . . . . . . . 8
10 hashfz1 12472 . . . . . . . 8
119, 10syl 17 . . . . . . 7
1211fveq2d 5822 . . . . . 6
13 nnnn0 10820 . . . . . . . . 9
14 hashfz1 12472 . . . . . . . . 9
1513, 14syl 17 . . . . . . . 8
1615adantr 466 . . . . . . 7
1716, 11oveq12d 6260 . . . . . 6
1812, 17oveq12d 6260 . . . . 5
197, 18syl5eq 2468 . . . 4
2013adantr 466 . . . . . . . . 9
21 faccl 12412 . . . . . . . . 9
2220, 21syl 17 . . . . . . . 8
2322nncnd 10569 . . . . . . 7
24 fznn0sub 11775 . . . . . . . . . 10
2524adantl 467 . . . . . . . . 9
26 faccl 12412 . . . . . . . . 9
2725, 26syl 17 . . . . . . . 8
2827nncnd 10569 . . . . . . 7
2927nnne0d 10598 . . . . . . 7
3023, 28, 29divcld 10327 . . . . . 6
31 faccl 12412 . . . . . . . 8
329, 31syl 17 . . . . . . 7
3332nncnd 10569 . . . . . 6
3432nnne0d 10598 . . . . . 6
3530, 33, 34divcan2d 10329 . . . . 5
36 bcval2 12433 . . . . . . . 8
3736adantl 467 . . . . . . 7
3823, 28, 33, 29, 34divdiv1d 10358 . . . . . . 7
3937, 38eqtr4d 2459 . . . . . 6
4039oveq2d 6258 . . . . 5
41 fzfid 12129 . . . . . . . 8
42 elfznn 11772 . . . . . . . . . 10
4342adantl 467 . . . . . . . . 9
44 nnrp 11255 . . . . . . . . . . 11
4544relogcld 23507 . . . . . . . . . 10
4645recnd 9613 . . . . . . . . 9
4743, 46syl 17 . . . . . . . 8
4841, 47fsumcl 13735 . . . . . . 7
49 fzfid 12129 . . . . . . . 8
50 elfznn 11772 . . . . . . . . . 10
5150adantl 467 . . . . . . . . 9
5251, 46syl 17 . . . . . . . 8
5349, 52fsumcl 13735 . . . . . . 7
54 efsub 14090 . . . . . . 7
5548, 53, 54syl2anc 665 . . . . . 6
5625nn0red 10870 . . . . . . . . . . . 12
5756ltp1d 10481 . . . . . . . . . . 11
58 fzdisj 11770 . . . . . . . . . . 11
5957, 58syl 17 . . . . . . . . . 10
60 fznn0sub2 11841 . . . . . . . . . . . . . . . 16
6160adantl 467 . . . . . . . . . . . . . . 15
62 elfzle2 11747 . . . . . . . . . . . . . . 15
6361, 62syl 17 . . . . . . . . . . . . . 14
6463adantr 466 . . . . . . . . . . . . 13
65 simpr 462 . . . . . . . . . . . . . . 15
66 nnuz 11138 . . . . . . . . . . . . . . 15
6765, 66syl6eleq 2510 . . . . . . . . . . . . . 14
68 nnz 10903 . . . . . . . . . . . . . . 15
6968ad2antrr 730 . . . . . . . . . . . . . 14
70 elfz5 11736 . . . . . . . . . . . . . 14
7167, 69, 70syl2anc 665 . . . . . . . . . . . . 13
7264, 71mpbird 235 . . . . . . . . . . . 12
73 fzsplit 11769 . . . . . . . . . . . 12
7472, 73syl 17 . . . . . . . . . . 11
75 simpr 462 . . . . . . . . . . . . . . 15
7675oveq2d 6258 . . . . . . . . . . . . . 14
77 fz10 11764 . . . . . . . . . . . . . 14
7876, 77syl6eq 2472 . . . . . . . . . . . . 13
7978uneq1d 3555 . . . . . . . . . . . 12
80 uncom 3546 . . . . . . . . . . . . . 14
81 un0 3725 . . . . . . . . . . . . . 14
8280, 81eqtri 2444 . . . . . . . . . . . . 13
8375oveq1d 6257 . . . . . . . . . . . . . . 15
84 1e0p1 11023 . . . . . . . . . . . . . . 15
8583, 84syl6eqr 2474 . . . . . . . . . . . . . 14
8685oveq1d 6257 . . . . . . . . . . . . 13
8782, 86syl5eq 2468 . . . . . . . . . . . 12
8879, 87eqtr2d 2457 . . . . . . . . . . 11
89 elnn0 10815 . . . . . . . . . . . 12
9025, 89sylib 199 . . . . . . . . . . 11
9174, 88, 90mpjaodan 793 . . . . . . . . . 10
9259, 91, 41, 47fsumsplit 13742 . . . . . . . . 9
9392oveq1d 6257 . . . . . . . 8
94 fzfid 12129 . . . . . . . . . 10
95 nn0p1nn 10853 . . . . . . . . . . . . 13
9625, 95syl 17 . . . . . . . . . . . 12
97 elfzuz 11740 . . . . . . . . . . . 12
98 eluznn 11173 . . . . . . . . . . . 12
9996, 97, 98syl2an 479 . . . . . . . . . . 11
10099, 46syl 17 . . . . . . . . . 10
10194, 100fsumcl 13735 . . . . . . . . 9
10253, 101pncan2d 9932 . . . . . . . 8
10393, 102eqtr2d 2457 . . . . . . 7
104103fveq2d 5822 . . . . . 6
10522nnne0d 10598 . . . . . . . . 9
106 eflog 23461 . . . . . . . . 9
10723, 105, 106syl2anc 665 . . . . . . . 8
108 logfac 23485 . . . . . . . . . 10
10920, 108syl 17 . . . . . . . . 9
110109fveq2d 5822 . . . . . . . 8
111107, 110eqtr3d 2458 . . . . . . 7
112 eflog 23461 . . . . . . . . 9
11328, 29, 112syl2anc 665 . . . . . . . 8
114 logfac 23485 . . . . . . . . . 10
11525, 114syl 17 . . . . . . . . 9
116115fveq2d 5822 . . . . . . . 8
117113, 116eqtr3d 2458 . . . . . . 7
118111, 117oveq12d 6260 . . . . . 6
11955, 104, 1183eqtr4d 2466 . . . . 5
12035, 40, 1193eqtr4d 2466 . . . 4
12119, 120eqtrd 2456 . . 3
122 birthday.s . . . . . . . 8
123 mapvalg 7430 . . . . . . . . 9
1244, 3, 123mp2an 676 . . . . . . . 8
125122, 124eqtr4i 2447 . . . . . . 7
126125fveq2i 5821 . . . . . 6
127 hashmap 12548 . . . . . . 7
1284, 3, 127mp2an 676 . . . . . 6
129126, 128eqtri 2444 . . . . 5
13016, 11oveq12d 6260 . . . . 5
131129, 130syl5eq 2468 . . . 4
132 nncn 10561 . . . . . 6
133132adantr 466 . . . . 5
134 nnne0 10586 . . . . . 6
135134adantr 466 . . . . 5
136 elfzelz 11744 . . . . . 6
137136adantl 467 . . . . 5
138 explog 23478 . . . . 5
139133, 135, 137, 138syl3anc 1264 . . . 4
140131, 139eqtrd 2456 . . 3
141121, 140oveq12d 6260 . 2
1429nn0cnd 10871 . . . 4
143 nnrp 11255 . . . . . . 7
144143adantr 466 . . . . . 6
145144relogcld 23507 . . . . 5
146145recnd 9613 . . . 4
147142, 146mulcld 9607 . . 3
148 efsub 14090 . . 3
149101, 147, 148syl2anc 665 . 2
150 relogdiv 23477 . . . . . . 7
15144, 144, 150syl2anr 480 . . . . . 6
15299, 151syldan 472 . . . . 5
153152sumeq2dv 13705 . . . 4
15468adantr 466 . . . . . 6
15525nn0zd 10982 . . . . . . 7
156155peano2zd 10987 . . . . . 6
15799, 44syl 17 . . . . . . . . 9
158144adantr 466 . . . . . . . . 9
159157, 158rpdivcld 11302 . . . . . . . 8
160159relogcld 23507 . . . . . . 7
161160recnd 9613 . . . . . 6
162 oveq1 6249 . . . . . . 7
163162fveq2d 5822 . . . . . 6
164154, 156, 154, 161, 163fsumrev 13776 . . . . 5
165133subidd 9918 . . . . . . 7
166 1cnd 9603 . . . . . . . . . 10
167133, 142, 166subsubd 9958 . . . . . . . . 9
168167oveq2d 6258 . . . . . . . 8
169 ax-1cn 9541 . . . . . . . . . 10
170 subcl 9818 . . . . . . . . . 10
171142, 169, 170sylancl 666 . . . . . . . . 9
172133, 171nncand 9935 . . . . . . . 8
173168, 172eqtr3d 2458 . . . . . . 7
174165, 173oveq12d 6260 . . . . . 6
175133adantr 466 . . . . . . . . 9
176 elfznn0 11831 . . . . . . . . . . 11
177176adantl 467 . . . . . . . . . 10
178177nn0cnd 10871 . . . . . . . . 9
179135adantr 466 . . . . . . . . 9
180175, 178, 175, 179divsubdird 10366 . . . . . . . 8
181175, 179dividd 10325 . . . . . . . . 9
182181oveq1d 6257 . . . . . . . 8
183180, 182eqtrd 2456 . . . . . . 7
184183fveq2d 5822 . . . . . 6
185174, 184sumeq12rdv 13709 . . . . 5
186164, 185eqtrd 2456 . . . 4
187146adantr 466 . . . . . 6
18894, 100, 187fsumsub 13785 . . . . 5
189 fsumconst 13787 . . . . . . . 8
19094, 146, 189syl2anc 665 . . . . . . 7
191 1zzd 10912 . . . . . . . . . . . 12
192 fzen 11760 . . . . . . . . . . . 12
193191, 137, 155, 192syl3anc 1264 . . . . . . . . . . 11
19425nn0cnd 10871 . . . . . . . . . . . . 13
195 addcom 9763 . . . . . . . . . . . . 13
196169, 194, 195sylancr 667 . . . . . . . . . . . 12
197142, 133pncan3d 9933 . . . . . . . . . . . 12
198196, 197oveq12d 6260 . . . . . . . . . . 11
199193, 198breqtrd 4384 . . . . . . . . . 10
200 hasheni 12474 . . . . . . . . . 10
201199, 200syl 17 . . . . . . . . 9
202201, 11eqtr3d 2458 . . . . . . . 8
203202oveq1d 6257 . . . . . . 7
204190, 203eqtrd 2456 . . . . . 6
205204oveq2d 6258 . . . . 5
206188, 205eqtrd 2456 . . . 4
207153, 186, 2063eqtr3rd 2465 . . 3
208207fveq2d 5822 . 2
209141, 149, 2083eqtr2d 2462 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wo 369   wa 370   wceq 1437   wcel 1872  cab 2408   wne 2593   cun 3370   cin 3371  c0 3697   class class class wbr 4359  wf 5533  wf1 5534  cfv 5537  (class class class)co 6242   cmap 7420   cen 7514  cfn 7517  cc 9481  cc0 9483  c1 9484   caddc 9486   cmul 9488   clt 9619   cle 9620   cmin 9804   cdiv 10213  cn 10553  cn0 10813  cz 10881  cuz 11103  crp 11246  cfz 11728  cexp 12215  cfa 12402   cbc 12430  chash 12458  csu 13688  ce 14050  clog 23439 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-inf2 8092  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-pre-sup 9561  ax-addf 9562  ax-mulf 9563 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-iin 4238  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-se 4749  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-isom 5546  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-of 6482  df-om 6644  df-1st 6744  df-2nd 6745  df-supp 6863  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7830  df-fi 7871  df-sup 7902  df-inf 7903  df-oi 7971  df-card 8318  df-cda 8542  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-div 10214  df-nn 10554  df-2 10612  df-3 10613  df-4 10614  df-5 10615  df-6 10616  df-7 10617  df-8 10618  df-9 10619  df-10 10620  df-n0 10814  df-z 10882  df-dec 10996  df-uz 11104  df-q 11209  df-rp 11247  df-xneg 11353  df-xadd 11354  df-xmul 11355  df-ioo 11583  df-ioc 11584  df-ico 11585  df-icc 11586  df-fz 11729  df-fzo 11860  df-fl 11971  df-mod 12040  df-seq 12157  df-exp 12216  df-fac 12403  df-bc 12431  df-hash 12459  df-shft 13067  df-cj 13099  df-re 13100  df-im 13101  df-sqrt 13235  df-abs 13236  df-limsup 13462  df-clim 13488  df-rlim 13489  df-sum 13689  df-ef 14057  df-sin 14059  df-cos 14060  df-pi 14062  df-struct 15059  df-ndx 15060  df-slot 15061  df-base 15062  df-sets 15063  df-ress 15064  df-plusg 15139  df-mulr 15140  df-starv 15141  df-sca 15142  df-vsca 15143  df-ip 15144  df-tset 15145  df-ple 15146  df-ds 15148  df-unif 15149  df-hom 15150  df-cco 15151  df-rest 15257  df-topn 15258  df-0g 15276  df-gsum 15277  df-topgen 15278  df-pt 15279  df-prds 15282  df-xrs 15336  df-qtop 15342  df-imas 15343  df-xps 15346  df-mre 15428  df-mrc 15429  df-acs 15431  df-mgm 16424  df-sgrp 16463  df-mnd 16473  df-submnd 16519  df-mulg 16612  df-cntz 16907  df-cmn 17368  df-psmet 18898  df-xmet 18899  df-met 18900  df-bl 18901  df-mopn 18902  df-fbas 18903  df-fg 18904  df-cnfld 18907  df-top 19856  df-bases 19857  df-topon 19858  df-topsp 19859  df-cld 19969  df-ntr 19970  df-cls 19971  df-nei 20049  df-lp 20087  df-perf 20088  df-cn 20178  df-cnp 20179  df-haus 20266  df-tx 20512  df-hmeo 20705  df-fil 20796  df-fm 20888  df-flim 20889  df-flf 20890  df-xms 21270  df-ms 21271  df-tms 21272  df-cncf 21845  df-limc 22756  df-dv 22757  df-log 23441 This theorem is referenced by:  birthdaylem3  23814
 Copyright terms: Public domain W3C validator