| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | binomfallfaclem.3 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | elfzelz 13565 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) | 
| 3 |  | bccl 14362 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) | 
| 5 | 4 | nn0cnd 12591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) | 
| 6 |  | binomfallfaclem.1 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 7 |  | fznn0sub 13597 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) | 
| 8 |  | fallfaccl 16053 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) | 
| 9 | 6, 7, 8 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac (𝑁 − 𝑘)) ∈ ℂ) | 
| 10 |  | binomfallfaclem.2 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 11 |  | elfznn0 13661 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 12 |  | fallfaccl 16053 | . . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵 FallFac 𝑘) ∈
ℂ) | 
| 13 | 10, 11, 12 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac 𝑘) ∈ ℂ) | 
| 14 | 9, 13 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) | 
| 15 | 6, 10 | addcld 11281 | . . . . . . . 8
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) | 
| 16 | 1 | nn0cnd 12591 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 17 | 15, 16 | subcld 11621 | . . . . . . 7
⊢ (𝜑 → ((𝐴 + 𝐵) − 𝑁) ∈ ℂ) | 
| 18 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 + 𝐵) − 𝑁) ∈ ℂ) | 
| 19 | 5, 14, 18 | mulassd 11285 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = ((𝑁C𝑘) · (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁)))) | 
| 20 | 7 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈ ℂ) | 
| 21 |  | subcl 11508 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℂ) → (𝐴 − (𝑁 − 𝑘)) ∈ ℂ) | 
| 22 | 6, 20, 21 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − (𝑁 − 𝑘)) ∈ ℂ) | 
| 23 | 11 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) | 
| 24 |  | subcl 11508 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐵 − 𝑘) ∈ ℂ) | 
| 25 | 10, 23, 24 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 − 𝑘) ∈ ℂ) | 
| 26 | 14, 22, 25 | adddid 11286 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘))) = ((((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) + (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)))) | 
| 27 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) | 
| 28 | 16 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℂ) | 
| 29 | 27, 28 | subcld 11621 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − 𝑁) ∈ ℂ) | 
| 30 | 23 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) | 
| 31 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ ℂ) | 
| 32 | 29, 30, 31 | ppncand 11661 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 − 𝑁) + 𝑘) + (𝐵 − 𝑘)) = ((𝐴 − 𝑁) + 𝐵)) | 
| 33 | 27, 28, 30 | subsubd 11649 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 − (𝑁 − 𝑘)) = ((𝐴 − 𝑁) + 𝑘)) | 
| 34 | 33 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘)) = (((𝐴 − 𝑁) + 𝑘) + (𝐵 − 𝑘))) | 
| 35 | 27, 31, 28 | addsubd 11642 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 + 𝐵) − 𝑁) = ((𝐴 − 𝑁) + 𝐵)) | 
| 36 | 32, 34, 35 | 3eqtr4d 2786 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘)) = ((𝐴 + 𝐵) − 𝑁)) | 
| 37 | 36 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 − (𝑁 − 𝑘)) + (𝐵 − 𝑘))) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁))) | 
| 38 | 9, 13, 22 | mul32d 11472 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘))) · (𝐵 FallFac 𝑘))) | 
| 39 |  | 1cnd 11257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) | 
| 40 | 28, 39, 30 | addsubd 11642 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) | 
| 41 | 40 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 − 𝑘) + 1))) | 
| 42 |  | fallfacp1 16067 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ0) → (𝐴 FallFac ((𝑁 − 𝑘) + 1)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) | 
| 43 | 6, 7, 42 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 − 𝑘) + 1)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) | 
| 44 | 41, 43 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘)))) | 
| 45 | 44 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐴 − (𝑁 − 𝑘))) · (𝐵 FallFac 𝑘))) | 
| 46 | 38, 45 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) = ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 47 | 9, 13, 25 | mulassd 11285 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘)))) | 
| 48 |  | fallfacp1 16067 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐵 FallFac (𝑘 + 1)) = ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘))) | 
| 49 | 10, 11, 48 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac (𝑘 + 1)) = ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘))) | 
| 50 | 49 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) = ((𝐴 FallFac (𝑁 − 𝑘)) · ((𝐵 FallFac 𝑘) · (𝐵 − 𝑘)))) | 
| 51 | 47, 50 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘)) = ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) | 
| 52 | 46, 51 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐴 − (𝑁 − 𝑘))) + (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · (𝐵 − 𝑘))) = (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) | 
| 53 | 26, 37, 52 | 3eqtr3d 2784 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁)) = (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) | 
| 54 | 53 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)) · ((𝐴 + 𝐵) − 𝑁))) = ((𝑁C𝑘) · (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 55 | 1 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 56 |  | uzid 12894 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) | 
| 57 |  | peano2uz 12944 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) | 
| 58 |  | fzss2 13605 | . . . . . . . . . 10
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(𝑁 + 1))) | 
| 59 | 55, 56, 57, 58 | 4syl 19 | . . . . . . . . 9
⊢ (𝜑 → (0...𝑁) ⊆ (0...(𝑁 + 1))) | 
| 60 | 59 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...(𝑁 + 1))) | 
| 61 |  | fznn0sub 13597 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈
ℕ0) | 
| 62 |  | fallfaccl 16053 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) | 
| 63 | 6, 61, 62 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) | 
| 64 | 60, 63 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) ∈ ℂ) | 
| 65 | 64, 13 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) | 
| 66 |  | peano2nn0 12568 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 67 | 11, 66 | syl 17 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 + 1) ∈
ℕ0) | 
| 68 |  | fallfaccl 16053 | . . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐵 FallFac (𝑘 + 1)) ∈ ℂ) | 
| 69 | 10, 67, 68 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵 FallFac (𝑘 + 1)) ∈ ℂ) | 
| 70 | 9, 69 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) ∈ ℂ) | 
| 71 | 5, 65, 70 | adddid 11286 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) + ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 72 | 19, 54, 71 | 3eqtrd 2780 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 73 | 72 | sumeq2dv 15739 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 74 | 73 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 75 | 15, 1 | fallfacp1d 16069 | . . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = (((𝐴 + 𝐵) FallFac 𝑁) · ((𝐴 + 𝐵) − 𝑁))) | 
| 76 |  | binomfallfaclem.4 | . . . . 5
⊢ (𝜓 → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 77 | 76 | oveq1d 7447 | . . . 4
⊢ (𝜓 → (((𝐴 + 𝐵) FallFac 𝑁) · ((𝐴 + 𝐵) − 𝑁)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) | 
| 78 | 75, 77 | sylan9eq 2796 | . . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) | 
| 79 |  | fzfid 14015 | . . . . 5
⊢ (𝜑 → (0...𝑁) ∈ Fin) | 
| 80 | 5, 14 | mulcld 11282 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 81 | 79, 17, 80 | fsummulc1 15822 | . . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) | 
| 82 | 81 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝜓) → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) | 
| 83 | 78, 82 | eqtrd 2776 | . 2
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))) · ((𝐴 + 𝐵) − 𝑁))) | 
| 84 |  | elfzelz 13565 | . . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) | 
| 85 |  | bcpasc 14361 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) | 
| 86 | 1, 84, 85 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) | 
| 87 | 86 | oveq1d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 88 | 1, 84, 3 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) | 
| 89 | 88 | nn0cnd 12591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℂ) | 
| 90 |  | peano2zm 12662 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) | 
| 91 | 84, 90 | syl 17 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) | 
| 92 |  | bccl 14362 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) | 
| 93 | 1, 91, 92 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) | 
| 94 | 93 | nn0cnd 12591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ) | 
| 95 |  | elfznn0 13661 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) | 
| 96 | 10, 95, 12 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐵 FallFac 𝑘) ∈ ℂ) | 
| 97 | 63, 96 | mulcld 11282 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) ∈ ℂ) | 
| 98 | 89, 94, 97 | adddird 11287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 99 | 87, 98 | eqtr3d 2778 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 100 | 99 | sumeq2dv 15739 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 101 |  | nn0uz 12921 | . . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) | 
| 102 | 1, 101 | eleqtrdi 2850 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 103 | 89, 97 | mulcld 11282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 104 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) | 
| 105 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑁 + 1) → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − (𝑁 + 1))) | 
| 106 | 105 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1)))) | 
| 107 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑘 = (𝑁 + 1) → (𝐵 FallFac 𝑘) = (𝐵 FallFac (𝑁 + 1))) | 
| 108 | 106, 107 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) | 
| 109 | 104, 108 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) | 
| 110 | 102, 103,
109 | fsump1 15793 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))))) | 
| 111 |  | peano2nn0 12568 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 112 | 1, 111 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) | 
| 113 | 112 | nn0zd 12641 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) | 
| 114 | 1 | nn0red 12590 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 115 | 114 | ltp1d 12199 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) | 
| 116 | 115 | olcd 874 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) | 
| 117 |  | bcval4 14347 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ ∧ ((𝑁 + 1) <
0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0) | 
| 118 | 1, 113, 116, 117 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) | 
| 119 | 118 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = (0 · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) | 
| 120 | 112 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) | 
| 121 | 120 | subidd 11609 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) − (𝑁 + 1)) = 0) | 
| 122 | 121 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) = (𝐴 FallFac 0)) | 
| 123 |  | 0nn0 12543 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 124 |  | fallfaccl 16053 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝐴 FallFac 0) ∈ ℂ) | 
| 125 | 6, 123, 124 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac 0) ∈ ℂ) | 
| 126 | 122, 125 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) ∈ ℂ) | 
| 127 |  | fallfaccl 16053 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ (𝑁 + 1) ∈
ℕ0) → (𝐵 FallFac (𝑁 + 1)) ∈ ℂ) | 
| 128 | 10, 112, 127 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 FallFac (𝑁 + 1)) ∈ ℂ) | 
| 129 | 126, 128 | mulcld 11282 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))) ∈ ℂ) | 
| 130 | 129 | mul02d 11460 | . . . . . . . . 9
⊢ (𝜑 → (0 · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = 0) | 
| 131 | 119, 130 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1)))) = 0) | 
| 132 | 131 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑁 + 1)) · ((𝐴 FallFac ((𝑁 + 1) − (𝑁 + 1))) · (𝐵 FallFac (𝑁 + 1))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + 0)) | 
| 133 | 60, 103 | syldan 591 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 134 | 79, 133 | fsumcl 15770 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 135 | 134 | addridd 11462 | . . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + 0) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 136 | 110, 132,
135 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 137 | 112, 101 | eleqtrdi 2850 | . . . . . . . 8
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) | 
| 138 | 94, 97 | mulcld 11282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) ∈ ℂ) | 
| 139 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) | 
| 140 |  | df-neg 11496 | . . . . . . . . . . 11
⊢ -1 = (0
− 1) | 
| 141 | 139, 140 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑘 − 1) = -1) | 
| 142 | 141 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C-1)) | 
| 143 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0)) | 
| 144 | 143 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐴 FallFac ((𝑁 + 1) − 𝑘)) = (𝐴 FallFac ((𝑁 + 1) − 0))) | 
| 145 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝐵 FallFac 𝑘) = (𝐵 FallFac 0)) | 
| 146 | 144, 145 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑘 = 0 → ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)) = ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) | 
| 147 | 142, 146 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0)))) | 
| 148 | 137, 138,
147 | fsum1p 15790 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = (((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 149 |  | neg1z 12655 | . . . . . . . . . . . 12
⊢ -1 ∈
ℤ | 
| 150 |  | neg1lt0 12384 | . . . . . . . . . . . . 13
⊢ -1 <
0 | 
| 151 | 150 | orci 865 | . . . . . . . . . . . 12
⊢ (-1 <
0 ∨ 𝑁 <
-1) | 
| 152 |  | bcval4 14347 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ -1 ∈ ℤ ∧ (-1 < 0 ∨ 𝑁 < -1)) → (𝑁C-1) = 0) | 
| 153 | 149, 151,
152 | mp3an23 1454 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁C-1) =
0) | 
| 154 | 1, 153 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁C-1) = 0) | 
| 155 | 154 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) = (0 ·
((𝐴 FallFac ((𝑁 + 1) − 0)) ·
(𝐵 FallFac
0)))) | 
| 156 | 120 | subid1d 11610 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) − 0) = (𝑁 + 1)) | 
| 157 | 156 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − 0)) = (𝐴 FallFac (𝑁 + 1))) | 
| 158 |  | fallfaccl 16053 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 + 1) ∈
ℕ0) → (𝐴 FallFac (𝑁 + 1)) ∈ ℂ) | 
| 159 | 6, 112, 158 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 FallFac (𝑁 + 1)) ∈ ℂ) | 
| 160 | 157, 159 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 FallFac ((𝑁 + 1) − 0)) ∈
ℂ) | 
| 161 |  | fallfaccl 16053 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝐵 FallFac 0) ∈ ℂ) | 
| 162 | 10, 123, 161 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 FallFac 0) ∈ ℂ) | 
| 163 | 160, 162 | mulcld 11282 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0)) ∈
ℂ) | 
| 164 | 163 | mul02d 11460 | . . . . . . . . 9
⊢ (𝜑 → (0 · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) =
0) | 
| 165 | 155, 164 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → ((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) =
0) | 
| 166 |  | 1zzd 12650 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) | 
| 167 |  | 0zd 12627 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) | 
| 168 | 6, 10, 1 | binomfallfaclem1 16076 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) ∈ ℂ) | 
| 169 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑗 = (𝑘 − 1) → (𝑁C𝑗) = (𝑁C(𝑘 − 1))) | 
| 170 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑘 − 1) → (𝑁 − 𝑗) = (𝑁 − (𝑘 − 1))) | 
| 171 | 170 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 − 1) → (𝐴 FallFac (𝑁 − 𝑗)) = (𝐴 FallFac (𝑁 − (𝑘 − 1)))) | 
| 172 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑘 − 1) → (𝑗 + 1) = ((𝑘 − 1) + 1)) | 
| 173 | 172 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 − 1) → (𝐵 FallFac (𝑗 + 1)) = (𝐵 FallFac ((𝑘 − 1) + 1))) | 
| 174 | 171, 173 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑗 = (𝑘 − 1) → ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))) = ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) | 
| 175 | 169, 174 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑗 = (𝑘 − 1) → ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))))) | 
| 176 | 166, 167,
55, 168, 175 | fsumshft 15817 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))))) | 
| 177 | 16 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ) | 
| 178 |  | elfzelz 13565 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℤ) | 
| 179 | 178 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℤ) | 
| 180 | 179 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℂ) | 
| 181 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) | 
| 182 | 177, 180,
181 | subsub3d 11651 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 + 1) − 𝑘)) | 
| 183 | 182 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐴 FallFac (𝑁 − (𝑘 − 1))) = (𝐴 FallFac ((𝑁 + 1) − 𝑘))) | 
| 184 | 180, 181 | npcand 11625 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑘 − 1) + 1) = 𝑘) | 
| 185 | 184 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐵 FallFac ((𝑘 − 1) + 1)) = (𝐵 FallFac 𝑘)) | 
| 186 | 183, 185 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1))) = ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) | 
| 187 | 186 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 188 | 187 | sumeq2dv 15739 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac (𝑁 − (𝑘 − 1))) · (𝐵 FallFac ((𝑘 − 1) + 1)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) | 
| 189 | 176, 188 | eqtr2d 2777 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))))) | 
| 190 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝑁C𝑘) = (𝑁C𝑗)) | 
| 191 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑁 − 𝑘) = (𝑁 − 𝑗)) | 
| 192 | 191 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐴 FallFac (𝑁 − 𝑘)) = (𝐴 FallFac (𝑁 − 𝑗))) | 
| 193 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1)) | 
| 194 | 193 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝐵 FallFac (𝑘 + 1)) = (𝐵 FallFac (𝑗 + 1))) | 
| 195 | 192, 194 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))) = ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) | 
| 196 | 190, 195 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) = ((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1))))) | 
| 197 | 196 | cbvsumv 15733 | . . . . . . . . 9
⊢
Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) = Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((𝐴 FallFac (𝑁 − 𝑗)) · (𝐵 FallFac (𝑗 + 1)))) | 
| 198 | 189, 197 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) | 
| 199 | 165, 198 | oveq12d 7450 | . . . . . . 7
⊢ (𝜑 → (((𝑁C-1) · ((𝐴 FallFac ((𝑁 + 1) − 0)) · (𝐵 FallFac 0))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (0 + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 200 | 6, 10, 1 | binomfallfaclem1 16076 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) ∈ ℂ) | 
| 201 | 79, 200 | fsumcl 15770 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))) ∈ ℂ) | 
| 202 | 201 | addlidd 11463 | . . . . . . 7
⊢ (𝜑 → (0 + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) | 
| 203 | 148, 199,
202 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) | 
| 204 | 136, 203 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 205 |  | fzfid 14015 | . . . . . 6
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) | 
| 206 | 205, 103,
138 | fsumadd 15777 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))) | 
| 207 | 79, 133, 200 | fsumadd 15777 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 208 | 204, 206,
207 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 209 | 100, 208 | eqtrd 2776 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 210 | 209 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))) + ((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac (𝑘 + 1)))))) | 
| 211 | 74, 83, 210 | 3eqtr4d 2786 | 1
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘)))) |