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

Theorem birthdaylem2 25835
Description: For general 𝑁 and 𝐾, count the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
birthday.s 𝑆 = {𝑓𝑓:(1...𝐾)⟶(1...𝑁)}
birthday.t 𝑇 = {𝑓𝑓:(1...𝐾)–1-1→(1...𝑁)}
Assertion
Ref Expression
birthdaylem2 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))
Distinct variable groups:   𝑓,𝑘,𝐾   𝑓,𝑁,𝑘
Allowed substitution hints:   𝑆(𝑓,𝑘)   𝑇(𝑓,𝑘)

Proof of Theorem birthdaylem2
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 birthday.t . . . . . . 7 𝑇 = {𝑓𝑓:(1...𝐾)–1-1→(1...𝑁)}
21fveq2i 6720 . . . . . 6 (♯‘𝑇) = (♯‘{𝑓𝑓:(1...𝐾)–1-1→(1...𝑁)})
3 fzfi 13545 . . . . . . 7 (1...𝐾) ∈ Fin
4 fzfi 13545 . . . . . . 7 (1...𝑁) ∈ Fin
5 hashf1 14023 . . . . . . 7 (((1...𝐾) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘{𝑓𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))))
63, 4, 5mp2an 692 . . . . . 6 (♯‘{𝑓𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾))))
72, 6eqtri 2765 . . . . 5 (♯‘𝑇) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾))))
8 elfznn0 13205 . . . . . . . . 9 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)
98adantl 485 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ0)
10 hashfz1 13912 . . . . . . . 8 (𝐾 ∈ ℕ0 → (♯‘(1...𝐾)) = 𝐾)
119, 10syl 17 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝐾)) = 𝐾)
1211fveq2d 6721 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(♯‘(1...𝐾))) = (!‘𝐾))
13 nnnn0 12097 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
14 hashfz1 13912 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
1513, 14syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (♯‘(1...𝑁)) = 𝑁)
1615adantr 484 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝑁)) = 𝑁)
1716, 11oveq12d 7231 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(1...𝑁))C(♯‘(1...𝐾))) = (𝑁C𝐾))
1812, 17oveq12d 7231 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))) = ((!‘𝐾) · (𝑁C𝐾)))
197, 18syl5eq 2790 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑇) = ((!‘𝐾) · (𝑁C𝐾)))
2013adantr 484 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
2120faccld 13850 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℕ)
2221nncnd 11846 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℂ)
23 fznn0sub 13144 . . . . . . . . . 10 (𝐾 ∈ (0...𝑁) → (𝑁𝐾) ∈ ℕ0)
2423adantl 485 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ ℕ0)
2524faccld 13850 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁𝐾)) ∈ ℕ)
2625nncnd 11846 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁𝐾)) ∈ ℂ)
2725nnne0d 11880 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁𝐾)) ≠ 0)
2822, 26, 27divcld 11608 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁𝐾))) ∈ ℂ)
299faccld 13850 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℕ)
3029nncnd 11846 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℂ)
3129nnne0d 11880 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ≠ 0)
3228, 30, 31divcan2d 11610 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁𝐾))) / (!‘𝐾))) = ((!‘𝑁) / (!‘(𝑁𝐾))))
33 bcval2 13871 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))))
3433adantl 485 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))))
3522, 26, 30, 27, 31divdiv1d 11639 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((!‘𝑁) / (!‘(𝑁𝐾))) / (!‘𝐾)) = ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))))
3634, 35eqtr4d 2780 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (((!‘𝑁) / (!‘(𝑁𝐾))) / (!‘𝐾)))
3736oveq2d 7229 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁𝐾))) / (!‘𝐾))))
38 fzfid 13546 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
39 elfznn 13141 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
4039adantl 485 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
41 nnrp 12597 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
4241relogcld 25511 . . . . . . . . . 10 (𝑛 ∈ ℕ → (log‘𝑛) ∈ ℝ)
4342recnd 10861 . . . . . . . . 9 (𝑛 ∈ ℕ → (log‘𝑛) ∈ ℂ)
4440, 43syl 17 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ∈ ℂ)
4538, 44fsumcl 15297 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) ∈ ℂ)
46 fzfid 13546 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...(𝑁𝐾)) ∈ Fin)
47 elfznn 13141 . . . . . . . . . 10 (𝑛 ∈ (1...(𝑁𝐾)) → 𝑛 ∈ ℕ)
4847adantl 485 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁𝐾))) → 𝑛 ∈ ℕ)
4948, 43syl 17 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁𝐾))) → (log‘𝑛) ∈ ℂ)
5046, 49fsumcl 15297 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛) ∈ ℂ)
51 efsub 15661 . . . . . . 7 ((Σ𝑛 ∈ (1...𝑁)(log‘𝑛) ∈ ℂ ∧ Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛) ∈ ℂ) → (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))))
5245, 50, 51syl2anc 587 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))))
5324nn0red 12151 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ ℝ)
5453ltp1d 11762 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) < ((𝑁𝐾) + 1))
55 fzdisj 13139 . . . . . . . . . . 11 ((𝑁𝐾) < ((𝑁𝐾) + 1) → ((1...(𝑁𝐾)) ∩ (((𝑁𝐾) + 1)...𝑁)) = ∅)
5654, 55syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1...(𝑁𝐾)) ∩ (((𝑁𝐾) + 1)...𝑁)) = ∅)
57 fznn0sub2 13219 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (0...𝑁) → (𝑁𝐾) ∈ (0...𝑁))
5857adantl 485 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ (0...𝑁))
59 elfzle2 13116 . . . . . . . . . . . . . . 15 ((𝑁𝐾) ∈ (0...𝑁) → (𝑁𝐾) ≤ 𝑁)
6058, 59syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ≤ 𝑁)
6160adantr 484 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → (𝑁𝐾) ≤ 𝑁)
62 simpr 488 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → (𝑁𝐾) ∈ ℕ)
63 nnuz 12477 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6462, 63eleqtrdi 2848 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → (𝑁𝐾) ∈ (ℤ‘1))
65 nnz 12199 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
6665ad2antrr 726 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → 𝑁 ∈ ℤ)
67 elfz5 13104 . . . . . . . . . . . . . 14 (((𝑁𝐾) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑁𝐾) ∈ (1...𝑁) ↔ (𝑁𝐾) ≤ 𝑁))
6864, 66, 67syl2anc 587 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → ((𝑁𝐾) ∈ (1...𝑁) ↔ (𝑁𝐾) ≤ 𝑁))
6961, 68mpbird 260 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → (𝑁𝐾) ∈ (1...𝑁))
70 fzsplit 13138 . . . . . . . . . . . 12 ((𝑁𝐾) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑁𝐾)) ∪ (((𝑁𝐾) + 1)...𝑁)))
7169, 70syl 17 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) ∈ ℕ) → (1...𝑁) = ((1...(𝑁𝐾)) ∪ (((𝑁𝐾) + 1)...𝑁)))
72 simpr 488 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (𝑁𝐾) = 0)
7372oveq2d 7229 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (1...(𝑁𝐾)) = (1...0))
74 fz10 13133 . . . . . . . . . . . . . 14 (1...0) = ∅
7573, 74eqtrdi 2794 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (1...(𝑁𝐾)) = ∅)
7675uneq1d 4076 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → ((1...(𝑁𝐾)) ∪ (((𝑁𝐾) + 1)...𝑁)) = (∅ ∪ (((𝑁𝐾) + 1)...𝑁)))
77 uncom 4067 . . . . . . . . . . . . . 14 (∅ ∪ (((𝑁𝐾) + 1)...𝑁)) = ((((𝑁𝐾) + 1)...𝑁) ∪ ∅)
78 un0 4305 . . . . . . . . . . . . . 14 ((((𝑁𝐾) + 1)...𝑁) ∪ ∅) = (((𝑁𝐾) + 1)...𝑁)
7977, 78eqtri 2765 . . . . . . . . . . . . 13 (∅ ∪ (((𝑁𝐾) + 1)...𝑁)) = (((𝑁𝐾) + 1)...𝑁)
8072oveq1d 7228 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → ((𝑁𝐾) + 1) = (0 + 1))
81 1e0p1 12335 . . . . . . . . . . . . . . 15 1 = (0 + 1)
8280, 81eqtr4di 2796 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → ((𝑁𝐾) + 1) = 1)
8382oveq1d 7228 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (((𝑁𝐾) + 1)...𝑁) = (1...𝑁))
8479, 83syl5eq 2790 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (∅ ∪ (((𝑁𝐾) + 1)...𝑁)) = (1...𝑁))
8576, 84eqtr2d 2778 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁𝐾) = 0) → (1...𝑁) = ((1...(𝑁𝐾)) ∪ (((𝑁𝐾) + 1)...𝑁)))
86 elnn0 12092 . . . . . . . . . . . 12 ((𝑁𝐾) ∈ ℕ0 ↔ ((𝑁𝐾) ∈ ℕ ∨ (𝑁𝐾) = 0))
8724, 86sylib 221 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁𝐾) ∈ ℕ ∨ (𝑁𝐾) = 0))
8871, 85, 87mpjaodan 959 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) = ((1...(𝑁𝐾)) ∪ (((𝑁𝐾) + 1)...𝑁)))
8956, 88, 38, 44fsumsplit 15305 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)))
9089oveq1d 7228 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)) = ((Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)))
91 fzfid 13546 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((𝑁𝐾) + 1)...𝑁) ∈ Fin)
92 nn0p1nn 12129 . . . . . . . . . . . . 13 ((𝑁𝐾) ∈ ℕ0 → ((𝑁𝐾) + 1) ∈ ℕ)
9324, 92syl 17 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁𝐾) + 1) ∈ ℕ)
94 elfzuz 13108 . . . . . . . . . . . 12 (𝑛 ∈ (((𝑁𝐾) + 1)...𝑁) → 𝑛 ∈ (ℤ‘((𝑁𝐾) + 1)))
95 eluznn 12514 . . . . . . . . . . . 12 ((((𝑁𝐾) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((𝑁𝐾) + 1))) → 𝑛 ∈ ℕ)
9693, 94, 95syl2an 599 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → 𝑛 ∈ ℕ)
9796, 43syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (log‘𝑛) ∈ ℂ)
9891, 97fsumcl 15297 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ)
9950, 98pncan2d 11191 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)) = Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛))
10090, 99eqtr2d 2778 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)))
101100fveq2d 6721 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) = (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))))
10221nnne0d 11880 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ≠ 0)
103 eflog 25465 . . . . . . . . 9 (((!‘𝑁) ∈ ℂ ∧ (!‘𝑁) ≠ 0) → (exp‘(log‘(!‘𝑁))) = (!‘𝑁))
10422, 102, 103syl2anc 587 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘𝑁))) = (!‘𝑁))
105 logfac 25489 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛))
10620, 105syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛))
107106fveq2d 6721 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘𝑁))) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)))
108104, 107eqtr3d 2779 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)))
109 eflog 25465 . . . . . . . . 9 (((!‘(𝑁𝐾)) ∈ ℂ ∧ (!‘(𝑁𝐾)) ≠ 0) → (exp‘(log‘(!‘(𝑁𝐾)))) = (!‘(𝑁𝐾)))
11026, 27, 109syl2anc 587 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘(𝑁𝐾)))) = (!‘(𝑁𝐾)))
111 logfac 25489 . . . . . . . . . 10 ((𝑁𝐾) ∈ ℕ0 → (log‘(!‘(𝑁𝐾))) = Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))
11224, 111syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘(𝑁𝐾))) = Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))
113112fveq2d 6721 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘(𝑁𝐾)))) = (exp‘Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)))
114110, 113eqtr3d 2779 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁𝐾)) = (exp‘Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛)))
115108, 114oveq12d 7231 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁𝐾))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁𝐾))(log‘𝑛))))
11652, 101, 1153eqtr4d 2787 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) = ((!‘𝑁) / (!‘(𝑁𝐾))))
11732, 37, 1163eqtr4d 2787 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = (exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)))
11819, 117eqtrd 2777 . . 3 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑇) = (exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)))
119 birthday.s . . . . . . . 8 𝑆 = {𝑓𝑓:(1...𝐾)⟶(1...𝑁)}
120 mapvalg 8518 . . . . . . . . 9 (((1...𝑁) ∈ Fin ∧ (1...𝐾) ∈ Fin) → ((1...𝑁) ↑m (1...𝐾)) = {𝑓𝑓:(1...𝐾)⟶(1...𝑁)})
1214, 3, 120mp2an 692 . . . . . . . 8 ((1...𝑁) ↑m (1...𝐾)) = {𝑓𝑓:(1...𝐾)⟶(1...𝑁)}
122119, 121eqtr4i 2768 . . . . . . 7 𝑆 = ((1...𝑁) ↑m (1...𝐾))
123122fveq2i 6720 . . . . . 6 (♯‘𝑆) = (♯‘((1...𝑁) ↑m (1...𝐾)))
124 hashmap 14002 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘((1...𝑁) ↑m (1...𝐾))) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾))))
1254, 3, 124mp2an 692 . . . . . 6 (♯‘((1...𝑁) ↑m (1...𝐾))) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾)))
126123, 125eqtri 2765 . . . . 5 (♯‘𝑆) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾)))
12716, 11oveq12d 7231 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(1...𝑁))↑(♯‘(1...𝐾))) = (𝑁𝐾))
128126, 127syl5eq 2790 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑆) = (𝑁𝐾))
129 nncn 11838 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
130129adantr 484 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℂ)
131 nnne0 11864 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
132131adantr 484 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ≠ 0)
133 elfzelz 13112 . . . . . 6 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
134133adantl 485 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
135 explog 25482 . . . . 5 ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ∧ 𝐾 ∈ ℤ) → (𝑁𝐾) = (exp‘(𝐾 · (log‘𝑁))))
136130, 132, 134, 135syl3anc 1373 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) = (exp‘(𝐾 · (log‘𝑁))))
137128, 136eqtrd 2777 . . 3 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑆) = (exp‘(𝐾 · (log‘𝑁))))
138118, 137oveq12d 7231 . 2 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = ((exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
1399nn0cnd 12152 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℂ)
140 nnrp 12597 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
141140adantr 484 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℝ+)
142141relogcld 25511 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℝ)
143142recnd 10861 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℂ)
144139, 143mulcld 10853 . . 3 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 · (log‘𝑁)) ∈ ℂ)
145 efsub 15661 . . 3 ((Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ ∧ (𝐾 · (log‘𝑁)) ∈ ℂ) → (exp‘(Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
14698, 144, 145syl2anc 587 . 2 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
147 relogdiv 25481 . . . . . . 7 ((𝑛 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
14841, 141, 147syl2anr 600 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ ℕ) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
14996, 148syldan 594 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
150149sumeq2dv 15267 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)))
15165adantr 484 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ)
15224nn0zd 12280 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ ℤ)
153152peano2zd 12285 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁𝐾) + 1) ∈ ℤ)
15496nnrpd 12626 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → 𝑛 ∈ ℝ+)
155141adantr 484 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → 𝑁 ∈ ℝ+)
156154, 155rpdivcld 12645 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (𝑛 / 𝑁) ∈ ℝ+)
157156relogcld 25511 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℝ)
158157recnd 10861 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℂ)
159 fvoveq1 7236 . . . . . 6 (𝑛 = (𝑁𝑘) → (log‘(𝑛 / 𝑁)) = (log‘((𝑁𝑘) / 𝑁)))
160151, 153, 151, 158, 159fsumrev 15343 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ ((𝑁𝑁)...(𝑁 − ((𝑁𝐾) + 1)))(log‘((𝑁𝑘) / 𝑁)))
161130subidd 11177 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝑁) = 0)
162 1cnd 10828 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℂ)
163130, 139, 162subsubd 11217 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝐾 − 1)) = ((𝑁𝐾) + 1))
164163oveq2d 7229 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝑁 − ((𝑁𝐾) + 1)))
165 ax-1cn 10787 . . . . . . . . . 10 1 ∈ ℂ
166 subcl 11077 . . . . . . . . . 10 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐾 − 1) ∈ ℂ)
167139, 165, 166sylancl 589 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 − 1) ∈ ℂ)
168130, 167nncand 11194 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝐾 − 1))
169164, 168eqtr3d 2779 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − ((𝑁𝐾) + 1)) = (𝐾 − 1))
170161, 169oveq12d 7231 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁𝑁)...(𝑁 − ((𝑁𝐾) + 1))) = (0...(𝐾 − 1)))
171130adantr 484 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℂ)
172 elfznn0 13205 . . . . . . . . . . 11 (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℕ0)
173172adantl 485 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℕ0)
174173nn0cnd 12152 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℂ)
175132adantr 484 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 ≠ 0)
176171, 174, 171, 175divsubdird 11647 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁𝑘) / 𝑁) = ((𝑁 / 𝑁) − (𝑘 / 𝑁)))
177171, 175dividd 11606 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝑁 / 𝑁) = 1)
178177oveq1d 7228 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 / 𝑁) − (𝑘 / 𝑁)) = (1 − (𝑘 / 𝑁)))
179176, 178eqtrd 2777 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁𝑘) / 𝑁) = (1 − (𝑘 / 𝑁)))
180179fveq2d 6721 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (log‘((𝑁𝑘) / 𝑁)) = (log‘(1 − (𝑘 / 𝑁))))
181170, 180sumeq12rdv 15271 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑘 ∈ ((𝑁𝑁)...(𝑁 − ((𝑁𝐾) + 1)))(log‘((𝑁𝑘) / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
182160, 181eqtrd 2777 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
183143adantr 484 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)) → (log‘𝑁) ∈ ℂ)
18491, 97, 183fsumsub 15352 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑁)))
185 fsumconst 15354 . . . . . . . 8 (((((𝑁𝐾) + 1)...𝑁) ∈ Fin ∧ (log‘𝑁) ∈ ℂ) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑁) = ((♯‘(((𝑁𝐾) + 1)...𝑁)) · (log‘𝑁)))
18691, 143, 185syl2anc 587 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑁) = ((♯‘(((𝑁𝐾) + 1)...𝑁)) · (log‘𝑁)))
187 1zzd 12208 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℤ)
188 fzen 13129 . . . . . . . . . . . 12 ((1 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑁𝐾) ∈ ℤ) → (1...𝐾) ≈ ((1 + (𝑁𝐾))...(𝐾 + (𝑁𝐾))))
189187, 134, 152, 188syl3anc 1373 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ ((1 + (𝑁𝐾))...(𝐾 + (𝑁𝐾))))
19024nn0cnd 12152 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ ℂ)
191 addcom 11018 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ (𝑁𝐾) ∈ ℂ) → (1 + (𝑁𝐾)) = ((𝑁𝐾) + 1))
192165, 190, 191sylancr 590 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1 + (𝑁𝐾)) = ((𝑁𝐾) + 1))
193139, 130pncan3d 11192 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 + (𝑁𝐾)) = 𝑁)
194192, 193oveq12d 7231 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1 + (𝑁𝐾))...(𝐾 + (𝑁𝐾))) = (((𝑁𝐾) + 1)...𝑁))
195189, 194breqtrd 5079 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ (((𝑁𝐾) + 1)...𝑁))
196 hasheni 13914 . . . . . . . . . 10 ((1...𝐾) ≈ (((𝑁𝐾) + 1)...𝑁) → (♯‘(1...𝐾)) = (♯‘(((𝑁𝐾) + 1)...𝑁)))
197195, 196syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝐾)) = (♯‘(((𝑁𝐾) + 1)...𝑁)))
198197, 11eqtr3d 2779 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(((𝑁𝐾) + 1)...𝑁)) = 𝐾)
199198oveq1d 7228 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(((𝑁𝐾) + 1)...𝑁)) · (log‘𝑁)) = (𝐾 · (log‘𝑁)))
200186, 199eqtrd 2777 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑁) = (𝐾 · (log‘𝑁)))
201200oveq2d 7229 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑁)) = (Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))))
202184, 201eqtrd 2777 . . . 4 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))))
203150, 182, 2023eqtr3rd 2786 . . 3 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
204203fveq2d 6721 . 2 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))
205138, 146, 2043eqtr2d 2783 1 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2110  {cab 2714  wne 2940  cun 3864  cin 3865  c0 4237   class class class wbr 5053  wf 6376  1-1wf1 6377  cfv 6380  (class class class)co 7213  m cmap 8508  cen 8623  Fincfn 8626  cc 10727  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734   < clt 10867  cle 10868  cmin 11062   / cdiv 11489  cn 11830  0cn0 12090  cz 12176  cuz 12438  +crp 12586  ...cfz 13095  cexp 13635  !cfa 13839  Ccbc 13868  chash 13896  Σcsu 15249  expce 15623  logclog 25443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808  ax-mulf 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-supp 7904  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-oadd 8206  df-er 8391  df-map 8510  df-pm 8511  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fsupp 8986  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-xnn0 12163  df-z 12177  df-dec 12294  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ioc 12940  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-mod 13443  df-seq 13575  df-exp 13636  df-fac 13840  df-bc 13869  df-hash 13897  df-shft 14630  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-limsup 15032  df-clim 15049  df-rlim 15050  df-sum 15250  df-ef 15629  df-sin 15631  df-cos 15632  df-pi 15634  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-ress 16785  df-plusg 16815  df-mulr 16816  df-starv 16817  df-sca 16818  df-vsca 16819  df-ip 16820  df-tset 16821  df-ple 16822  df-ds 16824  df-unif 16825  df-hom 16826  df-cco 16827  df-rest 16927  df-topn 16928  df-0g 16946  df-gsum 16947  df-topgen 16948  df-pt 16949  df-prds 16952  df-xrs 17007  df-qtop 17012  df-imas 17013  df-xps 17015  df-mre 17089  df-mrc 17090  df-acs 17092  df-mgm 18114  df-sgrp 18163  df-mnd 18174  df-submnd 18219  df-mulg 18489  df-cntz 18711  df-cmn 19172  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-fbas 20360  df-fg 20361  df-cnfld 20364  df-top 21791  df-topon 21808  df-topsp 21830  df-bases 21843  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-lp 22033  df-perf 22034  df-cn 22124  df-cnp 22125  df-haus 22212  df-tx 22459  df-hmeo 22652  df-fil 22743  df-fm 22835  df-flim 22836  df-flf 22837  df-xms 23218  df-ms 23219  df-tms 23220  df-cncf 23775  df-limc 24763  df-dv 24764  df-log 25445
This theorem is referenced by:  birthdaylem3  25836
  Copyright terms: Public domain W3C validator