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