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