Theorem binomcxplemwb

Description: Lemma for binomcxp . The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxplem.c	$$⊢\phi \to C\in ℂ$$
	binomcxplem.k	$$⊢\phi \to K\in \mathbb{N}$$
Assertion	binomcxplemwb	$$⊢\phi \to \left(C-K\right)\left(C{C}_{𝑐}K\right)+\left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=C\left(C{C}_{𝑐}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		binomcxplem.c	$$⊢\phi \to C\in ℂ$$
2		binomcxplem.k	$$⊢\phi \to K\in \mathbb{N}$$
3	2	nncnd	$$⊢\phi \to K\in ℂ$$
4	1 3	npcand	$$⊢\phi \to C-K+K=C$$
5	4	oveq1d	$$⊢\phi \to \left(C-K+K\right)\left(C^{\underset{\_}{K}}\right)=C\left(C^{\underset{\_}{K}}\right)$$
6	1 3	subcld	$$⊢\phi \to C-K\in ℂ$$
7	2	nnnn0d	$$⊢\phi \to K\in {\mathbb{N}}_0$$
8		fallfaccl	$$⊢\left(C\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to C^{\underset{\_}{K}}\in ℂ$$
9	1 7 8	syl2anc	$$⊢\phi \to C^{\underset{\_}{K}}\in ℂ$$
10	6 3 9	adddird	$$⊢\phi \to \left(C-K+K\right)\left(C^{\underset{\_}{K}}\right)=\left(C-K\right)\left(C^{\underset{\_}{K}}\right)+K\left(C^{\underset{\_}{K}}\right)$$
11	5 10	eqtr3d	$$⊢\phi \to C\left(C^{\underset{\_}{K}}\right)=\left(C-K\right)\left(C^{\underset{\_}{K}}\right)+K\left(C^{\underset{\_}{K}}\right)$$
12	11	oveq1d	$$⊢\phi \to \frac{C\left(C^{\underset{\_}{K}}\right)}{K!}=\frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)+K\left(C^{\underset{\_}{K}}\right)}{K!}$$
13	1 7	bccval	$$⊢\phi \to C{C}_{𝑐}K=\frac{C^{\underset{\_}{K}}}{K!}$$
14	13	oveq2d	$$⊢\phi \to C\left(C{C}_{𝑐}K\right)=C\left(\frac{C^{\underset{\_}{K}}}{K!}\right)$$
15		faccl	$$⊢K\in {\mathbb{N}}_0\to K!\in \mathbb{N}$$
16	15	nncnd	$$⊢K\in {\mathbb{N}}_0\to K!\in ℂ$$
17	7 16	syl	$$⊢\phi \to K!\in ℂ$$
18		facne0	$$⊢K\in {\mathbb{N}}_0\to K!\ne 0$$
19	7 18	syl	$$⊢\phi \to K!\ne 0$$
20	1 9 17 19	divassd	$$⊢\phi \to \frac{C\left(C^{\underset{\_}{K}}\right)}{K!}=C\left(\frac{C^{\underset{\_}{K}}}{K!}\right)$$
21	14 20	eqtr4d	$$⊢\phi \to C\left(C{C}_{𝑐}K\right)=\frac{C\left(C^{\underset{\_}{K}}\right)}{K!}$$
22	6 9 17 19	divassd	$$⊢\phi \to \frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)}{K!}=\left(C-K\right)\left(\frac{C^{\underset{\_}{K}}}{K!}\right)$$
23	22	oveq1d	$$⊢\phi \to \left(\frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)}{K!}\right)+\left(\frac{K\left(C^{\underset{\_}{K}}\right)}{K!}\right)=\left(C-K\right)\left(\frac{C^{\underset{\_}{K}}}{K!}\right)+\left(\frac{K\left(C^{\underset{\_}{K}}\right)}{K!}\right)$$
24	6 9	mulcld	$$⊢\phi \to \left(C-K\right)\left(C^{\underset{\_}{K}}\right)\in ℂ$$
25	3 9	mulcld	$$⊢\phi \to K\left(C^{\underset{\_}{K}}\right)\in ℂ$$
26	24 25 17 19	divdird	$$⊢\phi \to \frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)+K\left(C^{\underset{\_}{K}}\right)}{K!}=\left(\frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)}{K!}\right)+\left(\frac{K\left(C^{\underset{\_}{K}}\right)}{K!}\right)$$
27	13	oveq2d	$$⊢\phi \to \left(C-K\right)\left(C{C}_{𝑐}K\right)=\left(C-K\right)\left(\frac{C^{\underset{\_}{K}}}{K!}\right)$$
28		nnm1nn0	$$⊢K\in \mathbb{N}\to K-1\in {\mathbb{N}}_0$$
29	2 28	syl	$$⊢\phi \to K-1\in {\mathbb{N}}_0$$
30		faccl	$$⊢K-1\in {\mathbb{N}}_0\to \left(K-1\right)!\in \mathbb{N}$$
31	30	nncnd	$$⊢K-1\in {\mathbb{N}}_0\to \left(K-1\right)!\in ℂ$$
32	29 31	syl	$$⊢\phi \to \left(K-1\right)!\in ℂ$$
33		facne0	$$⊢K-1\in {\mathbb{N}}_0\to \left(K-1\right)!\ne 0$$
34	29 33	syl	$$⊢\phi \to \left(K-1\right)!\ne 0$$
35	2	nnne0d	$$⊢\phi \to K\ne 0$$
36	9 32 3 34 35	divcan5d	$$⊢\phi \to \frac{K\left(C^{\underset{\_}{K}}\right)}{K\left(K-1\right)!}=\frac{C^{\underset{\_}{K}}}{\left(K-1\right)!}$$
37		1cnd	$$⊢\phi \to 1\in ℂ$$
38	3 37	npcand	$$⊢\phi \to K-1+1=K$$
39	38	fveq2d	$$⊢\phi \to \left(K-1+1\right)!=K!$$
40	38	oveq2d	$$⊢\phi \to \left(K-1\right)!\left(K-1+1\right)=\left(K-1\right)!K$$
41		facp1	$$⊢K-1\in {\mathbb{N}}_0\to \left(K-1+1\right)!=\left(K-1\right)!\left(K-1+1\right)$$
42	29 41	syl	$$⊢\phi \to \left(K-1+1\right)!=\left(K-1\right)!\left(K-1+1\right)$$
43	3 32	mulcomd	$$⊢\phi \to K\left(K-1\right)!=\left(K-1\right)!K$$
44	40 42 43	3eqtr4d	$$⊢\phi \to \left(K-1+1\right)!=K\left(K-1\right)!$$
45	39 44	eqtr3d	$$⊢\phi \to K!=K\left(K-1\right)!$$
46	45	oveq2d	$$⊢\phi \to \frac{K\left(C^{\underset{\_}{K}}\right)}{K!}=\frac{K\left(C^{\underset{\_}{K}}\right)}{K\left(K-1\right)!}$$
47	3 37	subcld	$$⊢\phi \to K-1\in ℂ$$
48	1 47	subcld	$$⊢\phi \to C-\left(K-1\right)\in ℂ$$
49		fallfaccl	$$⊢\left(C\in ℂ\wedge K-1\in {\mathbb{N}}_0\right)\to C^{\underset{\_}{\left(K-1\right)}}\in ℂ$$
50	1 29 49	syl2anc	$$⊢\phi \to C^{\underset{\_}{\left(K-1\right)}}\in ℂ$$
51	48 50 32 34	divassd	$$⊢\phi \to \frac{\left(C-\left(K-1\right)\right)\left(C^{\underset{\_}{\left(K-1\right)}}\right)}{\left(K-1\right)!}=\left(C-\left(K-1\right)\right)\left(\frac{C^{\underset{\_}{\left(K-1\right)}}}{\left(K-1\right)!}\right)$$
52	38	oveq2d	$$⊢\phi \to C^{\underset{\_}{\left(K-1+1\right)}}=C^{\underset{\_}{K}}$$
53		fallfacp1	$$⊢\left(C\in ℂ\wedge K-1\in {\mathbb{N}}_0\right)\to C^{\underset{\_}{\left(K-1+1\right)}}=\left(C^{\underset{\_}{\left(K-1\right)}}\right)\left(C-\left(K-1\right)\right)$$
54	1 29 53	syl2anc	$$⊢\phi \to C^{\underset{\_}{\left(K-1+1\right)}}=\left(C^{\underset{\_}{\left(K-1\right)}}\right)\left(C-\left(K-1\right)\right)$$
55	52 54	eqtr3d	$$⊢\phi \to C^{\underset{\_}{K}}=\left(C^{\underset{\_}{\left(K-1\right)}}\right)\left(C-\left(K-1\right)\right)$$
56	48 50	mulcomd	$$⊢\phi \to \left(C-\left(K-1\right)\right)\left(C^{\underset{\_}{\left(K-1\right)}}\right)=\left(C^{\underset{\_}{\left(K-1\right)}}\right)\left(C-\left(K-1\right)\right)$$
57	55 56	eqtr4d	$$⊢\phi \to C^{\underset{\_}{K}}=\left(C-\left(K-1\right)\right)\left(C^{\underset{\_}{\left(K-1\right)}}\right)$$
58	57	oveq1d	$$⊢\phi \to \frac{C^{\underset{\_}{K}}}{\left(K-1\right)!}=\frac{\left(C-\left(K-1\right)\right)\left(C^{\underset{\_}{\left(K-1\right)}}\right)}{\left(K-1\right)!}$$
59	1 29	bccval	$$⊢\phi \to C{C}_{𝑐}\left(K-1\right)=\frac{C^{\underset{\_}{\left(K-1\right)}}}{\left(K-1\right)!}$$
60	59	oveq2d	$$⊢\phi \to \left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=\left(C-\left(K-1\right)\right)\left(\frac{C^{\underset{\_}{\left(K-1\right)}}}{\left(K-1\right)!}\right)$$
61	51 58 60	3eqtr4rd	$$⊢\phi \to \left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=\frac{C^{\underset{\_}{K}}}{\left(K-1\right)!}$$
62	36 46 61	3eqtr4rd	$$⊢\phi \to \left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=\frac{K\left(C^{\underset{\_}{K}}\right)}{K!}$$
63	27 62	oveq12d	$$⊢\phi \to \left(C-K\right)\left(C{C}_{𝑐}K\right)+\left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=\left(C-K\right)\left(\frac{C^{\underset{\_}{K}}}{K!}\right)+\left(\frac{K\left(C^{\underset{\_}{K}}\right)}{K!}\right)$$
64	23 26 63	3eqtr4rd	$$⊢\phi \to \left(C-K\right)\left(C{C}_{𝑐}K\right)+\left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=\frac{\left(C-K\right)\left(C^{\underset{\_}{K}}\right)+K\left(C^{\underset{\_}{K}}\right)}{K!}$$
65	12 21 64	3eqtr4rd	$$⊢\phi \to \left(C-K\right)\left(C{C}_{𝑐}K\right)+\left(C-\left(K-1\right)\right)\left(C{C}_{𝑐}\left(K-1\right)\right)=C\left(C{C}_{𝑐}K\right)$$