Step | Hyp | Ref
| Expression |
1 | | bcval2 12954 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
2 | 1 | adantl 481 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
3 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
5 | | mulass 9903 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
7 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ) |
8 | | elfzuz3 12210 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
10 | | eluznn 11634 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈ ℕ) |
11 | 7, 9, 10 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ) |
12 | 11 | adantrr 749 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℕ) |
13 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝐾 ∈ ℕ) |
14 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
15 | | nnrp 11718 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ+) |
16 | | ltsubrp 11742 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ+)
→ (𝑁 − 𝐾) < 𝑁) |
17 | 14, 15, 16 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 − 𝐾) < 𝑁) |
18 | 12, 13, 17 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) < 𝑁) |
19 | 12 | nnzd 11357 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℤ) |
20 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
21 | 20 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝐾 ∈ ℤ) |
22 | 19, 21 | zsubcld 11363 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℤ) |
23 | | zltp1le 11304 |
. . . . . . . . . . 11
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
24 | 22, 19, 23 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
25 | 18, 24 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) |
26 | 22 | peano2zd 11361 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
27 | | eluz 11577 |
. . . . . . . . . 10
⊢ ((((𝑁 − 𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
28 | 26, 19, 27 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
29 | 25, 28 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
30 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℕ) |
31 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
32 | 30, 31 | syl6eleq 2698 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈
(ℤ≥‘1)) |
33 | | fvi 6165 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → ( I ‘𝑘) = 𝑘) |
34 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
35 | 34 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ) |
36 | 33, 35 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → ( I ‘𝑘) ∈ ℂ) |
37 | 36 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (1...𝑁)) → ( I ‘𝑘) ∈ ℂ) |
38 | 4, 6, 29, 32, 37 | seqsplit 12696 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (seq1( · ,
I )‘𝑁) = ((seq1(
· , I )‘(𝑁
− 𝐾)) ·
(seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁))) |
39 | | facnn 12924 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) = (seq1(
· , I )‘𝑁)) |
40 | 12, 39 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) |
41 | | facnn 12924 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) |
42 | 30, 41 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) |
43 | 42 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = ((seq1( · , I
)‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
44 | 38, 40, 43 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
45 | 44 | expr 641 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) |
46 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) |
47 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
48 | | nncn 10905 |
. . . . . . . . 9
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℂ) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℂ) |
50 | 49 | mulid2d 9937 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) =
(!‘𝑁)) |
51 | 11, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) = (1 ·
(seq1( · , I )‘𝑁))) |
53 | 50, 52 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁))) |
54 | | fveq2 6103 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = (!‘0)) |
55 | | fac0 12925 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
56 | 54, 55 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = 1) |
57 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = (0 + 1)) |
58 | | 0p1e1 11009 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
59 | 57, 58 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = 1) |
60 | 59 | seqeq1d 12669 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → seq((𝑁 − 𝐾) + 1)( · , I ) = seq1( · , I
)) |
61 | 60 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = (seq1( · , I
)‘𝑁)) |
62 | 56, 61 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) = 0 → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = (1 · (seq1( ·
, I )‘𝑁))) |
63 | 62 | eqeq2d 2620 |
. . . . . 6
⊢ ((𝑁 − 𝐾) = 0 → ((!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) ↔ (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁)))) |
64 | 53, 63 | syl5ibrcom 236 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) = 0 → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) |
65 | | fznn0sub 12244 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
66 | 65 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) |
67 | | elnn0 11171 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℕ0 ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
68 | 66, 67 | sylib 207 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
69 | 45, 64, 68 | mpjaod 395 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
70 | 69 | oveq1d 6564 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
71 | | eqid 2610 |
. . . . . 6
⊢
(ℤ≥‘((𝑁 − 𝐾) + 1)) =
(ℤ≥‘((𝑁 − 𝐾) + 1)) |
72 | | nn0z 11277 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
73 | | zsubcl 11296 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 − 𝐾) ∈ ℤ) |
74 | 72, 20, 73 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
75 | 74 | peano2zd 11361 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ ((𝑁 − 𝐾) + 1) ∈
ℤ) |
76 | 75 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
77 | | fvi 6165 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → ( I ‘𝑘) = 𝑘) |
78 | | eluzelcn 11575 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑘 ∈ ℂ) |
79 | 77, 78 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → ( I ‘𝑘) ∈ ℂ) |
80 | 79 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) → ( I ‘𝑘) ∈
ℂ) |
81 | 3 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
82 | 71, 76, 80, 81 | seqf 12684 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → seq((𝑁 − 𝐾) + 1)( · , I
):(ℤ≥‘((𝑁 − 𝐾) + 1))⟶ℂ) |
83 | 11, 7, 17 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) < 𝑁) |
84 | 74 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
85 | 11 | nnzd 11357 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ) |
86 | 84, 85, 23 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
87 | 83, 86 | mpbid 221 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) |
88 | 76, 85, 27 | syl2anc 691 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
89 | 87, 88 | mpbird 246 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
90 | 82, 89 | ffvelrnd 6268 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) ∈
ℂ) |
91 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
92 | 91 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈
ℕ0) |
93 | | faccl 12932 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
94 | 92, 93 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℕ) |
95 | 94 | nncnd 10913 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℂ) |
96 | | faccl 12932 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
97 | 66, 96 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
98 | 97 | nncnd 10913 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
99 | 94 | nnne0d 10942 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ≠ 0) |
100 | 97 | nnne0d 10942 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ≠ 0) |
101 | 90, 95, 98, 99, 100 | divcan5d 10706 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
102 | 2, 70, 101 | 3eqtrd 2648 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
103 | | nnnn0 11176 |
. . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
104 | 103 | ad2antlr 759 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ0) |
105 | | nncn 10905 |
. . . . 5
⊢
((!‘𝐾) ∈
ℕ → (!‘𝐾)
∈ ℂ) |
106 | | nnne0 10930 |
. . . . 5
⊢
((!‘𝐾) ∈
ℕ → (!‘𝐾)
≠ 0) |
107 | 105, 106 | div0d 10679 |
. . . 4
⊢
((!‘𝐾) ∈
ℕ → (0 / (!‘𝐾)) = 0) |
108 | 104, 93, 107 | 3syl 18 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 /
(!‘𝐾)) =
0) |
109 | 3 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
110 | | fvi 6165 |
. . . . . . 7
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → ( I ‘𝑘) = 𝑘) |
111 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑘 ∈ ℤ) |
112 | 111 | zcnd 11359 |
. . . . . . 7
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑘 ∈ ℂ) |
113 | 110, 112 | eqeltrd 2688 |
. . . . . 6
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → ( I ‘𝑘) ∈ ℂ) |
114 | 113 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → ( I ‘𝑘) ∈ ℂ) |
115 | | mul02 10093 |
. . . . . 6
⊢ (𝑘 ∈ ℂ → (0
· 𝑘) =
0) |
116 | 115 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (0
· 𝑘) =
0) |
117 | | mul01 10094 |
. . . . . 6
⊢ (𝑘 ∈ ℂ → (𝑘 · 0) =
0) |
118 | 117 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) =
0) |
119 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 𝐾 ∈ (0...𝑁)) |
120 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
121 | 104, 120 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
(ℤ≥‘0)) |
122 | 72 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℤ) |
123 | | elfz5 12205 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
124 | 121, 122,
123 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
125 | | nn0re 11178 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
126 | 125 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℝ) |
127 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
128 | 127 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℝ) |
129 | 126, 128 | subge0d 10496 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ≤
(𝑁 − 𝐾) ↔ 𝐾 ≤ 𝑁)) |
130 | 124, 129 | bitr4d 270 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 0 ≤ (𝑁 − 𝐾))) |
131 | 119, 130 | mtbid 313 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 0
≤ (𝑁 − 𝐾)) |
132 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
133 | 132 | zred 11358 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ) |
134 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
135 | | ltnle 9996 |
. . . . . . . . 9
⊢ (((𝑁 − 𝐾) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤
(𝑁 − 𝐾))) |
136 | 133, 134,
135 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤ (𝑁 − 𝐾))) |
137 | 131, 136 | mpbird 246 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) < 0) |
138 | | 0z 11265 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
139 | | zltp1le 11304 |
. . . . . . . 8
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
140 | 132, 138,
139 | sylancl 693 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
141 | 137, 140 | mpbid 221 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 0) |
142 | | nn0ge0 11195 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
143 | 142 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ≤
𝑁) |
144 | | 0zd 11266 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
ℤ) |
145 | 75 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
146 | | elfz 12203 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ ((𝑁
− 𝐾) + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ) → (0 ∈ (((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
147 | 144, 145,
122, 146 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ∈
(((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
148 | 141, 143,
147 | mpbir2and 959 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
(((𝑁 − 𝐾) + 1)...𝑁)) |
149 | | simpll 786 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) |
150 | | 0cn 9911 |
. . . . . 6
⊢ 0 ∈
ℂ |
151 | | fvi 6165 |
. . . . . 6
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
152 | 150, 151 | mp1i 13 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ( I
‘0) = 0) |
153 | 109, 114,
116, 118, 148, 149, 152 | seqz 12711 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = 0) |
154 | 153 | oveq1d 6564 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
((seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁) / (!‘𝐾)) = (0 / (!‘𝐾))) |
155 | | bcval3 12955 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
156 | 20, 155 | syl3an2 1352 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
157 | 156 | 3expa 1257 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
158 | 108, 154,
157 | 3eqtr4rd 2655 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
159 | 102, 158 | pm2.61dan 828 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |