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𝑐 𝑘 ) · ( ( 𝐴 ↑𝑐 ( 𝐶 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )