Metamath Proof Explorer


Theorem binomcxp

Description: Generalize the binomial theorem binom to positive real summand A , real summand B , and complex exponent C . Proof in https://en.wikibooks.org/wiki/Advanced_Calculus ; see also https://en.wikipedia.org/wiki/Binomial_series , https://en.wikipedia.org/wiki/Binomial_theorem (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem . (Contributed by Steve Rodriguez, 22-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 binomcxp.a ( 𝜑𝐴 ∈ ℝ+ )
2 binomcxp.b ( 𝜑𝐵 ∈ ℝ )
3 binomcxp.lt ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4 binomcxp.c ( 𝜑𝐶 ∈ ℂ )
5 1 2 3 4 binomcxplemnn0 ( ( 𝜑𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
6 eqid ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
7 fveq2 ( 𝑥 = 𝑘 → ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) = ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) )
8 oveq2 ( 𝑥 = 𝑘 → ( 𝑏𝑥 ) = ( 𝑏𝑘 ) )
9 7 8 oveq12d ( 𝑥 = 𝑘 → ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) = ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) · ( 𝑏𝑘 ) ) )
10 9 cbvmptv ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) · ( 𝑏𝑘 ) ) )
11 10 mpteq2i ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) · ( 𝑏𝑘 ) ) ) )
12 eqid sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
13 id ( 𝑥 = 𝑘𝑥 = 𝑘 )
14 oveq2 ( 𝑦 = 𝑗 → ( 𝐶 C𝑐 𝑦 ) = ( 𝐶 C𝑐 𝑗 ) )
15 14 cbvmptv ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
16 15 a1i ( 𝑥 = 𝑘 → ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
17 16 13 fveq12d ( 𝑥 = 𝑘 → ( ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) ‘ 𝑥 ) = ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) )
18 13 17 oveq12d ( 𝑥 = 𝑘 → ( 𝑥 · ( ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) ‘ 𝑥 ) ) = ( 𝑘 · ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) ) )
19 oveq1 ( 𝑥 = 𝑘 → ( 𝑥 − 1 ) = ( 𝑘 − 1 ) )
20 19 oveq2d ( 𝑥 = 𝑘 → ( 𝑏 ↑ ( 𝑥 − 1 ) ) = ( 𝑏 ↑ ( 𝑘 − 1 ) ) )
21 18 20 oveq12d ( 𝑥 = 𝑘 → ( ( 𝑥 · ( ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) ‘ 𝑥 ) ) · ( 𝑏 ↑ ( 𝑥 − 1 ) ) ) = ( ( 𝑘 · ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
22 21 cbvmptv ( 𝑥 ∈ ℕ ↦ ( ( 𝑥 · ( ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) ‘ 𝑥 ) ) · ( 𝑏 ↑ ( 𝑥 − 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
23 22 mpteq2i ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ ↦ ( ( 𝑥 · ( ( 𝑦 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑦 ) ) ‘ 𝑥 ) ) · ( 𝑏 ↑ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
24 oveq2 ( 𝑥 = 𝑗 → ( 𝐶 C𝑐 𝑥 ) = ( 𝐶 C𝑐 𝑗 ) )
25 24 cbvmptv ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
26 25 fveq1i ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) = ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 )
27 26 oveq1i ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) = ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) )
28 27 mpteq2i ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) )
29 28 mpteq2i ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) = ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) )
30 29 fveq1i ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 )
31 seqeq3 ( ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) → seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) )
32 30 31 ax-mp seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) )
33 32 eleq1i ( seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ )
34 33 rabbii { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ }
35 34 supeq1i sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
36 35 oveq2i ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) = ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
37 36 imaeq2i ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) = ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
38 eqid ( 𝑏 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑏 ) ‘ 𝑘 ) ) = ( 𝑏 ∈ ( abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑥 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑏 ∈ ℂ ↦ ( 𝑥 ∈ ℕ0 ↦ ( ( ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) ‘ 𝑥 ) · ( 𝑏𝑥 ) ) ) ) ‘ 𝑏 ) ‘ 𝑘 ) )
39 1 2 3 4 6 11 12 23 37 38 binomcxplemnotnn0 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
40 5 39 pm2.61dan ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )