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 ⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
birthday.t ⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
Assertion birthdaylem2 ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) = ( exp ‘ Σ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( log ‘ ( 1 − ( 𝑘 / 𝑁 ) ) ) ) )

Proof

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