Step | Hyp | Ref
| Expression |
1 | | birthday.t |
. . . . . . 7
⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} |
2 | 1 | fveq2i 6194 |
. . . . . 6
⊢
(#‘𝑇) =
(#‘{𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}) |
3 | | fzfi 12771 |
. . . . . . 7
⊢
(1...𝐾) ∈
Fin |
4 | | fzfi 12771 |
. . . . . . 7
⊢
(1...𝑁) ∈
Fin |
5 | | hashf1 13241 |
. . . . . . 7
⊢
(((1...𝐾) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ (#‘{𝑓 ∣
𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(#‘(1...𝐾))) ·
((#‘(1...𝑁))C(#‘(1...𝐾))))) |
6 | 3, 4, 5 | mp2an 708 |
. . . . . 6
⊢
(#‘{𝑓 ∣
𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(#‘(1...𝐾))) ·
((#‘(1...𝑁))C(#‘(1...𝐾)))) |
7 | 2, 6 | eqtri 2644 |
. . . . 5
⊢
(#‘𝑇) =
((!‘(#‘(1...𝐾))) · ((#‘(1...𝑁))C(#‘(1...𝐾)))) |
8 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
9 | 8 | adantl 482 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈
ℕ0) |
10 | | hashfz1 13134 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (#‘(1...𝐾)) =
𝐾) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘(1...𝐾)) = 𝐾) |
12 | 11 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(#‘(1...𝐾))) = (!‘𝐾)) |
13 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
14 | | hashfz1 13134 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(#‘(1...𝑁)) = 𝑁) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘(1...𝑁)) = 𝑁) |
17 | 16, 11 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((#‘(1...𝑁))C(#‘(1...𝐾))) = (𝑁C𝐾)) |
18 | 12, 17 | oveq12d 6668 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘(#‘(1...𝐾))) ·
((#‘(1...𝑁))C(#‘(1...𝐾)))) = ((!‘𝐾) · (𝑁C𝐾))) |
19 | 7, 18 | syl5eq 2668 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘𝑇) = ((!‘𝐾) · (𝑁C𝐾))) |
20 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) |
21 | | faccl 13070 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℕ) |
23 | 22 | nncnd 11036 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℂ) |
24 | | fznn0sub 12373 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
25 | 24 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) |
26 | | faccl 13070 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
28 | 27 | nncnd 11036 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
29 | 27 | nnne0d 11065 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ≠ 0) |
30 | 23, 28, 29 | divcld 10801 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁 − 𝐾))) ∈ ℂ) |
31 | | faccl 13070 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
32 | 9, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℕ) |
33 | 32 | nncnd 11036 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℂ) |
34 | 32 | nnne0d 11065 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ≠ 0) |
35 | 30, 33, 34 | divcan2d 10803 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾))) = ((!‘𝑁) / (!‘(𝑁 − 𝐾)))) |
36 | | bcval2 13092 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
37 | 36 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
38 | 23, 28, 33, 29, 34 | divdiv1d 10832 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
39 | 37, 38 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾))) |
40 | 39 | oveq2d 6666 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾)))) |
41 | | fzfid 12772 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
42 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
43 | 42 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ) |
44 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
45 | 44 | relogcld 24369 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(log‘𝑛) ∈
ℝ) |
46 | 45 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(log‘𝑛) ∈
ℂ) |
47 | 43, 46 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ∈ ℂ) |
48 | 41, 47 | fsumcl 14464 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) ∈ ℂ) |
49 | | fzfid 12772 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...(𝑁 − 𝐾)) ∈ Fin) |
50 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(𝑁 − 𝐾)) → 𝑛 ∈ ℕ) |
51 | 50 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁 − 𝐾))) → 𝑛 ∈ ℕ) |
52 | 51, 46 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁 − 𝐾))) → (log‘𝑛) ∈ ℂ) |
53 | 49, 52 | fsumcl 14464 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) ∈ ℂ) |
54 | | efsub 14830 |
. . . . . . 7
⊢
((Σ𝑛 ∈
(1...𝑁)(log‘𝑛) ∈ ℂ ∧
Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) ∈ ℂ) →
(exp‘(Σ𝑛 ∈
(1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))) |
55 | 48, 53, 54 | syl2anc 693 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))) |
56 | 25 | nn0red 11352 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ) |
57 | 56 | ltp1d 10954 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) < ((𝑁 − 𝐾) + 1)) |
58 | | fzdisj 12368 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) < ((𝑁 − 𝐾) + 1) → ((1...(𝑁 − 𝐾)) ∩ (((𝑁 − 𝐾) + 1)...𝑁)) = ∅) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1...(𝑁 − 𝐾)) ∩ (((𝑁 − 𝐾) + 1)...𝑁)) = ∅) |
60 | | fznn0sub2 12446 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁)) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ (0...𝑁)) |
62 | | elfzle2 12345 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − 𝐾) ≤ 𝑁) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ≤ 𝑁) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ≤ 𝑁) |
65 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈ ℕ) |
66 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
67 | 65, 66 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈
(ℤ≥‘1)) |
68 | | nnz 11399 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → 𝑁 ∈ ℤ) |
70 | | elfz5 12334 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 − 𝐾) ∈ (ℤ≥‘1)
∧ 𝑁 ∈ ℤ)
→ ((𝑁 − 𝐾) ∈ (1...𝑁) ↔ (𝑁 − 𝐾) ≤ 𝑁)) |
71 | 67, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → ((𝑁 − 𝐾) ∈ (1...𝑁) ↔ (𝑁 − 𝐾) ≤ 𝑁)) |
72 | 64, 71 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈ (1...𝑁)) |
73 | | fzsplit 12367 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 𝐾) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁))) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁))) |
75 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (𝑁 − 𝐾) = 0) |
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...(𝑁 − 𝐾)) = (1...0)) |
77 | | fz10 12362 |
. . . . . . . . . . . . . 14
⊢ (1...0) =
∅ |
78 | 76, 77 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...(𝑁 − 𝐾)) = ∅) |
79 | 78 | uneq1d 3766 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁))) |
80 | | uncom 3757 |
. . . . . . . . . . . . . 14
⊢ (∅
∪ (((𝑁 − 𝐾) + 1)...𝑁)) = ((((𝑁 − 𝐾) + 1)...𝑁) ∪ ∅) |
81 | | un0 3967 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 − 𝐾) + 1)...𝑁) ∪ ∅) = (((𝑁 − 𝐾) + 1)...𝑁) |
82 | 80, 81 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (((𝑁 − 𝐾) + 1)...𝑁) |
83 | 75 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((𝑁 − 𝐾) + 1) = (0 + 1)) |
84 | | 1e0p1 11552 |
. . . . . . . . . . . . . . 15
⊢ 1 = (0 +
1) |
85 | 83, 84 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((𝑁 − 𝐾) + 1) = 1) |
86 | 85 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (((𝑁 − 𝐾) + 1)...𝑁) = (1...𝑁)) |
87 | 82, 86 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (1...𝑁)) |
88 | 79, 87 | eqtr2d 2657 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁))) |
89 | | elnn0 11294 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 𝐾) ∈ ℕ0 ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
90 | 25, 89 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
91 | 74, 88, 90 | mpjaodan 827 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁))) |
92 | 59, 91, 41, 47 | fsumsplit 14471 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛))) |
93 | 92 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) = ((Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) |
94 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((𝑁 − 𝐾) + 1)...𝑁) ∈ Fin) |
95 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 𝐾) ∈ ℕ0 → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
96 | 25, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
97 | | elfzuz 12338 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑛 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) |
98 | | eluznn 11758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 − 𝐾) + 1) ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) → 𝑛 ∈ ℕ) |
99 | 96, 97, 98 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑛 ∈ ℕ) |
100 | 99, 46 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘𝑛) ∈ ℂ) |
101 | 94, 100 | fsumcl 14464 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ) |
102 | 53, 101 | pncan2d 10394 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) = Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) |
103 | 93, 102 | eqtr2d 2657 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) |
104 | 103 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) = (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))) |
105 | 22 | nnne0d 11065 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ≠ 0) |
106 | | eflog 24323 |
. . . . . . . . 9
⊢
(((!‘𝑁) ∈
ℂ ∧ (!‘𝑁)
≠ 0) → (exp‘(log‘(!‘𝑁))) = (!‘𝑁)) |
107 | 23, 105, 106 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) →
(exp‘(log‘(!‘𝑁))) = (!‘𝑁)) |
108 | | logfac 24347 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) |
109 | 20, 108 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) |
110 | 109 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) →
(exp‘(log‘(!‘𝑁))) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛))) |
111 | 107, 110 | eqtr3d 2658 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛))) |
112 | | eflog 24323 |
. . . . . . . . 9
⊢
(((!‘(𝑁
− 𝐾)) ∈ ℂ
∧ (!‘(𝑁 −
𝐾)) ≠ 0) →
(exp‘(log‘(!‘(𝑁 − 𝐾)))) = (!‘(𝑁 − 𝐾))) |
113 | 28, 29, 112 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) →
(exp‘(log‘(!‘(𝑁 − 𝐾)))) = (!‘(𝑁 − 𝐾))) |
114 | | logfac 24347 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(log‘(!‘(𝑁
− 𝐾))) = Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) |
115 | 25, 114 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘(𝑁 − 𝐾))) = Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) |
116 | 115 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) →
(exp‘(log‘(!‘(𝑁 − 𝐾)))) = (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) |
117 | 113, 116 | eqtr3d 2658 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) = (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) |
118 | 111, 117 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁 − 𝐾))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))) |
119 | 55, 104, 118 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) = ((!‘𝑁) / (!‘(𝑁 − 𝐾)))) |
120 | 35, 40, 119 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛))) |
121 | 19, 120 | eqtrd 2656 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘𝑇) = (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛))) |
122 | | birthday.s |
. . . . . . . 8
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} |
123 | | mapvalg 7867 |
. . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝐾) ∈ Fin)
→ ((1...𝑁)
↑𝑚 (1...𝐾)) = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}) |
124 | 4, 3, 123 | mp2an 708 |
. . . . . . . 8
⊢
((1...𝑁)
↑𝑚 (1...𝐾)) = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} |
125 | 122, 124 | eqtr4i 2647 |
. . . . . . 7
⊢ 𝑆 = ((1...𝑁) ↑𝑚 (1...𝐾)) |
126 | 125 | fveq2i 6194 |
. . . . . 6
⊢
(#‘𝑆) =
(#‘((1...𝑁)
↑𝑚 (1...𝐾))) |
127 | | hashmap 13222 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝐾) ∈ Fin)
→ (#‘((1...𝑁)
↑𝑚 (1...𝐾))) = ((#‘(1...𝑁))↑(#‘(1...𝐾)))) |
128 | 4, 3, 127 | mp2an 708 |
. . . . . 6
⊢
(#‘((1...𝑁)
↑𝑚 (1...𝐾))) = ((#‘(1...𝑁))↑(#‘(1...𝐾))) |
129 | 126, 128 | eqtri 2644 |
. . . . 5
⊢
(#‘𝑆) =
((#‘(1...𝑁))↑(#‘(1...𝐾))) |
130 | 16, 11 | oveq12d 6668 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((#‘(1...𝑁))↑(#‘(1...𝐾))) = (𝑁↑𝐾)) |
131 | 129, 130 | syl5eq 2668 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘𝑆) = (𝑁↑𝐾)) |
132 | | nncn 11028 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
133 | 132 | adantr 481 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℂ) |
134 | | nnne0 11053 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
135 | 134 | adantr 481 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ≠ 0) |
136 | | elfzelz 12342 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
137 | 136 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℤ) |
138 | | explog 24340 |
. . . . 5
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ∧ 𝐾 ∈ ℤ) → (𝑁↑𝐾) = (exp‘(𝐾 · (log‘𝑁)))) |
139 | 133, 135,
137, 138 | syl3anc 1326 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁↑𝐾) = (exp‘(𝐾 · (log‘𝑁)))) |
140 | 131, 139 | eqtrd 2656 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘𝑆) = (exp‘(𝐾 · (log‘𝑁)))) |
141 | 121, 140 | oveq12d 6668 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((#‘𝑇) / (#‘𝑆)) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁))))) |
142 | 9 | nn0cnd 11353 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℂ) |
143 | | nnrp 11842 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
144 | 143 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℝ+) |
145 | 144 | relogcld 24369 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℝ) |
146 | 145 | recnd 10068 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℂ) |
147 | 142, 146 | mulcld 10060 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 · (log‘𝑁)) ∈ ℂ) |
148 | | efsub 14830 |
. . 3
⊢
((Σ𝑛 ∈
(((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ ∧ (𝐾 · (log‘𝑁)) ∈ ℂ) →
(exp‘(Σ𝑛 ∈
(((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁))))) |
149 | 101, 147,
148 | syl2anc 693 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁))))) |
150 | | relogdiv 24339 |
. . . . . . 7
⊢ ((𝑛 ∈ ℝ+
∧ 𝑁 ∈
ℝ+) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁))) |
151 | 44, 144, 150 | syl2anr 495 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ ℕ) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁))) |
152 | 99, 151 | syldan 487 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁))) |
153 | 152 | sumeq2dv 14433 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁))) |
154 | 68 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ) |
155 | 25 | nn0zd 11480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
156 | 155 | peano2zd 11485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
157 | 99, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑛 ∈ ℝ+) |
158 | 144 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑁 ∈
ℝ+) |
159 | 157, 158 | rpdivcld 11889 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (𝑛 / 𝑁) ∈
ℝ+) |
160 | 159 | relogcld 24369 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℝ) |
161 | 160 | recnd 10068 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℂ) |
162 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = (𝑁 − 𝑘) → (𝑛 / 𝑁) = ((𝑁 − 𝑘) / 𝑁)) |
163 | 162 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = (𝑁 − 𝑘) → (log‘(𝑛 / 𝑁)) = (log‘((𝑁 − 𝑘) / 𝑁))) |
164 | 154, 156,
154, 161, 163 | fsumrev 14511 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1)))(log‘((𝑁 − 𝑘) / 𝑁))) |
165 | 133 | subidd 10380 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝑁) = 0) |
166 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℂ) |
167 | 133, 142,
166 | subsubd 10420 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝐾 − 1)) = ((𝑁 − 𝐾) + 1)) |
168 | 167 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝑁 − ((𝑁 − 𝐾) + 1))) |
169 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
170 | | subcl 10280 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐾 −
1) ∈ ℂ) |
171 | 142, 169,
170 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 − 1) ∈ ℂ) |
172 | 133, 171 | nncand 10397 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝐾 − 1)) |
173 | 168, 172 | eqtr3d 2658 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − ((𝑁 − 𝐾) + 1)) = (𝐾 − 1)) |
174 | 165, 173 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1))) = (0...(𝐾 − 1))) |
175 | 133 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℂ) |
176 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℕ0) |
177 | 176 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℕ0) |
178 | 177 | nn0cnd 11353 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℂ) |
179 | 135 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 ≠ 0) |
180 | 175, 178,
175, 179 | divsubdird 10840 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 − 𝑘) / 𝑁) = ((𝑁 / 𝑁) − (𝑘 / 𝑁))) |
181 | 175, 179 | dividd 10799 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝑁 / 𝑁) = 1) |
182 | 181 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 / 𝑁) − (𝑘 / 𝑁)) = (1 − (𝑘 / 𝑁))) |
183 | 180, 182 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 − 𝑘) / 𝑁) = (1 − (𝑘 / 𝑁))) |
184 | 183 | fveq2d 6195 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (log‘((𝑁 − 𝑘) / 𝑁)) = (log‘(1 − (𝑘 / 𝑁)))) |
185 | 174, 184 | sumeq12rdv 14438 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑘 ∈ ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1)))(log‘((𝑁 − 𝑘) / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))) |
186 | 164, 185 | eqtrd 2656 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))) |
187 | 146 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘𝑁) ∈ ℂ) |
188 | 94, 100, 187 | fsumsub 14520 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁))) |
189 | | fsumconst 14522 |
. . . . . . . 8
⊢
(((((𝑁 − 𝐾) + 1)...𝑁) ∈ Fin ∧ (log‘𝑁) ∈ ℂ) →
Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = ((#‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁))) |
190 | 94, 146, 189 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = ((#‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁))) |
191 | | 1zzd 11408 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℤ) |
192 | | fzen 12358 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 𝐾
∈ ℤ ∧ (𝑁
− 𝐾) ∈ ℤ)
→ (1...𝐾) ≈ ((1
+ (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾)))) |
193 | 191, 137,
155, 192 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ ((1 + (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾)))) |
194 | 25 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℂ) |
195 | | addcom 10222 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (𝑁
− 𝐾) ∈ ℂ)
→ (1 + (𝑁 −
𝐾)) = ((𝑁 − 𝐾) + 1)) |
196 | 169, 194,
195 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1 + (𝑁 − 𝐾)) = ((𝑁 − 𝐾) + 1)) |
197 | 142, 133 | pncan3d 10395 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 + (𝑁 − 𝐾)) = 𝑁) |
198 | 196, 197 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1 + (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾))) = (((𝑁 − 𝐾) + 1)...𝑁)) |
199 | 193, 198 | breqtrd 4679 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ (((𝑁 − 𝐾) + 1)...𝑁)) |
200 | | hasheni 13136 |
. . . . . . . . . 10
⊢
((1...𝐾) ≈
(((𝑁 − 𝐾) + 1)...𝑁) → (#‘(1...𝐾)) = (#‘(((𝑁 − 𝐾) + 1)...𝑁))) |
201 | 199, 200 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘(1...𝐾)) = (#‘(((𝑁 − 𝐾) + 1)...𝑁))) |
202 | 201, 11 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (#‘(((𝑁 − 𝐾) + 1)...𝑁)) = 𝐾) |
203 | 202 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((#‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁)) = (𝐾 · (log‘𝑁))) |
204 | 190, 203 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = (𝐾 · (log‘𝑁))) |
205 | 204 | oveq2d 6666 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) |
206 | 188, 205 | eqtrd 2656 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) |
207 | 153, 186,
206 | 3eqtr3rd 2665 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))) |
208 | 207 | fveq2d 6195 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))) |
209 | 141, 149,
208 | 3eqtr2d 2662 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((#‘𝑇) / (#‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))) |