# 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}=\left\{{f}|{f}:\left(1\dots {K}\right)⟶\left(1\dots {N}\right)\right\}$
birthday.t ${⊢}{T}=\left\{{f}|{f}:\left(1\dots {K}\right)\underset{1-1}{⟶}\left(1\dots {N}\right)\right\}$
Assertion birthdaylem2 ${⊢}\left({N}\in ℕ\wedge {K}\in \left(0\dots {N}\right)\right)\to \frac{\left|{T}\right|}{\left|{S}\right|}={\mathrm{e}}^{\sum _{{k}=0}^{{K}-1}\mathrm{log}\left(1-\left(\frac{{k}}{{N}}\right)\right)}$

### Proof

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