Step | Hyp | Ref
| Expression |
1 | | bcval2 9677 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
2 | 1 | adantl 271 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
3 | | simprl 497 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝑘 ∈ ℂ) |
4 | | simprr 498 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝑥 ∈ ℂ) |
5 | 3, 4 | mulcld 7139 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
6 | | simpr1 944 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑘 ∈ ℂ) |
7 | | simpr2 945 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑥 ∈ ℂ) |
8 | | simpr3 946 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑦 ∈ ℂ) |
9 | 6, 7, 8 | mulassd 7142 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
10 | | simpll 495 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) |
11 | 10 | nn0zd 8467 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ) |
12 | | simplr 496 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ) |
13 | 12 | nnzd 8468 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℤ) |
14 | 11, 13 | zsubcld 8474 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
15 | 14 | peano2zd 8472 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
16 | | 1red 7134 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 1 ∈
ℝ) |
17 | 12 | nnred 8052 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℝ) |
18 | 10 | nn0red 8342 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
19 | 12 | nnge1d 8081 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 1 ≤ 𝐾) |
20 | 16, 17, 18, 19 | lesub2dd 7662 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ≤ (𝑁 − 1)) |
21 | 14 | zred 8469 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ) |
22 | | leaddsub 7542 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 𝐾) ∈ ℝ ∧ 1 ∈ ℝ
∧ 𝑁 ∈ ℝ)
→ (((𝑁 − 𝐾) + 1) ≤ 𝑁 ↔ (𝑁 − 𝐾) ≤ (𝑁 − 1))) |
23 | 21, 16, 18, 22 | syl3anc 1169 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((𝑁 − 𝐾) + 1) ≤ 𝑁 ↔ (𝑁 − 𝐾) ≤ (𝑁 − 1))) |
24 | 20, 23 | mpbird 165 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) |
25 | | eluz2 8625 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ (((𝑁 − 𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) |
26 | 15, 11, 24, 25 | syl3anbrc 1122 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
27 | 26 | adantrr 462 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) |
28 | | cnex 7097 |
. . . . . . . . 9
⊢ ℂ
∈ V |
29 | 28 | a1i 9 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ℂ ∈
V) |
30 | | simprr 498 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℕ) |
31 | | nnuz 8654 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
32 | 30, 31 | syl6eleq 2171 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈
(ℤ≥‘1)) |
33 | | vex 2604 |
. . . . . . . . . 10
⊢ 𝑘 ∈ V |
34 | | fvi 5251 |
. . . . . . . . . 10
⊢ (𝑘 ∈ V → ( I
‘𝑘) = 𝑘) |
35 | 33, 34 | ax-mp 7 |
. . . . . . . . 9
⊢ ( I
‘𝑘) = 𝑘 |
36 | | eluzelcn 8630 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℂ) |
37 | 36 | adantl 271 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℂ) |
38 | 35, 37 | syl5eqel 2165 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘1))
→ ( I ‘𝑘) ∈
ℂ) |
39 | 5, 9, 27, 29, 32, 38 | iseqsplit 9458 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (seq1( · ,
I , ℂ)‘𝑁) =
((seq1( · , I , ℂ)‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁))) |
40 | | elfzuz3 9042 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
41 | 40 | adantl 271 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) |
42 | | eluznn 8687 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈ ℕ) |
43 | 12, 41, 42 | syl2anc 403 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ) |
44 | 43 | adantrr 462 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℕ) |
45 | | facnn 9654 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) = (seq1(
· , I , ℂ)‘𝑁)) |
46 | 44, 45 | syl 14 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = (seq1( · , I ,
ℂ)‘𝑁)) |
47 | | facnn 9654 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ → (!‘(𝑁 − 𝐾)) = (seq1( · , I ,
ℂ)‘(𝑁 −
𝐾))) |
48 | 30, 47 | syl 14 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘(𝑁 − 𝐾)) = (seq1( · , I ,
ℂ)‘(𝑁 −
𝐾))) |
49 | 48 | oveq1d 5547 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)) = ((seq1( · , I ,
ℂ)‘(𝑁 −
𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁))) |
50 | 39, 46, 49 | 3eqtr4d 2123 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁))) |
51 | 50 | expr 367 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)))) |
52 | 10 | faccld 9663 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℕ) |
53 | 52 | nncnd 8053 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℂ) |
54 | 53 | mulid2d 7137 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) =
(!‘𝑁)) |
55 | 43, 45 | syl 14 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (seq1( · , I ,
ℂ)‘𝑁)) |
56 | 55 | oveq2d 5548 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) = (1 ·
(seq1( · , I , ℂ)‘𝑁))) |
57 | 54, 56 | eqtr3d 2115 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (1 · (seq1( ·
, I , ℂ)‘𝑁))) |
58 | | fveq2 5198 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = (!‘0)) |
59 | | fac0 9655 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
60 | 58, 59 | syl6eq 2129 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = 1) |
61 | | oveq1 5539 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = (0 + 1)) |
62 | | 0p1e1 8153 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
63 | 61, 62 | syl6eq 2129 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = 1) |
64 | | iseqeq1 9434 |
. . . . . . . . . 10
⊢ (((𝑁 − 𝐾) + 1) = 1 → seq((𝑁 − 𝐾) + 1)( · , I , ℂ) = seq1(
· , I , ℂ)) |
65 | 63, 64 | syl 14 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → seq((𝑁 − 𝐾) + 1)( · , I , ℂ) = seq1(
· , I , ℂ)) |
66 | 65 | fveq1d 5200 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) = (seq1( · , I ,
ℂ)‘𝑁)) |
67 | 60, 66 | oveq12d 5550 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) = 0 → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)) = (1 · (seq1( ·
, I , ℂ)‘𝑁))) |
68 | 67 | eqeq2d 2092 |
. . . . . 6
⊢ ((𝑁 − 𝐾) = 0 → ((!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)) ↔ (!‘𝑁) = (1 · (seq1( ·
, I , ℂ)‘𝑁)))) |
69 | 57, 68 | syl5ibrcom 155 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) = 0 → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)))) |
70 | | fznn0sub 9075 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
71 | 70 | adantl 271 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) |
72 | | elnn0 8290 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℕ0 ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
73 | 71, 72 | sylib 120 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) |
74 | 51, 69, 73 | mpjaod 670 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁))) |
75 | 74 | oveq1d 5547 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
76 | 28 | a1i 9 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ℂ ∈
V) |
77 | | vex 2604 |
. . . . . . 7
⊢ 𝑓 ∈ V |
78 | | fvi 5251 |
. . . . . . 7
⊢ (𝑓 ∈ V → ( I
‘𝑓) = 𝑓) |
79 | 77, 78 | ax-mp 7 |
. . . . . 6
⊢ ( I
‘𝑓) = 𝑓 |
80 | | eluzelcn 8630 |
. . . . . . 7
⊢ (𝑓 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑓 ∈ ℂ) |
81 | 80 | adantl 271 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑓 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) → 𝑓 ∈ ℂ) |
82 | 79, 81 | syl5eqel 2165 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑓 ∈ (ℤ≥‘((𝑁 − 𝐾) + 1))) → ( I ‘𝑓) ∈
ℂ) |
83 | | mulcl 7100 |
. . . . . 6
⊢ ((𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ) → (𝑓 · 𝑔) ∈ ℂ) |
84 | 83 | adantl 271 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ)) → (𝑓 · 𝑔) ∈ ℂ) |
85 | 26, 76, 82, 84 | iseqcl 9443 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) ∈
ℂ) |
86 | 12 | nnnn0d 8341 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈
ℕ0) |
87 | 86 | faccld 9663 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℕ) |
88 | 87 | nncnd 8053 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℂ) |
89 | 71 | faccld 9663 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
90 | 89 | nncnd 8053 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
91 | 87 | nnap0d 8084 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) # 0) |
92 | 89 | nnap0d 8084 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) # 0) |
93 | 85, 88, 90, 91, 92 | divcanap5d 7903 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) / (!‘𝐾))) |
94 | 2, 75, 93 | 3eqtrd 2117 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) / (!‘𝐾))) |
95 | | simplr 496 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ) |
96 | 95 | nnnn0d 8341 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ0) |
97 | 96 | faccld 9663 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) ∈
ℕ) |
98 | 97 | nncnd 8053 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) ∈
ℂ) |
99 | 97 | nnap0d 8084 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
(!‘𝐾) #
0) |
100 | 98, 99 | div0apd 7875 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 /
(!‘𝐾)) =
0) |
101 | | mulcl 7100 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
102 | 101 | adantl 271 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
103 | | eluzelcn 8630 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑘 ∈ ℂ) |
104 | 103 | adantl 271 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) → 𝑘 ∈ ℂ) |
105 | 35, 104 | syl5eqel 2165 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) → ( I ‘𝑘) ∈
ℂ) |
106 | 28 | a1i 9 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ℂ
∈ V) |
107 | | simpr 108 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → 𝑘 ∈
ℂ) |
108 | 107 | mul02d 7496 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (0
· 𝑘) =
0) |
109 | 107 | mul01d 7497 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) =
0) |
110 | | simpr 108 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 𝐾 ∈ (0...𝑁)) |
111 | | nn0uz 8653 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
112 | 96, 111 | syl6eleq 2171 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
(ℤ≥‘0)) |
113 | | simpll 495 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) |
114 | 113 | nn0zd 8467 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℤ) |
115 | | elfz5 9037 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
116 | 112, 114,
115 | syl2anc 403 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) |
117 | | nn0re 8297 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
118 | 117 | ad2antrr 471 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℝ) |
119 | | nnre 8046 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
120 | 119 | ad2antlr 472 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℝ) |
121 | 118, 120 | subge0d 7635 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ≤
(𝑁 − 𝐾) ↔ 𝐾 ≤ 𝑁)) |
122 | 116, 121 | bitr4d 189 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 0 ≤ (𝑁 − 𝐾))) |
123 | 110, 122 | mtbid 629 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 0
≤ (𝑁 − 𝐾)) |
124 | | simpl 107 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝑁 ∈
ℕ0) |
125 | 124 | nn0zd 8467 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝑁 ∈
ℤ) |
126 | | simpr 108 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝐾 ∈
ℕ) |
127 | 126 | nnzd 8468 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 𝐾 ∈
ℤ) |
128 | 125, 127 | zsubcld 8474 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) |
129 | 128 | adantr 270 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
130 | | 0z 8362 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
131 | | zltnle 8397 |
. . . . . . . . 9
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤
(𝑁 − 𝐾))) |
132 | 129, 130,
131 | sylancl 404 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤ (𝑁 − 𝐾))) |
133 | 123, 132 | mpbird 165 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) < 0) |
134 | | zltp1le 8405 |
. . . . . . . 8
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
135 | 129, 130,
134 | sylancl 404 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) |
136 | 133, 135 | mpbid 145 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 0) |
137 | | nn0ge0 8313 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
138 | 137 | ad2antrr 471 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ≤
𝑁) |
139 | | 0zd 8363 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
ℤ) |
140 | 129 | peano2zd 8472 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) |
141 | | elfz 9035 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ ((𝑁
− 𝐾) + 1) ∈
ℤ ∧ 𝑁 ∈
ℤ) → (0 ∈ (((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
142 | 139, 140,
114, 141 | syl3anc 1169 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ∈
(((𝑁 − 𝐾) + 1)...𝑁) ↔ (((𝑁 − 𝐾) + 1) ≤ 0 ∧ 0 ≤ 𝑁))) |
143 | 136, 138,
142 | mpbir2and 885 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
(((𝑁 − 𝐾) + 1)...𝑁)) |
144 | | elex 2610 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
V) |
145 | 144 | ad2antrr 471 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈ V) |
146 | | 0cn 7111 |
. . . . . 6
⊢ 0 ∈
ℂ |
147 | | fvi 5251 |
. . . . . 6
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
148 | 146, 147 | mp1i 10 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ( I
‘0) = 0) |
149 | 102, 105,
106, 108, 109, 143, 145, 148 | iseqz 9469 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) = 0) |
150 | 149 | oveq1d 5547 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
((seq((𝑁 − 𝐾) + 1)( · , I ,
ℂ)‘𝑁) /
(!‘𝐾)) = (0 /
(!‘𝐾))) |
151 | | nnz 8370 |
. . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
152 | | bcval3 9678 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
153 | 151, 152 | syl3an2 1203 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
154 | 153 | 3expa 1138 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
155 | 100, 150,
154 | 3eqtr4rd 2124 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) / (!‘𝐾))) |
156 | | 0zd 8363 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ 0 ∈ ℤ) |
157 | | fzdcel 9059 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ) → DECID 𝐾 ∈ (0...𝑁)) |
158 | 127, 156,
125, 157 | syl3anc 1169 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ DECID 𝐾 ∈ (0...𝑁)) |
159 | | exmiddc 777 |
. . 3
⊢
(DECID 𝐾 ∈ (0...𝑁) → (𝐾 ∈ (0...𝑁) ∨ ¬ 𝐾 ∈ (0...𝑁))) |
160 | 158, 159 | syl 14 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝐾 ∈ (0...𝑁) ∨ ¬ 𝐾 ∈ (0...𝑁))) |
161 | 94, 155, 160 | mpjaodan 744 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I , ℂ)‘𝑁) / (!‘𝐾))) |