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	$$⊢\phi \to A\in {ℝ}^{+}$$
	binomcxp.b	$$⊢\phi \to B\in ℝ$$
	binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
	binomcxp.c	$$⊢\phi \to C\in ℂ$$
Assertion	binomcxp	$$⊢\phi \to {\left(A+B\right)}^C=\sum _{k\in {\mathbb{N}}_0}\left(C{C}_{𝑐}k\right)A^{C-k}{B}^k$$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$$⊢\phi \to A\in {ℝ}^{+}$$
2		binomcxp.b	$$⊢\phi \to B\in ℝ$$
3		binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
4		binomcxp.c	$$⊢\phi \to C\in ℂ$$
5	1 2 3 4	binomcxplemnn0	$$⊢\left(\phi \wedge C\in {\mathbb{N}}_0\right)\to {\left(A+B\right)}^C=\sum _{k\in {\mathbb{N}}_0}\left(C{C}_{𝑐}k\right)A^{C-k}{B}^k$$
6		eqid	$$⊢\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
7		fveq2	$$⊢x=k\to \left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)$$
8		oveq2	$$⊢x=k\to b^x=b^k$$
9	7 8	oveq12d	$$⊢x=k\to \left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^k$$
10	9	cbvmptv	$$⊢\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)=\left(k\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^k\right)$$
11	10	mpteq2i	$$⊢\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)=\left(b\in ℂ⟼\left(k\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^k\right)\right)$$
12		eqid	$$⊢sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$$
13		id	$$⊢x=k\to x=k$$
14		oveq2	$$⊢y=j\to C{C}_{𝑐}y=C{C}_{𝑐}j$$
15	14	cbvmptv	$$⊢\left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
16	15	a1i	$$⊢x=k\to \left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
17	16 13	fveq12d	$$⊢x=k\to \left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)\left(x\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)$$
18	13 17	oveq12d	$$⊢x=k\to x\left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)\left(x\right)=k\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)$$
19		oveq1	$$⊢x=k\to x-1=k-1$$
20	19	oveq2d	$$⊢x=k\to b^{x-1}=b^{k-1}$$
21	18 20	oveq12d	$$⊢x=k\to x\left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)\left(x\right)b^{x-1}=k\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^{k-1}$$
22	21	cbvmptv	$$⊢\left(x\in \mathbb{N}⟼x\left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)\left(x\right)b^{x-1}\right)=\left(k\in \mathbb{N}⟼k\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^{k-1}\right)$$
23	22	mpteq2i	$$⊢\left(b\in ℂ⟼\left(x\in \mathbb{N}⟼x\left(y\in {\mathbb{N}}_0⟼C{C}_{𝑐}y\right)\left(x\right)b^{x-1}\right)\right)=\left(b\in ℂ⟼\left(k\in \mathbb{N}⟼k\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(k\right)b^{k-1}\right)\right)$$
24		oveq2	$$⊢x=j\to C{C}_{𝑐}x=C{C}_{𝑐}j$$
25	24	cbvmptv	$$⊢\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
26	25	fveq1i	$$⊢\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)$$
27	26	oveq1i	$$⊢\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x$$
28	27	mpteq2i	$$⊢\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)=\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)$$
29	28	mpteq2i	$$⊢\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)=\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)$$
30	29	fveq1i	$$⊢\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)=\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)$$
31		seqeq3	$$⊢\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)=\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\to seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)=seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)$$
32	30 31	ax-mp	$$⊢seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)=seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)$$
33	32	eleq1i	$$⊢seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\leftrightarrow seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝$$
34	33	rabbii	$$⊢\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\}=\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\}$$
35	34	supeq1i	$$⊢sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$$
36	35	oveq2i	$$⊢\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)=\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)$$
37	36	imaeq2i	$$⊢{\mathrm{abs}}^{-1}\left[\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)\right]={\mathrm{abs}}^{-1}\left[\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)\right]$$
38		eqid	$$⊢\left(b\in {\mathrm{abs}}^{-1}\left[\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)\right]⟼\sum _{k\in {\mathbb{N}}_0}\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(b\right)\left(k\right)\right)=\left(b\in {\mathrm{abs}}^{-1}\left[\left[0,sup\left(\left\{r\in ℝ|seq0\left(+,\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(x\in {\mathbb{N}}_0⟼C{C}_{𝑐}x\right)\left(x\right)b^x\right)\right)\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\right)\right]⟼\sum _{k\in {\mathbb{N}}_0}\left(b\in ℂ⟼\left(x\in {\mathbb{N}}_0⟼\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)\left(x\right)b^x\right)\right)\left(b\right)\left(k\right)\right)$$
39	1 2 3 4 6 11 12 23 37 38	binomcxplemnotnn0	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to {\left(A+B\right)}^C=\sum _{k\in {\mathbb{N}}_0}\left(C{C}_{𝑐}k\right)A^{C-k}{B}^k$$
40	5 39	pm2.61dan	$$⊢\phi \to {\left(A+B\right)}^C=\sum _{k\in {\mathbb{N}}_0}\left(C{C}_{𝑐}k\right)A^{C-k}{B}^k$$