Metamath Proof Explorer


Theorem birthdaylem2

Description: For general N and K , count the fraction of injective functions from 1 ... K to 1 ... N . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses birthday.s S = f | f : 1 K 1 N
birthday.t T = f | f : 1 K 1-1 1 N
Assertion birthdaylem2 N K 0 N T S = e k = 0 K 1 log 1 k N

Proof

Step Hyp Ref Expression
1 birthday.s S = f | f : 1 K 1 N
2 birthday.t T = f | f : 1 K 1-1 1 N
3 2 fveq2i T = f | f : 1 K 1-1 1 N
4 fzfi 1 K Fin
5 fzfi 1 N Fin
6 hashf1 1 K Fin 1 N Fin f | f : 1 K 1-1 1 N = 1 K ! ( 1 N 1 K)
7 4 5 6 mp2an f | f : 1 K 1-1 1 N = 1 K ! ( 1 N 1 K)
8 3 7 eqtri T = 1 K ! ( 1 N 1 K)
9 elfznn0 K 0 N K 0
10 9 adantl N K 0 N K 0
11 hashfz1 K 0 1 K = K
12 10 11 syl N K 0 N 1 K = K
13 12 fveq2d N K 0 N 1 K ! = K !
14 nnnn0 N N 0
15 hashfz1 N 0 1 N = N
16 14 15 syl N 1 N = N
17 16 adantr N K 0 N 1 N = N
18 17 12 oveq12d N K 0 N ( 1 N 1 K) = ( N K)
19 13 18 oveq12d N K 0 N 1 K ! ( 1 N 1 K) = K ! ( N K)
20 8 19 syl5eq N K 0 N T = K ! ( N K)
21 14 adantr N K 0 N N 0
22 21 faccld N K 0 N N !
23 22 nncnd N K 0 N N !
24 fznn0sub K 0 N N K 0
25 24 adantl N K 0 N N K 0
26 25 faccld N K 0 N N K !
27 26 nncnd N K 0 N N K !
28 26 nnne0d N K 0 N N K ! 0
29 23 27 28 divcld N K 0 N N ! N K !
30 10 faccld N K 0 N K !
31 30 nncnd N K 0 N K !
32 30 nnne0d N K 0 N K ! 0
33 29 31 32 divcan2d N K 0 N K ! N ! N K ! K ! = N ! N K !
34 bcval2 K 0 N ( N K) = N ! N K ! K !
35 34 adantl N K 0 N ( N K) = N ! N K ! K !
36 23 27 31 28 32 divdiv1d N K 0 N N ! N K ! K ! = N ! N K ! K !
37 35 36 eqtr4d N K 0 N ( N K) = N ! N K ! K !
38 37 oveq2d N K 0 N K ! ( N K) = K ! N ! N K ! K !
39 fzfid N K 0 N 1 N Fin
40 elfznn n 1 N n
41 40 adantl N K 0 N n 1 N n
42 nnrp n n +
43 42 relogcld n log n
44 43 recnd n log n
45 41 44 syl N K 0 N n 1 N log n
46 39 45 fsumcl N K 0 N n = 1 N log n
47 fzfid N K 0 N 1 N K Fin
48 elfznn n 1 N K n
49 48 adantl N K 0 N n 1 N K n
50 49 44 syl N K 0 N n 1 N K log n
51 47 50 fsumcl N K 0 N n = 1 N K log n
52 efsub n = 1 N log n n = 1 N K log n e n = 1 N log n n = 1 N K log n = e n = 1 N log n e n = 1 N K log n
53 46 51 52 syl2anc N K 0 N e n = 1 N log n n = 1 N K log n = e n = 1 N log n e n = 1 N K log n
54 25 nn0red N K 0 N N K
55 54 ltp1d N K 0 N N K < N - K + 1
56 fzdisj N K < N - K + 1 1 N K N - K + 1 N =
57 55 56 syl N K 0 N 1 N K N - K + 1 N =
58 fznn0sub2 K 0 N N K 0 N
59 58 adantl N K 0 N N K 0 N
60 elfzle2 N K 0 N N K N
61 59 60 syl N K 0 N N K N
62 61 adantr N K 0 N N K N K N
63 simpr N K 0 N N K N K
64 nnuz = 1
65 63 64 eleqtrdi N K 0 N N K N K 1
66 nnz N N
67 66 ad2antrr N K 0 N N K N
68 elfz5 N K 1 N N K 1 N N K N
69 65 67 68 syl2anc N K 0 N N K N K 1 N N K N
70 62 69 mpbird N K 0 N N K N K 1 N
71 fzsplit N K 1 N 1 N = 1 N K N - K + 1 N
72 70 71 syl N K 0 N N K 1 N = 1 N K N - K + 1 N
73 simpr N K 0 N N K = 0 N K = 0
74 73 oveq2d N K 0 N N K = 0 1 N K = 1 0
75 fz10 1 0 =
76 74 75 eqtrdi N K 0 N N K = 0 1 N K =
77 76 uneq1d N K 0 N N K = 0 1 N K N - K + 1 N = N - K + 1 N
78 uncom N - K + 1 N = N - K + 1 N
79 un0 N - K + 1 N = N - K + 1 N
80 78 79 eqtri N - K + 1 N = N - K + 1 N
81 73 oveq1d N K 0 N N K = 0 N - K + 1 = 0 + 1
82 1e0p1 1 = 0 + 1
83 81 82 eqtr4di N K 0 N N K = 0 N - K + 1 = 1
84 83 oveq1d N K 0 N N K = 0 N - K + 1 N = 1 N
85 80 84 syl5eq N K 0 N N K = 0 N - K + 1 N = 1 N
86 77 85 eqtr2d N K 0 N N K = 0 1 N = 1 N K N - K + 1 N
87 elnn0 N K 0 N K N K = 0
88 25 87 sylib N K 0 N N K N K = 0
89 72 86 88 mpjaodan N K 0 N 1 N = 1 N K N - K + 1 N
90 57 89 39 45 fsumsplit N K 0 N n = 1 N log n = n = 1 N K log n + n = N - K + 1 N log n
91 90 oveq1d N K 0 N n = 1 N log n n = 1 N K log n = n = 1 N K log n + n = N - K + 1 N log n - n = 1 N K log n
92 fzfid N K 0 N N - K + 1 N Fin
93 nn0p1nn N K 0 N - K + 1
94 25 93 syl N K 0 N N - K + 1
95 elfzuz n N - K + 1 N n N - K + 1
96 eluznn N - K + 1 n N - K + 1 n
97 94 95 96 syl2an N K 0 N n N - K + 1 N n
98 97 44 syl N K 0 N n N - K + 1 N log n
99 92 98 fsumcl N K 0 N n = N - K + 1 N log n
100 51 99 pncan2d N K 0 N n = 1 N K log n + n = N - K + 1 N log n - n = 1 N K log n = n = N - K + 1 N log n
101 91 100 eqtr2d N K 0 N n = N - K + 1 N log n = n = 1 N log n n = 1 N K log n
102 101 fveq2d N K 0 N e n = N - K + 1 N log n = e n = 1 N log n n = 1 N K log n
103 22 nnne0d N K 0 N N ! 0
104 eflog N ! N ! 0 e log N ! = N !
105 23 103 104 syl2anc N K 0 N e log N ! = N !
106 logfac N 0 log N ! = n = 1 N log n
107 21 106 syl N K 0 N log N ! = n = 1 N log n
108 107 fveq2d N K 0 N e log N ! = e n = 1 N log n
109 105 108 eqtr3d N K 0 N N ! = e n = 1 N log n
110 eflog N K ! N K ! 0 e log N K ! = N K !
111 27 28 110 syl2anc N K 0 N e log N K ! = N K !
112 logfac N K 0 log N K ! = n = 1 N K log n
113 25 112 syl N K 0 N log N K ! = n = 1 N K log n
114 113 fveq2d N K 0 N e log N K ! = e n = 1 N K log n
115 111 114 eqtr3d N K 0 N N K ! = e n = 1 N K log n
116 109 115 oveq12d N K 0 N N ! N K ! = e n = 1 N log n e n = 1 N K log n
117 53 102 116 3eqtr4d N K 0 N e n = N - K + 1 N log n = N ! N K !
118 33 38 117 3eqtr4d N K 0 N K ! ( N K) = e n = N - K + 1 N log n
119 20 118 eqtrd N K 0 N T = e n = N - K + 1 N log n
120 mapvalg 1 N Fin 1 K Fin 1 N 1 K = f | f : 1 K 1 N
121 5 4 120 mp2an 1 N 1 K = f | f : 1 K 1 N
122 1 121 eqtr4i S = 1 N 1 K
123 122 fveq2i S = 1 N 1 K
124 hashmap 1 N Fin 1 K Fin 1 N 1 K = 1 N 1 K
125 5 4 124 mp2an 1 N 1 K = 1 N 1 K
126 123 125 eqtri S = 1 N 1 K
127 17 12 oveq12d N K 0 N 1 N 1 K = N K
128 126 127 syl5eq N K 0 N S = N K
129 nncn N N
130 129 adantr N K 0 N N
131 nnne0 N N 0
132 131 adantr N K 0 N N 0
133 elfzelz K 0 N K
134 133 adantl N K 0 N K
135 explog N N 0 K N K = e K log N
136 130 132 134 135 syl3anc N K 0 N N K = e K log N
137 128 136 eqtrd N K 0 N S = e K log N
138 119 137 oveq12d N K 0 N T S = e n = N - K + 1 N log n e K log N
139 10 nn0cnd N K 0 N K
140 nnrp N N +
141 140 adantr N K 0 N N +
142 141 relogcld N K 0 N log N
143 142 recnd N K 0 N log N
144 139 143 mulcld N K 0 N K log N
145 efsub n = N - K + 1 N log n K log N e n = N - K + 1 N log n K log N = e n = N - K + 1 N log n e K log N
146 99 144 145 syl2anc N K 0 N e n = N - K + 1 N log n K log N = e n = N - K + 1 N log n e K log N
147 relogdiv n + N + log n N = log n log N
148 42 141 147 syl2anr N K 0 N n log n N = log n log N
149 97 148 syldan N K 0 N n N - K + 1 N log n N = log n log N
150 149 sumeq2dv N K 0 N n = N - K + 1 N log n N = n = N - K + 1 N log n log N
151 66 adantr N K 0 N N
152 25 nn0zd N K 0 N N K
153 152 peano2zd N K 0 N N - K + 1
154 97 nnrpd N K 0 N n N - K + 1 N n +
155 141 adantr N K 0 N n N - K + 1 N N +
156 154 155 rpdivcld N K 0 N n N - K + 1 N n N +
157 156 relogcld N K 0 N n N - K + 1 N log n N
158 157 recnd N K 0 N n N - K + 1 N log n N
159 fvoveq1 n = N k log n N = log N k N
160 151 153 151 158 159 fsumrev N K 0 N n = N - K + 1 N log n N = k = N N N N - K + 1 log N k N
161 130 subidd N K 0 N N N = 0
162 1cnd N K 0 N 1
163 130 139 162 subsubd N K 0 N N K 1 = N - K + 1
164 163 oveq2d N K 0 N N N K 1 = N N - K + 1
165 ax-1cn 1
166 subcl K 1 K 1
167 139 165 166 sylancl N K 0 N K 1
168 130 167 nncand N K 0 N N N K 1 = K 1
169 164 168 eqtr3d N K 0 N N N - K + 1 = K 1
170 161 169 oveq12d N K 0 N N N N N - K + 1 = 0 K 1
171 130 adantr N K 0 N k 0 K 1 N
172 elfznn0 k 0 K 1 k 0
173 172 adantl N K 0 N k 0 K 1 k 0
174 173 nn0cnd N K 0 N k 0 K 1 k
175 132 adantr N K 0 N k 0 K 1 N 0
176 171 174 171 175 divsubdird N K 0 N k 0 K 1 N k N = N N k N
177 171 175 dividd N K 0 N k 0 K 1 N N = 1
178 177 oveq1d N K 0 N k 0 K 1 N N k N = 1 k N
179 176 178 eqtrd N K 0 N k 0 K 1 N k N = 1 k N
180 179 fveq2d N K 0 N k 0 K 1 log N k N = log 1 k N
181 170 180 sumeq12rdv N K 0 N k = N N N N - K + 1 log N k N = k = 0 K 1 log 1 k N
182 160 181 eqtrd N K 0 N n = N - K + 1 N log n N = k = 0 K 1 log 1 k N
183 143 adantr N K 0 N n N - K + 1 N log N
184 92 98 183 fsumsub N K 0 N n = N - K + 1 N log n log N = n = N - K + 1 N log n n = N - K + 1 N log N
185 fsumconst N - K + 1 N Fin log N n = N - K + 1 N log N = N - K + 1 N log N
186 92 143 185 syl2anc N K 0 N n = N - K + 1 N log N = N - K + 1 N log N
187 1zzd N K 0 N 1
188 fzen 1 K N K 1 K 1 + N - K K + N - K
189 187 134 152 188 syl3anc N K 0 N 1 K 1 + N - K K + N - K
190 25 nn0cnd N K 0 N N K
191 addcom 1 N K 1 + N - K = N - K + 1
192 165 190 191 sylancr N K 0 N 1 + N - K = N - K + 1
193 139 130 pncan3d N K 0 N K + N - K = N
194 192 193 oveq12d N K 0 N 1 + N - K K + N - K = N - K + 1 N
195 189 194 breqtrd N K 0 N 1 K N - K + 1 N
196 hasheni 1 K N - K + 1 N 1 K = N - K + 1 N
197 195 196 syl N K 0 N 1 K = N - K + 1 N
198 197 12 eqtr3d N K 0 N N - K + 1 N = K
199 198 oveq1d N K 0 N N - K + 1 N log N = K log N
200 186 199 eqtrd N K 0 N n = N - K + 1 N log N = K log N
201 200 oveq2d N K 0 N n = N - K + 1 N log n n = N - K + 1 N log N = n = N - K + 1 N log n K log N
202 184 201 eqtrd N K 0 N n = N - K + 1 N log n log N = n = N - K + 1 N log n K log N
203 150 182 202 3eqtr3rd N K 0 N n = N - K + 1 N log n K log N = k = 0 K 1 log 1 k N
204 203 fveq2d N K 0 N e n = N - K + 1 N log n K log N = e k = 0 K 1 log 1 k N
205 138 146 204 3eqtr2d N K 0 N T S = e k = 0 K 1 log 1 k N