Proof of Theorem binomrisefac
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negdi 11567 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | 
| 2 | 1 | 3adant3 1132 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | 
| 3 | 2 | oveq1d 7447 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 + 𝐵) FallFac 𝑁) = ((-𝐴 + -𝐵) FallFac 𝑁)) | 
| 4 |  | negcl 11509 | . . . . . 6
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) | 
| 5 |  | negcl 11509 | . . . . . 6
⊢ (𝐵 ∈ ℂ → -𝐵 ∈
ℂ) | 
| 6 |  | id 22 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) | 
| 7 |  | binomfallfac 16078 | . . . . . 6
⊢ ((-𝐴 ∈ ℂ ∧ -𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((-𝐴 + -𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 8 | 4, 5, 6, 7 | syl3an 1160 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((-𝐴 + -𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 9 | 3, 8 | eqtrd 2776 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 10 | 9 | oveq2d 7448 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((-1↑𝑁)
· (-(𝐴 + 𝐵) FallFac 𝑁)) = ((-1↑𝑁) · Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 11 |  | fzfid 14015 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...𝑁) ∈
Fin) | 
| 12 |  | neg1cn 12381 | . . . . . 6
⊢ -1 ∈
ℂ | 
| 13 |  | expcl 14121 | . . . . . 6
⊢ ((-1
∈ ℂ ∧ 𝑁
∈ ℕ0) → (-1↑𝑁) ∈ ℂ) | 
| 14 | 12, 13 | mpan 690 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (-1↑𝑁) ∈
ℂ) | 
| 15 | 14 | 3ad2ant3 1135 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (-1↑𝑁) ∈
ℂ) | 
| 16 |  | simp3 1138 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) | 
| 17 |  | elfzelz 13565 | . . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) | 
| 18 |  | bccl 14362 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) | 
| 19 | 16, 17, 18 | syl2an 596 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) | 
| 20 | 19 | nn0cnd 12591 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) | 
| 21 |  | simpl1 1191 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) | 
| 22 | 21 | negcld 11608 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → -𝐴 ∈ ℂ) | 
| 23 | 16 | nn0zd 12641 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) | 
| 24 |  | zsubcl 12661 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑁 − 𝑘) ∈ ℤ) | 
| 25 | 23, 17, 24 | syl2an 596 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈ ℤ) | 
| 26 |  | elfzle2 13569 | . . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ≤ 𝑁) | 
| 27 | 26 | adantl 481 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ≤ 𝑁) | 
| 28 |  | simpl3 1193 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈
ℕ0) | 
| 29 | 28 | nn0red 12590 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) | 
| 30 |  | elfznn0 13661 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 32 | 31 | nn0red 12590 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℝ) | 
| 33 | 29, 32 | subge0d 11854 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (0 ≤ (𝑁 − 𝑘) ↔ 𝑘 ≤ 𝑁)) | 
| 34 | 27, 33 | mpbird 257 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 0 ≤ (𝑁 − 𝑘)) | 
| 35 |  | elnn0z 12628 | . . . . . . . 8
⊢ ((𝑁 − 𝑘) ∈ ℕ0 ↔ ((𝑁 − 𝑘) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑘))) | 
| 36 | 25, 34, 35 | sylanbrc 583 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) | 
| 37 |  | fallfaccl 16053 | . . . . . . 7
⊢ ((-𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (-𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) | 
| 38 | 22, 36, 37 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) | 
| 39 |  | simp2 1137 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℂ) | 
| 40 | 39 | negcld 11608 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ -𝐵 ∈
ℂ) | 
| 41 |  | fallfaccl 16053 | . . . . . . 7
⊢ ((-𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (-𝐵 FallFac 𝑘) ∈
ℂ) | 
| 42 | 40, 30, 41 | syl2an 596 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-𝐵 FallFac 𝑘) ∈ ℂ) | 
| 43 | 38, 42 | mulcld 11282 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)) ∈ ℂ) | 
| 44 | 20, 43 | mulcld 11282 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 45 | 11, 15, 44 | fsummulc2 15821 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((-1↑𝑁)
· Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 46 | 10, 45 | eqtrd 2776 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((-1↑𝑁)
· (-(𝐴 + 𝐵) FallFac 𝑁)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 47 |  | addcl 11238 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | 
| 48 |  | risefallfac 16061 | . . 3
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵) RiseFac 𝑁) = ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁))) | 
| 49 | 47, 48 | stoic3 1775 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 𝐵) RiseFac 𝑁) = ((-1↑𝑁) · (-(𝐴 + 𝐵) FallFac 𝑁))) | 
| 50 |  | risefallfac 16061 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (𝐴 RiseFac (𝑁 − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘)))) | 
| 51 | 21, 36, 50 | syl2anc 584 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝐴 RiseFac (𝑁 − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘)))) | 
| 52 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ ℂ) | 
| 53 |  | risefallfac 16061 | . . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵 RiseFac 𝑘) = ((-1↑𝑘) · (-𝐵 FallFac 𝑘))) | 
| 54 | 52, 31, 53 | syl2anc 584 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝐵 RiseFac 𝑘) = ((-1↑𝑘) · (-𝐵 FallFac 𝑘))) | 
| 55 | 51, 54 | oveq12d 7450 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘)) = (((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))) · ((-1↑𝑘) · (-𝐵 FallFac 𝑘)))) | 
| 56 |  | expcl 14121 | . . . . . . . 8
⊢ ((-1
∈ ℂ ∧ (𝑁
− 𝑘) ∈
ℕ0) → (-1↑(𝑁 − 𝑘)) ∈ ℂ) | 
| 57 | 12, 36, 56 | sylancr 587 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑘)) ∈ ℂ) | 
| 58 |  | expcl 14121 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑘
∈ ℕ0) → (-1↑𝑘) ∈ ℂ) | 
| 59 | 12, 30, 58 | sylancr 587 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ) | 
| 60 | 59 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈
ℂ) | 
| 61 | 57, 38, 60, 42 | mul4d 11474 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (((-1↑(𝑁 − 𝑘)) · (-𝐴 FallFac (𝑁 − 𝑘))) · ((-1↑𝑘) · (-𝐵 FallFac 𝑘))) = (((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 62 | 12 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → -1 ∈
ℂ) | 
| 63 | 62, 31, 36 | expaddd 14189 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-1↑((𝑁 − 𝑘) + 𝑘)) = ((-1↑(𝑁 − 𝑘)) · (-1↑𝑘))) | 
| 64 | 16 | nn0cnd 12591 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) | 
| 65 | 30 | nn0cnd 12591 | . . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) | 
| 66 |  | npcan 11518 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑁 − 𝑘) + 𝑘) = 𝑁) | 
| 67 | 64, 65, 66 | syl2an 596 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 𝑘) + 𝑘) = 𝑁) | 
| 68 | 67 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-1↑((𝑁 − 𝑘) + 𝑘)) = (-1↑𝑁)) | 
| 69 | 63, 68 | eqtr3d 2778 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) = (-1↑𝑁)) | 
| 70 | 69 | oveq1d 7447 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (((-1↑(𝑁 − 𝑘)) · (-1↑𝑘)) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))) = ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 71 | 55, 61, 70 | 3eqtrd 2780 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘)) = ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) | 
| 72 | 71 | oveq2d 7448 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = ((𝑁C𝑘) · ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 73 | 15 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑁) ∈
ℂ) | 
| 74 | 20, 73, 43 | mul12d 11471 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-1↑𝑁) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘)))) = ((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 75 | 72, 74 | eqtrd 2776 | . . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = ((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 76 | 75 | sumeq2dv 15739 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑁) · ((𝑁C𝑘) · ((-𝐴 FallFac (𝑁 − 𝑘)) · (-𝐵 FallFac 𝑘))))) | 
| 77 | 46, 49, 76 | 3eqtr4d 2786 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 𝐵) RiseFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘)))) |