| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bcval2 14345 | . . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) | 
| 2 | 1 | adantl 481 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) | 
| 3 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) | 
| 4 | 3 | adantl 481 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) | 
| 5 |  | mulass 11244 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) | 
| 6 | 5 | adantl 481 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) | 
| 7 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ) | 
| 8 |  | elfzuz3 13562 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ (ℤ≥‘𝐾)) | 
| 10 |  | eluznn 12961 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈ ℕ) | 
| 11 | 7, 9, 10 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ) | 
| 12 | 11 | adantrr 717 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℕ) | 
| 13 |  | simplr 768 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝐾 ∈ ℕ) | 
| 14 |  | nnre 12274 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 15 |  | nnrp 13047 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ+) | 
| 16 |  | ltsubrp 13072 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ+)
→ (𝑁 − 𝐾) < 𝑁) | 
| 17 | 14, 15, 16 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 − 𝐾) < 𝑁) | 
| 18 | 12, 13, 17 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) < 𝑁) | 
| 19 | 12 | nnzd 12642 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈ ℤ) | 
| 20 |  | nnz 12636 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) | 
| 21 | 20 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝐾 ∈ ℤ) | 
| 22 | 19, 21 | zsubcld 12729 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℤ) | 
| 23 |  | zltp1le 12669 | . . . . . . . . . . 11
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 24 | 22, 19, 23 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 25 | 18, 24 | mpbid 232 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) | 
| 26 | 22 | peano2zd 12727 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) | 
| 27 |  | eluz 12893 | . . . . . . . . . 10
⊢ ((((𝑁 − 𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 28 | 26, 19, 27 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 29 | 25, 28 | mpbird 257 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) | 
| 30 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈ ℕ) | 
| 31 |  | nnuz 12922 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 32 | 30, 31 | eleqtrdi 2850 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (𝑁 − 𝐾) ∈
(ℤ≥‘1)) | 
| 33 |  | fvi 6984 | . . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → ( I ‘𝑘) = 𝑘) | 
| 34 |  | elfzelz 13565 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) | 
| 35 | 34 | zcnd 12725 | . . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ) | 
| 36 | 33, 35 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → ( I ‘𝑘) ∈ ℂ) | 
| 37 | 36 | adantl 481 | . . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) ∧ 𝑘 ∈ (1...𝑁)) → ( I ‘𝑘) ∈ ℂ) | 
| 38 | 4, 6, 29, 32, 37 | seqsplit 14077 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (seq1( · ,
I )‘𝑁) = ((seq1(
· , I )‘(𝑁
− 𝐾)) ·
(seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁))) | 
| 39 |  | facnn 14315 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) = (seq1(
· , I )‘𝑁)) | 
| 40 | 12, 39 | syl 17 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) | 
| 41 |  | facnn 14315 | . . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) | 
| 42 | 30, 41 | syl 17 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘(𝑁 − 𝐾)) = (seq1( · , I )‘(𝑁 − 𝐾))) | 
| 43 | 42 | oveq1d 7447 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = ((seq1( · , I
)‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) | 
| 44 | 38, 40, 43 | 3eqtr4d 2786 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ (𝐾 ∈ (0...𝑁) ∧ (𝑁 − 𝐾) ∈ ℕ)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) | 
| 45 | 44 | expr 456 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) | 
| 46 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) | 
| 47 |  | faccl 14323 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) | 
| 48 |  | nncn 12275 | . . . . . . . . 9
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℂ) | 
| 49 | 46, 47, 48 | 3syl 18 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈
ℂ) | 
| 50 | 49 | mullidd 11280 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) =
(!‘𝑁)) | 
| 51 | 11, 39 | syl 17 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (seq1( · , I
)‘𝑁)) | 
| 52 | 51 | oveq2d 7448 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (1 ·
(!‘𝑁)) = (1 ·
(seq1( · , I )‘𝑁))) | 
| 53 | 50, 52 | eqtr3d 2778 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁))) | 
| 54 |  | fveq2 6905 | . . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = (!‘0)) | 
| 55 |  | fac0 14316 | . . . . . . . . 9
⊢
(!‘0) = 1 | 
| 56 | 54, 55 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (!‘(𝑁 − 𝐾)) = 1) | 
| 57 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = (0 + 1)) | 
| 58 |  | 0p1e1 12389 | . . . . . . . . . . 11
⊢ (0 + 1) =
1 | 
| 59 | 57, 58 | eqtrdi 2792 | . . . . . . . . . 10
⊢ ((𝑁 − 𝐾) = 0 → ((𝑁 − 𝐾) + 1) = 1) | 
| 60 | 59 | seqeq1d 14049 | . . . . . . . . 9
⊢ ((𝑁 − 𝐾) = 0 → seq((𝑁 − 𝐾) + 1)( · , I ) = seq1( · , I
)) | 
| 61 | 60 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝑁 − 𝐾) = 0 → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = (seq1( · , I
)‘𝑁)) | 
| 62 | 56, 61 | oveq12d 7450 | . . . . . . 7
⊢ ((𝑁 − 𝐾) = 0 → ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) = (1 · (seq1( ·
, I )‘𝑁))) | 
| 63 | 62 | eqeq2d 2747 | . . . . . 6
⊢ ((𝑁 − 𝐾) = 0 → ((!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) ↔ (!‘𝑁) = (1 · (seq1( ·
, I )‘𝑁)))) | 
| 64 | 53, 63 | syl5ibrcom 247 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) = 0 → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)))) | 
| 65 |  | fznn0sub 13597 | . . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) | 
| 66 | 65 | adantl 481 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) | 
| 67 |  | elnn0 12530 | . . . . . 6
⊢ ((𝑁 − 𝐾) ∈ ℕ0 ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) | 
| 68 | 66, 67 | sylib 218 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0)) | 
| 69 | 45, 64, 68 | mpjaod 860 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = ((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁))) | 
| 70 | 69 | oveq1d 7447 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) | 
| 71 |  | eqid 2736 | . . . . . 6
⊢
(ℤ≥‘((𝑁 − 𝐾) + 1)) =
(ℤ≥‘((𝑁 − 𝐾) + 1)) | 
| 72 |  | nn0z 12640 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 73 |  | zsubcl 12661 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 − 𝐾) ∈ ℤ) | 
| 74 | 72, 20, 73 | syl2an 596 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁 − 𝐾) ∈
ℤ) | 
| 75 | 74 | peano2zd 12727 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ ((𝑁 − 𝐾) + 1) ∈
ℤ) | 
| 76 | 75 | adantr 480 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) | 
| 77 |  | fvi 6984 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → ( I ‘𝑘) = 𝑘) | 
| 78 |  | eluzelcn 12891 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) → 𝑘 ∈ ℂ) | 
| 79 | 77, 78 | eqeltrd 2840 | . . . . . . 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 14065 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → seq((𝑁 − 𝐾) + 1)( · , I
):(ℤ≥‘((𝑁 − 𝐾) + 1))⟶ℂ) | 
| 83 | 11, 7, 17 | syl2anc 584 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) < 𝑁) | 
| 84 | 74 | adantr 480 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) | 
| 85 | 11 | nnzd 12642 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ) | 
| 86 | 84, 85, 23 | syl2anc 584 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) < 𝑁 ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 87 | 83, 86 | mpbid 232 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 𝑁) | 
| 88 | 76, 85, 27 | syl2anc 584 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1)) ↔ ((𝑁 − 𝐾) + 1) ≤ 𝑁)) | 
| 89 | 87, 88 | mpbird 257 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝐾) + 1))) | 
| 90 | 82, 89 | ffvelcdmd 7104 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) ∈
ℂ) | 
| 91 |  | elfznn0 13661 | . . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) | 
| 92 | 91 | adantl 481 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈
ℕ0) | 
| 93 | 92 | faccld 14324 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℕ) | 
| 94 | 93 | nncnd 12283 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈
ℂ) | 
| 95 | 66 | faccld 14324 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ) | 
| 96 | 95 | nncnd 12283 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ) | 
| 97 | 93 | nnne0d 12317 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ≠ 0) | 
| 98 | 95 | nnne0d 12317 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ≠ 0) | 
| 99 | 90, 94, 96, 97, 98 | divcan5d 12070 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (((!‘(𝑁 − 𝐾)) · (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁)) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) | 
| 100 | 2, 70, 99 | 3eqtrd 2780 | . 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) | 
| 101 |  | nnnn0 12535 | . . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) | 
| 102 | 101 | ad2antlr 727 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℕ0) | 
| 103 |  | faccl 14323 | . . . 4
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) | 
| 104 |  | nncn 12275 | . . . . 5
⊢
((!‘𝐾) ∈
ℕ → (!‘𝐾)
∈ ℂ) | 
| 105 |  | nnne0 12301 | . . . . 5
⊢
((!‘𝐾) ∈
ℕ → (!‘𝐾)
≠ 0) | 
| 106 | 104, 105 | div0d 12043 | . . . 4
⊢
((!‘𝐾) ∈
ℕ → (0 / (!‘𝐾)) = 0) | 
| 107 | 102, 103,
106 | 3syl 18 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 /
(!‘𝐾)) =
0) | 
| 108 | 3 | adantl 481 | . . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) | 
| 109 |  | fvi 6984 | . . . . . . 7
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → ( I ‘𝑘) = 𝑘) | 
| 110 |  | elfzelz 13565 | . . . . . . . 8
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑘 ∈ ℤ) | 
| 111 | 110 | zcnd 12725 | . . . . . . 7
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑘 ∈ ℂ) | 
| 112 | 109, 111 | eqeltrd 2840 | . . . . . 6
⊢ (𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → ( I ‘𝑘) ∈ ℂ) | 
| 113 | 112 | adantl 481 | . . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → ( I ‘𝑘) ∈ ℂ) | 
| 114 |  | mul02 11440 | . . . . . 6
⊢ (𝑘 ∈ ℂ → (0
· 𝑘) =
0) | 
| 115 | 114 | adantl 481 | . . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (0
· 𝑘) =
0) | 
| 116 |  | mul01 11441 | . . . . . 6
⊢ (𝑘 ∈ ℂ → (𝑘 · 0) =
0) | 
| 117 | 116 | adantl 481 | . . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) ∧ 𝑘 ∈ ℂ) → (𝑘 · 0) =
0) | 
| 118 | 75 | adantr 480 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ) | 
| 119 | 72 | ad2antrr 726 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℤ) | 
| 120 |  | 0zd 12627 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
ℤ) | 
| 121 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 𝐾 ∈ (0...𝑁)) | 
| 122 |  | nn0uz 12921 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 123 | 102, 122 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
(ℤ≥‘0)) | 
| 124 |  | elfz5 13557 | . . . . . . . . . . 11
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) | 
| 125 | 123, 119,
124 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ≤ 𝑁)) | 
| 126 |  | nn0re 12537 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) | 
| 127 | 126 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℝ) | 
| 128 |  | nnre 12274 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) | 
| 129 | 128 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝐾 ∈
ℝ) | 
| 130 | 127, 129 | subge0d 11854 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (0 ≤
(𝑁 − 𝐾) ↔ 𝐾 ≤ 𝑁)) | 
| 131 | 125, 130 | bitr4d 282 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝐾 ∈ (0...𝑁) ↔ 0 ≤ (𝑁 − 𝐾))) | 
| 132 | 121, 131 | mtbid 324 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬ 0
≤ (𝑁 − 𝐾)) | 
| 133 | 74 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) | 
| 134 | 133 | zred 12724 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ) | 
| 135 |  | 0re 11264 | . . . . . . . . 9
⊢ 0 ∈
ℝ | 
| 136 |  | ltnle 11341 | . . . . . . . . 9
⊢ (((𝑁 − 𝐾) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤
(𝑁 − 𝐾))) | 
| 137 | 134, 135,
136 | sylancl 586 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ¬ 0 ≤ (𝑁 − 𝐾))) | 
| 138 | 132, 137 | mpbird 257 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) < 0) | 
| 139 |  | 0z 12626 | . . . . . . . 8
⊢ 0 ∈
ℤ | 
| 140 |  | zltp1le 12669 | . . . . . . . 8
⊢ (((𝑁 − 𝐾) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) | 
| 141 | 133, 139,
140 | sylancl 586 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) < 0 ↔ ((𝑁 − 𝐾) + 1) ≤ 0)) | 
| 142 | 138, 141 | mpbid 232 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ((𝑁 − 𝐾) + 1) ≤ 0) | 
| 143 |  | nn0ge0 12553 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) | 
| 144 | 143 | ad2antrr 726 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ≤
𝑁) | 
| 145 | 118, 119,
120, 142, 144 | elfzd 13556 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 0 ∈
(((𝑁 − 𝐾) + 1)...𝑁)) | 
| 146 |  | simpll 766 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) | 
| 147 |  | 0cn 11254 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 148 |  | fvi 6984 | . . . . . 6
⊢ (0 ∈
ℂ → ( I ‘0) = 0) | 
| 149 | 147, 148 | mp1i 13 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → ( I
‘0) = 0) | 
| 150 | 108, 113,
115, 117, 145, 146, 149 | seqz 14092 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) = 0) | 
| 151 | 150 | oveq1d 7447 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) →
((seq((𝑁 − 𝐾) + 1)( · , I
)‘𝑁) / (!‘𝐾)) = (0 / (!‘𝐾))) | 
| 152 |  | bcval3 14346 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) | 
| 153 | 20, 152 | syl3an2 1164 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) | 
| 154 | 153 | 3expa 1118 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) | 
| 155 | 107, 151,
154 | 3eqtr4rd 2787 | . 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) | 
| 156 | 100, 155 | pm2.61dan 812 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℕ)
→ (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) |