Metamath Proof Explorer

Theorem binomcxplemnn0

Description: Lemma for binomcxp . When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set ( 0 ... C ) , and when the index set is widened beyond C the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion binomcxplemnn0 ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 binomcxp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4 binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 1 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7 binom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
8 7 3expia ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℕ0 → ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
9 5 6 8 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ℕ0 → ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
10 9 imp ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
11 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
13 11 12 addcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
15 cxpexp ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) )
16 13 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 + 𝐵 ) ↑ 𝐶 ) )
17 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝐶 ) → 𝑘 ∈ ℕ0 )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
20 18 19 bccbc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) = ( 𝐶 C 𝑘 ) )
21 17 20 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( 𝐶 C𝑐 𝑘 ) = ( 𝐶 C 𝑘 ) )
22 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → 𝐴 ∈ ℂ )
23 elfzle2 ⊢ ( 𝑘 ∈ ( 0 ... 𝐶 ) → 𝑘 ≤ 𝐶 )
24 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → 𝑘 ≤ 𝐶 )
25 nn0sub ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑘 ≤ 𝐶 ↔ ( 𝐶 − 𝑘 ) ∈ ℕ0 ) )
26 25 ancoms ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ≤ 𝐶 ↔ ( 𝐶 − 𝑘 ) ∈ ℕ0 ) )
27 26 adantll ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ≤ 𝐶 ↔ ( 𝐶 − 𝑘 ) ∈ ℕ0 ) )
28 17 27 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( 𝑘 ≤ 𝐶 ↔ ( 𝐶 − 𝑘 ) ∈ ℕ0 ) )
29 24 28 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( 𝐶 − 𝑘 ) ∈ ℕ0 )
30 cxpexp ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 − 𝑘 ) ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) = ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) )
31 22 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) = ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) )
32 31 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
33 21 32 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝐶 ) ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
34 33 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
35 10 16 34 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
36 4 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
37 13 36 cxpcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) ∈ ℂ )
38 35 37 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ∈ ℂ )
39 38 addid1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + 0 ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
40 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
41 eqid ⊢ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) = ( ℤ≥ ‘ ( 𝐶 + 1 ) )
42 1nn0 ⊢ 1 ∈ ℕ0
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 1 ∈ ℕ0 )
44 14 43 nn0addcld ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 + 1 ) ∈ ℕ0 )
45 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) )
46 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
47 46 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 𝑘 ) )
48 46 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐶 − 𝑗 ) = ( 𝐶 − 𝑘 ) )
49 48 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) = ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) )
50 46 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐵 ↑ 𝑗 ) = ( 𝐵 ↑ 𝑘 ) )
51 49 50 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) = ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
52 47 51 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
53 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
54 53 19 bcccl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
55 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
56 19 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
57 53 56 subcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 − 𝑘 ) ∈ ℂ )
58 55 57 cxpcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) ∈ ℂ )
59 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
60 59 19 expcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑘 ) ∈ ℂ )
61 58 60 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ∈ ℂ )
62 54 61 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ∈ ℂ )
63 45 52 19 62 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
64 peano2nn0 ⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 + 1 ) ∈ ℕ0 )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 + 1 ) ∈ ℕ0 )
66 c0ex ⊢ 0 ∈ V
67 66 fconst ⊢ ( ℕ0 × { 0 } ) : ℕ0 ⟶ { 0 }
68 67 a1i ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ℕ0 × { 0 } ) : ℕ0 ⟶ { 0 } )
69 0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 0 ∈ ℝ )
70 69 snssd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → { 0 } ⊆ ℝ )
71 68 70 fssd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ℕ0 × { 0 } ) : ℕ0 ⟶ ℝ )
72 71 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 0 } ) ‘ 𝑘 ) ∈ ℝ )
73 63 62 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
74 climrel ⊢ Rel ⇝
75 40 xpeq1i ⊢ ( ℕ0 × { 0 } ) = ( ( ℤ≥ ‘ 0 ) × { 0 } )
76 seqeq3 ⊢ ( ( ℕ0 × { 0 } ) = ( ( ℤ≥ ‘ 0 ) × { 0 } ) → seq 0 ( + , ( ℕ0 × { 0 } ) ) = seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) )
77 75 76 ax-mp ⊢ seq 0 ( + , ( ℕ0 × { 0 } ) ) = seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) )
78 0z ⊢ 0 ∈ ℤ
79 serclim0 ⊢ ( 0 ∈ ℤ → seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) ⇝ 0 )
80 78 79 ax-mp ⊢ seq 0 ( + , ( ( ℤ≥ ‘ 0 ) × { 0 } ) ) ⇝ 0
81 77 80 eqbrtri ⊢ seq 0 ( + , ( ℕ0 × { 0 } ) ) ⇝ 0
82 releldm ⊢ ( ( Rel ⇝ ∧ seq 0 ( + , ( ℕ0 × { 0 } ) ) ⇝ 0 ) → seq 0 ( + , ( ℕ0 × { 0 } ) ) ∈ dom ⇝ )
83 74 81 82 mp2an ⊢ seq 0 ( + , ( ℕ0 × { 0 } ) ) ∈ dom ⇝
84 83 a1i ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → seq 0 ( + , ( ℕ0 × { 0 } ) ) ∈ dom ⇝ )
85 eluznn0 ⊢ ( ( ( 𝐶 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
86 65 85 sylan ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
87 86 63 syldan ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
88 0zd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 0 ∈ ℤ )
89 86 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝑘 ∈ ℤ )
90 1zzd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 1 ∈ ℤ )
91 89 90 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
92 14 nn0zd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℤ )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐶 ∈ ℤ )
94 14 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 0 ≤ 𝐶 )
95 94 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 0 ≤ 𝐶 )
96 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) → ( 𝐶 + 1 ) ≤ 𝑘 )
97 96 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐶 + 1 ) ≤ 𝑘 )
98 93 zred ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐶 ∈ ℝ )
99 1red ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 1 ∈ ℝ )
100 86 nn0red ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝑘 ∈ ℝ )
101 leaddsub ⊢ ( ( 𝐶 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐶 + 1 ) ≤ 𝑘 ↔ 𝐶 ≤ ( 𝑘 − 1 ) ) )
102 98 99 100 101 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝐶 + 1 ) ≤ 𝑘 ↔ 𝐶 ≤ ( 𝑘 − 1 ) ) )
103 97 102 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐶 ≤ ( 𝑘 − 1 ) )
104 88 91 93 95 103 elfzd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) )
105 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐶 ∈ ℂ )
106 105 86 bcc0 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝐶 C𝑐 𝑘 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) ) )
107 104 106 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐶 C𝑐 𝑘 ) = 0 )
108 107 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( 0 · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
109 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐴 ∈ ℂ )
110 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) → 𝑘 ∈ ℂ )
111 110 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝑘 ∈ ℂ )
112 105 111 subcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐶 − 𝑘 ) ∈ ℂ )
113 109 112 cxpcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) ∈ ℂ )
114 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → 𝐵 ∈ ℂ )
115 114 86 expcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 𝐵 ↑ 𝑘 ) ∈ ℂ )
116 113 115 mulcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ∈ ℂ )
117 116 mul02d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 0 · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = 0 )
118 108 117 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = 0 )
119 87 118 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) = 0 )
120 119 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) = 0 )
121 0re ⊢ 0 ∈ ℝ
122 120 121 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) ∈ ℝ )
123 eqle ⊢ ( ( ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) = 0 ) → ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) ≤ 0 )
124 122 120 123 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) ≤ 0 )
125 72 recnd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ℕ0 × { 0 } ) ‘ 𝑘 ) ∈ ℂ )
126 86 125 syldan ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( ( ℕ0 × { 0 } ) ‘ 𝑘 ) ∈ ℂ )
127 126 mul02d ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( 0 · ( ( ℕ0 × { 0 } ) ‘ 𝑘 ) ) = 0 )
128 124 127 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ) → ( abs ‘ ( ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ‘ 𝑘 ) ) ≤ ( 0 · ( ( ℕ0 × { 0 } ) ‘ 𝑘 ) ) )
129 40 65 72 73 84 69 128 cvgcmpce ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → seq 0 ( + , ( 𝑗 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑗 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ) ) ∈ dom ⇝ )
130 40 41 44 63 62 129 isumsplit ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝐶 + 1 ) − 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
131 1cnd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
132 36 131 pncand ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) − 1 ) = 𝐶 )
133 132 oveq2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( 0 ... ( ( 𝐶 + 1 ) − 1 ) ) = ( 0 ... 𝐶 ) )
134 133 sumeq1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝐶 + 1 ) − 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
135 134 oveq1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝐶 + 1 ) − 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
136 118 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) 0 )
137 ssid ⊢ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐶 + 1 ) )
138 137 orci ⊢ ( ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ∨ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ∈ Fin )
139 sumz ⊢ ( ( ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ∨ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ∈ Fin ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) 0 = 0 )
140 138 139 ax-mp ⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) 0 = 0
141 136 140 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = 0 )
142 141 oveq2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐶 + 1 ) ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + 0 ) )
143 130 135 142 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝐶 ) ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) + 0 ) )
144 39 143 35 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )