Step | Hyp | Ref
| Expression |
1 | | bcval2 10673 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
2 | 1 | adantl 275 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
3 | | simprl 526 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝑘 ∈ ℂ) |
4 | | simprr 527 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝑥 ∈ ℂ) |
5 | 3, 4 | mulcld 7929 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
6 | | simpr1 998 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑘 ∈ ℂ) |
7 | | simpr2 999 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑥 ∈ ℂ) |
8 | | simpr3 1000 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑦 ∈ ℂ) |
9 | 6, 7, 8 | mulassd 7932 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
10 | | simpll 524 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) |
11 | 10 | nn0zd 9321 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ) |
12 | | simplr 525 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ) |
13 | 12 | nnzd 9322 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℤ) |
14 | 11, 13 | zsubcld 9328 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
15 | 14 | peano2zd 9326 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
16 | | 1red 7924 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 1 ∈
ℝ) |
17 | 12 | nnred 8880 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℝ) |
18 | 10 | nn0red 9178 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
19 | 12 | nnge1d 8910 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 1 ≤ 𝐾) |
20 | 16, 17, 18, 19 | lesub2dd 8470 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ≤ (𝑁 − 1)) |
21 | 14 | zred 9323 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ) |
22 | | leaddsub 8346 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 𝐾) ∈ ℝ ∧ 1 ∈ ℝ
∧ 𝑁 ∈ ℝ)
→ (((𝑁 − 𝐾) + 1) ≤ 𝑁 ↔ (𝑁 − 𝐾) ≤ (𝑁 − 1))) |
23 | 21, 16, 18, 22 | syl3anc 1233 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((𝑁 − 𝐾) + 1) ≤ 𝑁 ↔ (𝑁 − 𝐾) ≤ (𝑁 − 1))) |
24 | 20, 23 | mpbird 166 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) |
25 | | eluz2 9482 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ (((𝑁 − 𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
26 | 15, 11, 24, 25 | syl3anbrc 1176 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
27 | 26 | adantrr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
28 | | simprr 527 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℕ) |
29 | | nnuz 9511 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
30 | 28, 29 | eleqtrdi 2263 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈
(ℤ≥‘1)) |
31 | | fvi 5551 |
. . . . . . . . . 10
⊢ (𝑘 ∈ V → ( I
‘𝑘) = 𝑘) |
32 | 31 | elv 2734 |
. . . . . . . . 9
⊢ ( I
‘𝑘) = 𝑘 |
33 | | eluzelcn 9487 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℂ) |
34 | 33 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℂ) |
35 | 32, 34 | eqeltrid 2257 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘1))
→ ( I ‘𝑘) ∈
ℂ) |
36 | 5, 9, 27, 30, 35 | seq3split 10424 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (seq1( · ,
I )‘𝑁) = ((seq1(
· , I )‘(𝑁
− 𝐾)) ·
(seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁))) |
37 | | elfzuz3 9967 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
38 | 37 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
39 | | eluznn 9548 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈ ℕ) |
40 | 12, 38, 39 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ) |
41 | 40 | adantrr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℕ) |
42 | | facnn 10650 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) = (seq1(
· , I )‘𝑁)) |
43 | 41, 42 | syl 14 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) |
44 | | facnn 10650 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) |
45 | 28, 44 | syl 14 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) |
46 | 45 | oveq1d 5866 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = ((seq1( · , I
)‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
47 | 36, 43, 46 | 3eqtr4d 2213 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
48 | 47 | expr 373 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) |
49 | 10 | faccld 10659 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℕ) |
50 | 49 | nncnd 8881 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℂ) |
51 | 50 | mulid2d 7927 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) =
(!‘𝑁)) |
52 | 40, 42 | syl 14 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) |
53 | 52 | oveq2d 5867 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) = (1 ·
(seq1( · , I )‘𝑁))) |
54 | 51, 53 | eqtr3d 2205 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁))) |
55 | | fveq2 5494 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = (!‘0)) |
56 | | fac0 10651 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
57 | 55, 56 | eqtrdi 2219 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = 1) |
58 | | oveq1 5858 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = (0 + 1)) |
59 | | 0p1e1 8981 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
60 | 58, 59 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = 1) |
61 | 60 | seqeq1d 10396 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → seq((𝑁 − 𝐾) + 1)( · , I ) = seq1( · , I
)) |
62 | 61 | fveq1d 5496 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = (seq1( · , I
)‘𝑁)) |
63 | 57, 62 | oveq12d 5869 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) = 0 → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = (1 · (seq1( ·
, I )‘𝑁))) |
64 | 63 | eqeq2d 2182 |
. . . . . 6
⊢ ((𝑁 − 𝐾) = 0 → ((!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) ↔ (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁)))) |
65 | 54, 64 | syl5ibrcom 156 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) = 0 → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) |
66 | | fznn0sub 10002 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
67 | 66 | adantl 275 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) |
68 | | elnn0 9126 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℕ0 ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
69 | 67, 68 | sylib 121 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
70 | 48, 65, 69 | mpjaod 713 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) |
71 | 70 | oveq1d 5866 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
72 | | eqid 2170 |
. . . . . 6
⊢
(ℤ≥‘((𝑁 − 𝐾) + 1)) =
(ℤ≥‘((𝑁 − 𝐾) + 1)) |
73 | | fvi 5551 |
. . . . . . . 8
⊢ (𝑓 ∈ V → ( I
‘𝑓) = 𝑓) |
74 | 73 | elv 2734 |
. . . . . . 7
⊢ ( I
‘𝑓) = 𝑓 |
75 | | eluzelcn 9487 |
. . . . . . . 8
⊢ (𝑓 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑓 ∈ ℂ) |
76 | 75 | adantl 275 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑓 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) → 𝑓 ∈ ℂ) |
77 | 74, 76 | eqeltrid 2257 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑓 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) → ( I ‘𝑓) ∈
ℂ) |
78 | | mulcl 7890 |
. . . . . . 7
⊢ ((𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ) → (𝑓 · 𝑔) ∈ ℂ) |
79 | 78 | adantl 275 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ)) → (𝑓 · 𝑔) ∈ ℂ) |
80 | 72, 15, 77, 79 | seqf 10406 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → seq((𝑁 − 𝐾) + 1)( · , I
):(ℤ≥‘((𝑁 − 𝐾) + 1))⟶ℂ) |
81 | 80, 26 | ffvelrnd 5630 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) ∈
ℂ) |
82 | 12 | nnnn0d 9177 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈
ℕ0) |
83 | 82 | faccld 10659 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℕ) |
84 | 83 | nncnd 8881 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℂ) |
85 | 67 | faccld 10659 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
86 | 85 | nncnd 8881 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
87 | 83 | nnap0d 8913 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) # 0) |
88 | 85 | nnap0d 8913 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) # 0) |
89 | 81, 84, 86, 87, 88 | divcanap5d 8723 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
90 | 2, 71, 89 | 3eqtrd 2207 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
91 | | simplr 525 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ) |
92 | 91 | nnnn0d 9177 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ0) |
93 | 92 | faccld 10659 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) ∈
ℕ) |
94 | 93 | nncnd 8881 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) ∈
ℂ) |
95 | 93 | nnap0d 8913 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) #
0) |
96 | 94, 95 | div0apd 8693 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 /
(!‘𝐾)) =
0) |
97 | | mulcl 7890 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
98 | 97 | adantl 275 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
99 | | eluzelcn 9487 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑘 ∈ ℂ) |
100 | 99 | adantl 275 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) → 𝑘 ∈ ℂ) |
101 | 32, 100 | eqeltrid 2257 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) → ( I ‘𝑘) ∈
ℂ) |
102 | | simpr 109 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → 𝑘 ∈
ℂ) |
103 | 102 | mul02d 8300 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (0
· 𝑘) =
0) |
104 | 102 | mul01d 8301 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) =
0) |
105 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 𝐾 ∈ (0...𝑁)) |
106 | | nn0uz 9510 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
107 | 92, 106 | eleqtrdi 2263 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
(ℤ≥‘0)) |
108 | | simpll 524 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) |
109 | 108 | nn0zd 9321 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℤ) |
110 | | elfz5 9962 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
111 | 107, 109,
110 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
112 | | nn0re 9133 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
113 | 112 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℝ) |
114 | | nnre 8874 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
115 | 114 | ad2antlr 486 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℝ) |
116 | 113, 115 | subge0d 8443 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ≤
(𝑁 − 𝐾) ↔ 𝐾 ≤ 𝑁)) |
117 | 111, 116 | bitr4d 190 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 0 ≤ (𝑁 − 𝐾))) |
118 | 105, 117 | mtbid 667 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 0
≤ (𝑁 − 𝐾)) |
119 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝑁 ∈
ℕ0) |
120 | 119 | nn0zd 9321 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝑁 ∈
ℤ) |
121 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝐾 ∈
ℕ) |
122 | 121 | nnzd 9322 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝐾 ∈
ℤ) |
123 | 120, 122 | zsubcld 9328 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
124 | 123 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
125 | | 0z 9212 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
126 | | zltnle 9247 |
. . . . . . . . 9
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤
(𝑁 − 𝐾))) |
127 | 124, 125,
126 | sylancl 411 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤ (𝑁 − 𝐾))) |
128 | 118, 127 | mpbird 166 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) < 0) |
129 | | zltp1le 9255 |
. . . . . . . 8
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
130 | 124, 125,
129 | sylancl 411 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
131 | 128, 130 | mpbid 146 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 0) |
132 | | nn0ge0 9149 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
133 | 132 | ad2antrr 485 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ≤
𝑁) |
134 | | 0zd 9213 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
ℤ) |
135 | 124 | peano2zd 9326 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
136 | | elfz 9960 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ ((𝑁
− 𝐾) + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ) → (0 ∈ (((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
137 | 134, 135,
109, 136 | syl3anc 1233 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ∈
(((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
138 | 131, 133,
137 | mpbir2and 939 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
(((𝑁 − 𝐾) + 1)...𝑁)) |
139 | | 0cn 7901 |
. . . . . 6
⊢ 0 ∈
ℂ |
140 | | fvi 5551 |
. . . . . 6
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
141 | 139, 140 | mp1i 10 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ( I
‘0) = 0) |
142 | 98, 101, 103, 104, 138, 141 | seq3z 10456 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = 0) |
143 | 142 | oveq1d 5866 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
((seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁) / (!‘𝐾)) = (0 / (!‘𝐾))) |
144 | | nnz 9220 |
. . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
145 | | bcval3 10674 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
146 | 144, 145 | syl3an2 1267 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
147 | 146 | 3expa 1198 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
148 | 96, 143, 147 | 3eqtr4rd 2214 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |
149 | | 0zd 9213 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 0 ∈ ℤ) |
150 | | fzdcel 9985 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ) → DECID 𝐾 ∈ (0...𝑁)) |
151 | 122, 149,
120, 150 | syl3anc 1233 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ DECID 𝐾 ∈ (0...𝑁)) |
152 | | exmiddc 831 |
. . 3
⊢
(DECID 𝐾 ∈ (0...𝑁) → (𝐾 ∈ (0...𝑁) ∨ ¬ 𝐾 ∈ (0...𝑁))) |
153 | 151, 152 | syl 14 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝐾 ∈ (0...𝑁) ∨ ¬ 𝐾 ∈ (0...𝑁))) |
154 | 90, 148, 153 | mpjaodan 793 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |