binomcxplemnn0

Description: Lemma for binomcxp . When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set ( 0 ... C ) , and when the index set is widened beyond C the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
	binomcxp.b	$⊢ φ \to B \in ℝ$
	binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
	binomcxp.c	$⊢ φ \to C \in ℂ$
Assertion	binomcxplemnn0	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
2		binomcxp.b	$⊢ φ \to B \in ℝ$
3		binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
4		binomcxp.c	$⊢ φ \to C \in ℂ$
5	1	rpcnd	$⊢ φ \to A \in ℂ$
6	2	recnd	$⊢ φ \to B \in ℂ$
7		binom	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k = 0}^{C} (\binom{C}{k}) A^{C - k} B^{k}$
8	7	3expia	$⊢ (A \in ℂ \land B \in ℂ) \to (C \in ℕ_{0} \to {(A + B)}^{C} = \sum_{k = 0}^{C} (\binom{C}{k}) A^{C - k} B^{k})$
9	5 6 8	syl2anc	$⊢ φ \to (C \in ℕ_{0} \to {(A + B)}^{C} = \sum_{k = 0}^{C} (\binom{C}{k}) A^{C - k} B^{k})$
10	9	imp	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k = 0}^{C} (\binom{C}{k}) A^{C - k} B^{k}$
11	5	adantr	$⊢ (φ \land C \in ℕ_{0}) \to A \in ℂ$
12	6	adantr	$⊢ (φ \land C \in ℕ_{0}) \to B \in ℂ$
13	11 12	addcld	$⊢ (φ \land C \in ℕ_{0}) \to A + B \in ℂ$
14		simpr	$⊢ (φ \land C \in ℕ_{0}) \to C \in ℕ_{0}$
15		cxpexp	$⊢ (A + B \in ℂ \land C \in ℕ_{0}) \to {(A + B)}^{C} = {(A + B)}^{C}$
16	13 14 15	syl2anc	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} = {(A + B)}^{C}$
17		elfznn0	$⊢ k \in (0 \dots C) \to k \in ℕ_{0}$
18		simplr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to C \in ℕ_{0}$
19		simpr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
20	18 19	bccbc	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to C C_{𝑐} k = (\binom{C}{k})$
21	17 20	sylan2	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to C C_{𝑐} k = (\binom{C}{k})$
22	5	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to A \in ℂ$
23		elfzle2	$⊢ k \in (0 \dots C) \to k \leq C$
24	23	adantl	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to k \leq C$
25		nn0sub	$⊢ (k \in ℕ_{0} \land C \in ℕ_{0}) \to (k \leq C \leftrightarrow C - k \in ℕ_{0})$
26	25	ancoms	$⊢ (C \in ℕ_{0} \land k \in ℕ_{0}) \to (k \leq C \leftrightarrow C - k \in ℕ_{0})$
27	26	adantll	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (k \leq C \leftrightarrow C - k \in ℕ_{0})$
28	17 27	sylan2	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to (k \leq C \leftrightarrow C - k \in ℕ_{0})$
29	24 28	mpbid	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to C - k \in ℕ_{0}$
30		cxpexp	$⊢ (A \in ℂ \land C - k \in ℕ_{0}) \to A^{C - k} = A^{C - k}$
31	22 29 30	syl2anc	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to A^{C - k} = A^{C - k}$
32	31	oveq1d	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to A^{C - k} B^{k} = A^{C - k} B^{k}$
33	21 32	oveq12d	$⊢ ((φ \land C \in ℕ_{0}) \land k \in (0 \dots C)) \to (C C_{𝑐} k) A^{C - k} B^{k} = (\binom{C}{k}) A^{C - k} B^{k}$
34	33	sumeq2dv	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C} (\binom{C}{k}) A^{C - k} B^{k}$
35	10 16 34	3eqtr4d	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k}$
36	4	adantr	$⊢ (φ \land C \in ℕ_{0}) \to C \in ℂ$
37	13 36	cxpcld	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} \in ℂ$
38	35 37	eqeltrrd	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} \in ℂ$
39	38	addridd	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} + 0 = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k}$
40		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
41		eqid	$⊢ ℤ_{\geq (C + 1)} = ℤ_{\geq (C + 1)}$
42		1nn0	$⊢ 1 \in ℕ_{0}$
43	42	a1i	$⊢ (φ \land C \in ℕ_{0}) \to 1 \in ℕ_{0}$
44	14 43	nn0addcld	$⊢ (φ \land C \in ℕ_{0}) \to C + 1 \in ℕ_{0}$
45		eqidd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) = (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j})$
46		simpr	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to j = k$
47	46	oveq2d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to C C_{𝑐} j = C C_{𝑐} k$
48	46	oveq2d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to C - j = C - k$
49	48	oveq2d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to A^{C - j} = A^{C - k}$
50	46	oveq2d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to B^{j} = B^{k}$
51	49 50	oveq12d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to A^{C - j} B^{j} = A^{C - k} B^{k}$
52	47 51	oveq12d	$⊢ (((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \land j = k) \to (C C_{𝑐} j) A^{C - j} B^{j} = (C C_{𝑐} k) A^{C - k} B^{k}$
53	4	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to C \in ℂ$
54	53 19	bcccl	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
55	5	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in ℂ$
56	19	nn0cnd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℂ$
57	53 56	subcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to C - k \in ℂ$
58	55 57	cxpcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C - k} \in ℂ$
59	6	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to B \in ℂ$
60	59 19	expcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to B^{k} \in ℂ$
61	58 60	mulcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{C - k} B^{k} \in ℂ$
62	54 61	mulcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k) A^{C - k} B^{k} \in ℂ$
63	45 52 19 62	fvmptd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k) = (C C_{𝑐} k) A^{C - k} B^{k}$
64		peano2nn0	$⊢ C \in ℕ_{0} \to C + 1 \in ℕ_{0}$
65	64	adantl	$⊢ (φ \land C \in ℕ_{0}) \to C + 1 \in ℕ_{0}$
66		c0ex	$⊢ 0 \in V$
67	66	fconst	$⊢ (ℕ_{0} \times \{0\}) : ℕ_{0} ⟶ \{0\}$
68	67	a1i	$⊢ (φ \land C \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) : ℕ_{0} ⟶ \{0\}$
69		0red	$⊢ (φ \land C \in ℕ_{0}) \to 0 \in ℝ$
70	69	snssd	$⊢ (φ \land C \in ℕ_{0}) \to \{0\} \subseteq ℝ$
71	68 70	fssd	$⊢ (φ \land C \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) : ℕ_{0} ⟶ ℝ$
72	71	ffvelcdmda	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) (k) \in ℝ$
73	63 62	eqeltrd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k) \in ℂ$
74		climrel	$⊢ Rel ⇝$
75	40	xpeq1i	$⊢ ℕ_{0} \times \{0\} = ℤ_{\geq 0} \times \{0\}$
76		seqeq3	$⊢ ℕ_{0} \times \{0\} = ℤ_{\geq 0} \times \{0\} \to seq 0 (+ (ℕ_{0} \times \{0\})) = seq 0 (+ (ℤ_{\geq 0} \times \{0\}))$
77	75 76	ax-mp	$⊢ seq 0 (+ (ℕ_{0} \times \{0\})) = seq 0 (+ (ℤ_{\geq 0} \times \{0\}))$
78		0z	$⊢ 0 \in ℤ$
79		serclim0	$⊢ 0 \in ℤ \to seq 0 (+ (ℤ_{\geq 0} \times \{0\})) ⇝ 0$
80	78 79	ax-mp	$⊢ seq 0 (+ (ℤ_{\geq 0} \times \{0\})) ⇝ 0$
81	77 80	eqbrtri	$⊢ seq 0 (+ (ℕ_{0} \times \{0\})) ⇝ 0$
82		releldm	$⊢ (Rel ⇝ \land seq 0 (+ (ℕ_{0} \times \{0\})) ⇝ 0) \to seq 0 (+ (ℕ_{0} \times \{0\})) \in dom ⇝$
83	74 81 82	mp2an	$⊢ seq 0 (+ (ℕ_{0} \times \{0\})) \in dom ⇝$
84	83	a1i	$⊢ (φ \land C \in ℕ_{0}) \to seq 0 (+ (ℕ_{0} \times \{0\})) \in dom ⇝$
85		eluznn0	$⊢ (C + 1 \in ℕ_{0} \land k \in ℤ_{\geq (C + 1)}) \to k \in ℕ_{0}$
86	65 85	sylan	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to k \in ℕ_{0}$
87	86 63	syldan	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k) = (C C_{𝑐} k) A^{C - k} B^{k}$
88		0zd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 0 \in ℤ$
89	86	nn0zd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to k \in ℤ$
90		1zzd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 1 \in ℤ$
91	89 90	zsubcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to k - 1 \in ℤ$
92	14	nn0zd	$⊢ (φ \land C \in ℕ_{0}) \to C \in ℤ$
93	92	adantr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C \in ℤ$
94	14	nn0ge0d	$⊢ (φ \land C \in ℕ_{0}) \to 0 \leq C$
95	94	adantr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 0 \leq C$
96		eluzle	$⊢ k \in ℤ_{\geq (C + 1)} \to C + 1 \leq k$
97	96	adantl	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C + 1 \leq k$
98	93	zred	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C \in ℝ$
99		1red	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 1 \in ℝ$
100	86	nn0red	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to k \in ℝ$
101		leaddsub	$⊢ (C \in ℝ \land 1 \in ℝ \land k \in ℝ) \to (C + 1 \leq k \leftrightarrow C \leq k - 1)$
102	98 99 100 101	syl3anc	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (C + 1 \leq k \leftrightarrow C \leq k - 1)$
103	97 102	mpbid	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C \leq k - 1$
104	88 91 93 95 103	elfzd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C \in (0 \dots k - 1)$
105	4	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C \in ℂ$
106	105 86	bcc0	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (C C_{𝑐} k = 0 \leftrightarrow C \in (0 \dots k - 1))$
107	104 106	mpbird	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C C_{𝑐} k = 0$
108	107	oveq1d	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (C C_{𝑐} k) A^{C - k} B^{k} = 0 \cdot A^{C - k} B^{k}$
109	5	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to A \in ℂ$
110		eluzelcn	$⊢ k \in ℤ_{\geq (C + 1)} \to k \in ℂ$
111	110	adantl	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to k \in ℂ$
112	105 111	subcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to C - k \in ℂ$
113	109 112	cxpcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to A^{C - k} \in ℂ$
114	6	ad2antrr	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to B \in ℂ$
115	114 86	expcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to B^{k} \in ℂ$
116	113 115	mulcld	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to A^{C - k} B^{k} \in ℂ$
117	116	mul02d	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 0 \cdot A^{C - k} B^{k} = 0$
118	108 117	eqtrd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (C C_{𝑐} k) A^{C - k} B^{k} = 0$
119	87 118	eqtrd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k) = 0$
120	119	abs00bd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| = 0$
121		0re	$⊢ 0 \in ℝ$
122	120 121	eqeltrdi	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| \in ℝ$
123		eqle	$⊢ (\|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| \in ℝ \land \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| = 0) \to \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| \leq 0$
124	122 120 123	syl2anc	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| \leq 0$
125	72	recnd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℕ_{0}) \to (ℕ_{0} \times \{0\}) (k) \in ℂ$
126	86 125	syldan	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to (ℕ_{0} \times \{0\}) (k) \in ℂ$
127	126	mul02d	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to 0 \cdot (ℕ_{0} \times \{0\}) (k) = 0$
128	124 127	breqtrrd	$⊢ ((φ \land C \in ℕ_{0}) \land k \in ℤ_{\geq (C + 1)}) \to \|(j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j}) (k)\| \leq 0 \cdot (ℕ_{0} \times \{0\}) (k)$
129	40 65 72 73 84 69 128	cvgcmpce	$⊢ (φ \land C \in ℕ_{0}) \to seq 0 (+ (j \in ℕ_{0} ⟼ (C C_{𝑐} j) A^{C - j} B^{j})) \in dom ⇝$
130	40 41 44 63 62 129	isumsplit	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C + 1 - 1} (C C_{𝑐} k) A^{C - k} B^{k} + \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k}$
131		1cnd	$⊢ (φ \land C \in ℕ_{0}) \to 1 \in ℂ$
132	36 131	pncand	$⊢ (φ \land C \in ℕ_{0}) \to C + 1 - 1 = C$
133	132	oveq2d	$⊢ (φ \land C \in ℕ_{0}) \to (0 \dots C + 1 - 1) = (0 \dots C)$
134	133	sumeq1d	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C + 1 - 1} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k}$
135	134	oveq1d	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C + 1 - 1} (C C_{𝑐} k) A^{C - k} B^{k} + \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} + \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k}$
136	118	sumeq2dv	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k \in ℤ_{\geq (C + 1)}} 0$
137		ssid	$⊢ ℤ_{\geq (C + 1)} \subseteq ℤ_{\geq (C + 1)}$
138	137	orci	$⊢ (ℤ_{\geq (C + 1)} \subseteq ℤ_{\geq (C + 1)} \lor ℤ_{\geq (C + 1)} \in Fin)$
139		sumz	$⊢ (ℤ_{\geq (C + 1)} \subseteq ℤ_{\geq (C + 1)} \lor ℤ_{\geq (C + 1)} \in Fin) \to \sum_{k \in ℤ_{\geq (C + 1)}} 0 = 0$
140	138 139	ax-mp	$⊢ \sum_{k \in ℤ_{\geq (C + 1)}} 0 = 0$
141	136 140	eqtrdi	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k} = 0$
142	141	oveq2d	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} + \sum_{k \in ℤ_{\geq (C + 1)}} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} + 0$
143	130 135 142	3eqtrd	$⊢ (φ \land C \in ℕ_{0}) \to \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k} = \sum_{k = 0}^{C} (C C_{𝑐} k) A^{C - k} B^{k} + 0$
144	39 143 35	3eqtr4rd	$⊢ (φ \land C \in ℕ_{0}) \to {(A + B)}^{C} = \sum_{k \in ℕ_{0}} (C C_{𝑐} k) A^{C - k} B^{k}$

Metamath Proof Explorer

Theorem binomcxplemnn0

Proof