| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . 6
⊢ (𝑚 = 0 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 0)) | 
| 2 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑚 = 0 → (0...𝑚) = (0...0)) | 
| 3 |  | fz0sn 13668 | . . . . . . . 8
⊢ (0...0) =
{0} | 
| 4 | 2, 3 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑚 = 0 → (0...𝑚) = {0}) | 
| 5 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑚 = 0 → (𝑚C𝑘) = (0C𝑘)) | 
| 6 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 0 → (𝑚 − 𝑘) = (0 − 𝑘)) | 
| 7 | 6 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑚 = 0 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (0 − 𝑘))) | 
| 8 | 7 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑚 = 0 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 9 | 5, 8 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 0 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = 0 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 11 | 4, 10 | sumeq12dv 15743 | . . . . . 6
⊢ (𝑚 = 0 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 12 | 1, 11 | eqeq12d 2752 | . . . . 5
⊢ (𝑚 = 0 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 13 | 12 | imbi2d 340 | . . . 4
⊢ (𝑚 = 0 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 14 |  | oveq2 7440 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑛)) | 
| 15 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (0...𝑚) = (0...𝑛)) | 
| 16 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑚C𝑘) = (𝑛C𝑘)) | 
| 17 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑚 − 𝑘) = (𝑛 − 𝑘)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑛 − 𝑘))) | 
| 19 | 18 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 20 | 16, 19 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 21 | 20 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = 𝑛 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 22 | 15, 21 | sumeq12dv 15743 | . . . . . 6
⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 23 | 14, 22 | eqeq12d 2752 | . . . . 5
⊢ (𝑚 = 𝑛 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 24 | 23 | imbi2d 340 | . . . 4
⊢ (𝑚 = 𝑛 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 25 |  | oveq2 7440 | . . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac (𝑛 + 1))) | 
| 26 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (0...𝑚) = (0...(𝑛 + 1))) | 
| 27 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → (𝑚C𝑘) = ((𝑛 + 1)C𝑘)) | 
| 28 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 𝑘) = ((𝑛 + 1) − 𝑘)) | 
| 29 | 28 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac ((𝑛 + 1) − 𝑘))) | 
| 30 | 29 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 31 | 27, 30 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 32 | 31 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = (𝑛 + 1) ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 33 | 26, 32 | sumeq12dv 15743 | . . . . . 6
⊢ (𝑚 = (𝑛 + 1) → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 34 | 25, 33 | eqeq12d 2752 | . . . . 5
⊢ (𝑚 = (𝑛 + 1) → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 35 | 34 | imbi2d 340 | . . . 4
⊢ (𝑚 = (𝑛 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 36 |  | oveq2 7440 | . . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 + 𝐵) FallFac 𝑚) = ((𝐴 + 𝐵) FallFac 𝑁)) | 
| 37 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑚 = 𝑁 → (0...𝑚) = (0...𝑁)) | 
| 38 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑚 = 𝑁 → (𝑚C𝑘) = (𝑁C𝑘)) | 
| 39 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → (𝑚 − 𝑘) = (𝑁 − 𝑘)) | 
| 40 | 39 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (𝐴 FallFac (𝑚 − 𝑘)) = (𝐴 FallFac (𝑁 − 𝑘))) | 
| 41 | 40 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 42 | 38, 41 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑚 = 𝑁 → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 43 | 42 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = 𝑁 ∧ 𝑘 ∈ (0...𝑚)) → ((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 44 | 37, 43 | sumeq12dv 15743 | . . . . . 6
⊢ (𝑚 = 𝑁 → Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 45 | 36, 44 | eqeq12d 2752 | . . . . 5
⊢ (𝑚 = 𝑁 → (((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘))) ↔ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 46 | 45 | imbi2d 340 | . . . 4
⊢ (𝑚 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑚) = Σ𝑘 ∈ (0...𝑚)((𝑚C𝑘) · ((𝐴 FallFac (𝑚 − 𝑘)) · (𝐵 FallFac 𝑘)))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 47 |  | fallfac0 16065 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 0) =
1) | 
| 48 |  | fallfac0 16065 | . . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵 FallFac 0) =
1) | 
| 49 | 47, 48 | oveqan12d 7451 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) = (1 ·
1)) | 
| 50 |  | 1t1e1 12429 | . . . . . . . 8
⊢ (1
· 1) = 1 | 
| 51 | 49, 50 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 FallFac 0) · (𝐵 FallFac 0)) =
1) | 
| 52 | 51 | oveq2d 7448 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0))) =
(1 · 1)) | 
| 53 | 52, 50 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0))) =
1) | 
| 54 |  | 0cn 11254 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 55 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 56 | 53, 55 | eqeltrdi 2848 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴 FallFac 0)
· (𝐵 FallFac 0)))
∈ ℂ) | 
| 57 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑘 = 0 → (0C𝑘) = (0C0)) | 
| 58 |  | 0nn0 12543 | . . . . . . . . . 10
⊢ 0 ∈
ℕ0 | 
| 59 |  | bcnn 14352 | . . . . . . . . . 10
⊢ (0 ∈
ℕ0 → (0C0) = 1) | 
| 60 | 58, 59 | ax-mp 5 | . . . . . . . . 9
⊢ (0C0) =
1 | 
| 61 | 57, 60 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑘 = 0 → (0C𝑘) = 1) | 
| 62 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → (0 − 𝑘) = (0 −
0)) | 
| 63 |  | 0m0e0 12387 | . . . . . . . . . . 11
⊢ (0
− 0) = 0 | 
| 64 | 62, 63 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (0 − 𝑘) = 0) | 
| 65 | 64 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑘 = 0 → (𝐴 FallFac (0 − 𝑘)) = (𝐴 FallFac 0)) | 
| 66 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑘 = 0 → (𝐵 FallFac 𝑘) = (𝐵 FallFac 0)) | 
| 67 | 65, 66 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = 0 → ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac 0) · (𝐵 FallFac 0))) | 
| 68 | 61, 67 | oveq12d 7450 | . . . . . . 7
⊢ (𝑘 = 0 → ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) | 
| 69 | 68 | sumsn 15783 | . . . . . 6
⊢ ((0
∈ ℂ ∧ (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0))) ∈ ℂ) →
Σ𝑘 ∈ {0}
((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) | 
| 70 | 54, 56, 69 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
Σ𝑘 ∈ {0}
((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘))) = (1 · ((𝐴 FallFac 0) · (𝐵 FallFac 0)))) | 
| 71 |  | addcl 11238 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | 
| 72 |  | fallfac0 16065 | . . . . . 6
⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵) FallFac 0) = 1) | 
| 73 | 71, 72 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = 1) | 
| 74 | 53, 70, 73 | 3eqtr4rd 2787 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac 0) = Σ𝑘 ∈ {0} ((0C𝑘) · ((𝐴 FallFac (0 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 75 |  | simprl 770 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝐴 ∈
ℂ) | 
| 76 |  | simprr 772 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝐵 ∈
ℂ) | 
| 77 |  | simpl 482 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
→ 𝑛 ∈
ℕ0) | 
| 78 |  | id 22 | . . . . . . 7
⊢ (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 79 | 75, 76, 77, 78 | binomfallfaclem2 16077 | . . . . . 6
⊢ (((𝑛 ∈ ℕ0
∧ (𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ))
∧ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 80 | 79 | exp31 419 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ (((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘))) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 81 | 80 | a2d 29 | . . . 4
⊢ (𝑛 ∈ ℕ0
→ (((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 + 𝐵) FallFac 𝑛) = Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((𝐴 FallFac (𝑛 − 𝑘)) · (𝐵 FallFac 𝑘)))) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) FallFac (𝑛 + 1)) = Σ𝑘 ∈ (0...(𝑛 + 1))(((𝑛 + 1)C𝑘) · ((𝐴 FallFac ((𝑛 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))))) | 
| 82 | 13, 24, 35, 46, 74, 81 | nn0ind 12715 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 83 | 82 | com12 32 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 ∈ ℕ0
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 84 | 83 | 3impia 1117 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) |