| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | binomcxp.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 2 | 1 | rpcnd 13079 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 3 |  | binomcxp.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 4 | 3 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 5 |  | binom 15866 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0)
→ ((𝐴 + 𝐵)↑𝐶) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 6 | 5 | 3expia 1122 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 ∈ ℕ0
→ ((𝐴 + 𝐵)↑𝐶) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘))))) | 
| 7 | 2, 4, 6 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐶 ∈ ℕ0 → ((𝐴 + 𝐵)↑𝐶) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘))))) | 
| 8 | 7 | imp 406 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝐶) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 9 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 10 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 11 | 9, 10 | addcld 11280 | . . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℂ) | 
| 12 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 𝐶 ∈
ℕ0) | 
| 13 |  | cxpexp 26710 | . . . . . 6
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = ((𝐴 + 𝐵)↑𝐶)) | 
| 14 | 11, 12, 13 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = ((𝐴 + 𝐵)↑𝐶)) | 
| 15 |  | elfznn0 13660 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝐶) → 𝑘 ∈ ℕ0) | 
| 16 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐶 ∈
ℕ0) | 
| 17 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) | 
| 18 | 16, 17 | bccbc 44364 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐶C𝑐𝑘) = (𝐶C𝑘)) | 
| 19 | 15, 18 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → (𝐶C𝑐𝑘) = (𝐶C𝑘)) | 
| 20 | 2 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → 𝐴 ∈ ℂ) | 
| 21 |  | elfzle2 13568 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝐶) → 𝑘 ≤ 𝐶) | 
| 22 | 21 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → 𝑘 ≤ 𝐶) | 
| 23 |  | nn0sub 12576 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (𝑘 ≤ 𝐶 ↔ (𝐶 − 𝑘) ∈
ℕ0)) | 
| 24 | 23 | ancoms 458 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑘 ≤ 𝐶 ↔ (𝐶 − 𝑘) ∈
ℕ0)) | 
| 25 | 24 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ 𝐶 ↔ (𝐶 − 𝑘) ∈
ℕ0)) | 
| 26 | 15, 25 | sylan2 593 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → (𝑘 ≤ 𝐶 ↔ (𝐶 − 𝑘) ∈
ℕ0)) | 
| 27 | 22, 26 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → (𝐶 − 𝑘) ∈
ℕ0) | 
| 28 |  | cxpexp 26710 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝐶 − 𝑘) ∈ ℕ0) → (𝐴↑𝑐(𝐶 − 𝑘)) = (𝐴↑(𝐶 − 𝑘))) | 
| 29 | 20, 27, 28 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → (𝐴↑𝑐(𝐶 − 𝑘)) = (𝐴↑(𝐶 − 𝑘))) | 
| 30 | 29 | oveq1d 7446 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)) = ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘))) | 
| 31 | 19, 30 | oveq12d 7449 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝐶)) → ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = ((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 32 | 31 | sumeq2dv 15738 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑘) · ((𝐴↑(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 33 | 8, 14, 32 | 3eqtr4d 2787 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 34 |  | binomcxp.c | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 35 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 𝐶 ∈
ℂ) | 
| 36 | 11, 35 | cxpcld 26750 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) ∈ ℂ) | 
| 37 | 33, 36 | eqeltrrd 2842 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ) | 
| 38 | 37 | addridd 11461 | . 2
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + 0) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 39 |  | nn0uz 12920 | . . . 4
⊢
ℕ0 = (ℤ≥‘0) | 
| 40 |  | eqid 2737 | . . . 4
⊢
(ℤ≥‘(𝐶 + 1)) =
(ℤ≥‘(𝐶 + 1)) | 
| 41 |  | 1nn0 12542 | . . . . . 6
⊢ 1 ∈
ℕ0 | 
| 42 | 41 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 1 ∈
ℕ0) | 
| 43 | 12, 42 | nn0addcld 12591 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → (𝐶 + 1) ∈
ℕ0) | 
| 44 |  | eqidd 2738 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑗 ∈
ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗)))) = (𝑗 ∈ ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))) | 
| 45 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) | 
| 46 | 45 | oveq2d 7447 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → (𝐶C𝑐𝑗) = (𝐶C𝑐𝑘)) | 
| 47 | 45 | oveq2d 7447 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → (𝐶 − 𝑗) = (𝐶 − 𝑘)) | 
| 48 | 47 | oveq2d 7447 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → (𝐴↑𝑐(𝐶 − 𝑗)) = (𝐴↑𝑐(𝐶 − 𝑘))) | 
| 49 | 45 | oveq2d 7447 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → (𝐵↑𝑗) = (𝐵↑𝑘)) | 
| 50 | 48, 49 | oveq12d 7449 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗)) = ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) | 
| 51 | 46, 50 | oveq12d 7449 | . . . . 5
⊢ ((((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑗 = 𝑘) → ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))) = ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 52 | 34 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐶 ∈
ℂ) | 
| 53 | 52, 17 | bcccl 44358 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐶C𝑐𝑘) ∈ ℂ) | 
| 54 | 2 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
ℂ) | 
| 55 | 17 | nn0cnd 12589 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) | 
| 56 | 52, 55 | subcld 11620 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐶 − 𝑘) ∈
ℂ) | 
| 57 | 54, 56 | cxpcld 26750 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑐(𝐶 − 𝑘)) ∈ ℂ) | 
| 58 | 4 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐵 ∈
ℂ) | 
| 59 | 58, 17 | expcld 14186 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐵↑𝑘) ∈
ℂ) | 
| 60 | 57, 59 | mulcld 11281 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)) ∈ ℂ) | 
| 61 | 53, 60 | mulcld 11281 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ) | 
| 62 | 44, 51, 17, 61 | fvmptd 7023 | . . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑗 ∈
ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘) = ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 63 |  | peano2nn0 12566 | . . . . . 6
⊢ (𝐶 ∈ ℕ0
→ (𝐶 + 1) ∈
ℕ0) | 
| 64 | 63 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → (𝐶 + 1) ∈
ℕ0) | 
| 65 |  | c0ex 11255 | . . . . . . . . 9
⊢ 0 ∈
V | 
| 66 | 65 | fconst 6794 | . . . . . . . 8
⊢
(ℕ0 ×
{0}):ℕ0⟶{0} | 
| 67 | 66 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(ℕ0 ×
{0}):ℕ0⟶{0}) | 
| 68 |  | 0red 11264 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 0 ∈
ℝ) | 
| 69 | 68 | snssd 4809 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → {0}
⊆ ℝ) | 
| 70 | 67, 69 | fssd 6753 | . . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(ℕ0 ×
{0}):ℕ0⟶ℝ) | 
| 71 | 70 | ffvelcdmda 7104 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((ℕ0 × {0})‘𝑘) ∈ ℝ) | 
| 72 | 62, 61 | eqeltrd 2841 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑗 ∈
ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘) ∈ ℂ) | 
| 73 |  | climrel 15528 | . . . . . . 7
⊢ Rel
⇝ | 
| 74 | 39 | xpeq1i 5711 | . . . . . . . . 9
⊢
(ℕ0 × {0}) = ((ℤ≥‘0)
× {0}) | 
| 75 |  | seqeq3 14047 | . . . . . . . . 9
⊢
((ℕ0 × {0}) = ((ℤ≥‘0)
× {0}) → seq0( + , (ℕ0 × {0})) = seq0( + ,
((ℤ≥‘0) × {0}))) | 
| 76 | 74, 75 | ax-mp 5 | . . . . . . . 8
⊢ seq0( + ,
(ℕ0 × {0})) = seq0( + ,
((ℤ≥‘0) × {0})) | 
| 77 |  | 0z 12624 | . . . . . . . . 9
⊢ 0 ∈
ℤ | 
| 78 |  | serclim0 15613 | . . . . . . . . 9
⊢ (0 ∈
ℤ → seq0( + , ((ℤ≥‘0) × {0}))
⇝ 0) | 
| 79 | 77, 78 | ax-mp 5 | . . . . . . . 8
⊢ seq0( + ,
((ℤ≥‘0) × {0})) ⇝ 0 | 
| 80 | 76, 79 | eqbrtri 5164 | . . . . . . 7
⊢ seq0( + ,
(ℕ0 × {0})) ⇝ 0 | 
| 81 |  | releldm 5955 | . . . . . . 7
⊢ ((Rel
⇝ ∧ seq0( + , (ℕ0 × {0})) ⇝ 0) →
seq0( + , (ℕ0 × {0})) ∈ dom ⇝
) | 
| 82 | 73, 80, 81 | mp2an 692 | . . . . . 6
⊢ seq0( + ,
(ℕ0 × {0})) ∈ dom ⇝ | 
| 83 | 82 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → seq0( +
, (ℕ0 × {0})) ∈ dom ⇝ ) | 
| 84 |  | eluznn0 12959 | . . . . . . . . . . . 12
⊢ (((𝐶 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝑘 ∈ ℕ0) | 
| 85 | 64, 84 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝑘 ∈ ℕ0) | 
| 86 | 85, 62 | syldan 591 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝑗 ∈ ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘) = ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 87 |  | 0zd 12625 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 0 ∈
ℤ) | 
| 88 | 85 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝑘 ∈ ℤ) | 
| 89 |  | 1zzd 12648 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 1 ∈
ℤ) | 
| 90 | 88, 89 | zsubcld 12727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝑘 − 1) ∈ ℤ) | 
| 91 | 12 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 𝐶 ∈
ℤ) | 
| 92 | 91 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐶 ∈ ℤ) | 
| 93 | 12 | nn0ge0d 12590 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 0 ≤
𝐶) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 0 ≤ 𝐶) | 
| 95 |  | eluzle 12891 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘(𝐶 + 1)) → (𝐶 + 1) ≤ 𝑘) | 
| 96 | 95 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝐶 + 1) ≤ 𝑘) | 
| 97 | 92 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐶 ∈ ℝ) | 
| 98 |  | 1red 11262 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 1 ∈
ℝ) | 
| 99 | 85 | nn0red 12588 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝑘 ∈ ℝ) | 
| 100 |  | leaddsub 11739 | . . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑘 ∈
ℝ) → ((𝐶 + 1)
≤ 𝑘 ↔ 𝐶 ≤ (𝑘 − 1))) | 
| 101 | 97, 98, 99, 100 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝐶 + 1) ≤ 𝑘 ↔ 𝐶 ≤ (𝑘 − 1))) | 
| 102 | 96, 101 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐶 ≤ (𝑘 − 1)) | 
| 103 | 87, 90, 92, 94, 102 | elfzd 13555 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐶 ∈ (0...(𝑘 − 1))) | 
| 104 | 34 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐶 ∈ ℂ) | 
| 105 | 104, 85 | bcc0 44359 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝐶C𝑐𝑘) = 0 ↔ 𝐶 ∈ (0...(𝑘 − 1)))) | 
| 106 | 103, 105 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝐶C𝑐𝑘) = 0) | 
| 107 | 106 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = (0 · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 108 | 2 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐴 ∈ ℂ) | 
| 109 |  | eluzelcn 12890 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘(𝐶 + 1)) → 𝑘 ∈ ℂ) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝑘 ∈ ℂ) | 
| 111 | 104, 110 | subcld 11620 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝐶 − 𝑘) ∈ ℂ) | 
| 112 | 108, 111 | cxpcld 26750 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝐴↑𝑐(𝐶 − 𝑘)) ∈ ℂ) | 
| 113 | 4 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → 𝐵 ∈ ℂ) | 
| 114 | 113, 85 | expcld 14186 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (𝐵↑𝑘) ∈ ℂ) | 
| 115 | 112, 114 | mulcld 11281 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)) ∈ ℂ) | 
| 116 | 115 | mul02d 11459 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (0 · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = 0) | 
| 117 | 107, 116 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = 0) | 
| 118 | 86, 117 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((𝑗 ∈ ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘) = 0) | 
| 119 | 118 | abs00bd 15330 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) = 0) | 
| 120 |  | 0re 11263 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 121 | 119, 120 | eqeltrdi 2849 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) ∈ ℝ) | 
| 122 |  | eqle 11363 | . . . . . . 7
⊢
(((abs‘((𝑗
∈ ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) ∈ ℝ ∧ (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) = 0) → (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) ≤ 0) | 
| 123 | 121, 119,
122 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) ≤ 0) | 
| 124 | 71 | recnd 11289 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((ℕ0 × {0})‘𝑘) ∈ ℂ) | 
| 125 | 85, 124 | syldan 591 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → ((ℕ0 ×
{0})‘𝑘) ∈
ℂ) | 
| 126 | 125 | mul02d 11459 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (0 ·
((ℕ0 × {0})‘𝑘)) = 0) | 
| 127 | 123, 126 | breqtrrd 5171 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈
(ℤ≥‘(𝐶 + 1))) → (abs‘((𝑗 ∈ ℕ0
↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))‘𝑘)) ≤ (0 · ((ℕ0
× {0})‘𝑘))) | 
| 128 | 39, 64, 71, 72, 83, 68, 127 | cvgcmpce 15854 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → seq0( +
, (𝑗 ∈
ℕ0 ↦ ((𝐶C𝑐𝑗) · ((𝐴↑𝑐(𝐶 − 𝑗)) · (𝐵↑𝑗))))) ∈ dom ⇝ ) | 
| 129 | 39, 40, 43, 62, 61, 128 | isumsplit 15876 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈
ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = (Σ𝑘 ∈ (0...((𝐶 + 1) − 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))) | 
| 130 |  | 1cnd 11256 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → 1 ∈
ℂ) | 
| 131 | 35, 130 | pncand 11621 | . . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐶 + 1) − 1) = 𝐶) | 
| 132 | 131 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(0...((𝐶 + 1) − 1)) =
(0...𝐶)) | 
| 133 | 132 | sumeq1d 15736 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝐶 + 1) −
1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | 
| 134 | 133 | oveq1d 7446 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(Σ𝑘 ∈
(0...((𝐶 + 1) −
1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) = (Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))) | 
| 135 | 117 | sumeq2dv 15738 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (ℤ≥‘(𝐶 + 1))0) | 
| 136 |  | ssid 4006 | . . . . . . 7
⊢
(ℤ≥‘(𝐶 + 1)) ⊆
(ℤ≥‘(𝐶 + 1)) | 
| 137 | 136 | orci 866 | . . . . . 6
⊢
((ℤ≥‘(𝐶 + 1)) ⊆
(ℤ≥‘(𝐶 + 1)) ∨
(ℤ≥‘(𝐶 + 1)) ∈ Fin) | 
| 138 |  | sumz 15758 | . . . . . 6
⊢
(((ℤ≥‘(𝐶 + 1)) ⊆
(ℤ≥‘(𝐶 + 1)) ∨
(ℤ≥‘(𝐶 + 1)) ∈ Fin) → Σ𝑘 ∈
(ℤ≥‘(𝐶 + 1))0 = 0) | 
| 139 | 137, 138 | ax-mp 5 | . . . . 5
⊢
Σ𝑘 ∈
(ℤ≥‘(𝐶 + 1))0 = 0 | 
| 140 | 135, 139 | eqtrdi 2793 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = 0) | 
| 141 | 140 | oveq2d 7447 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
(Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (ℤ≥‘(𝐶 + 1))((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) = (Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + 0)) | 
| 142 | 129, 134,
141 | 3eqtrd 2781 | . 2
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) →
Σ𝑘 ∈
ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) = (Σ𝑘 ∈ (0...𝐶)((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))) + 0)) | 
| 143 | 38, 142, 33 | 3eqtr4rd 2788 | 1
⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) |