srgbinomlem3

Description: Lemma 3 for srgbinomlem . (Contributed by AV, 23-Aug-2019) (Proof shortened by AV, 27-Oct-2019)

	Ref	Expression
Hypotheses	srgbinom.s	$⊢ S = {Base}_{R}$
	srgbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
	srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
	srgbinom.g	$⊢ G = {mulGrp}_{R}$
	srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	srgbinomlem.r	$⊢ φ \to R \in SRing$
	srgbinomlem.a	$⊢ φ \to A \in S$
	srgbinomlem.b	$⊢ φ \to B \in S$
	srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
	srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
	srgbinomlem.i	$⊢ ψ \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
Assertion	srgbinomlem3	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	$⊢ S = {Base}_{R}$
2		srgbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
3		srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
5		srgbinom.g	$⊢ G = {mulGrp}_{R}$
6		srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		srgbinomlem.r	$⊢ φ \to R \in SRing$
8		srgbinomlem.a	$⊢ φ \to A \in S$
9		srgbinomlem.b	$⊢ φ \to B \in S$
10		srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
11		srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
12		srgbinomlem.i	$⊢ ψ \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
13	12	adantl	$⊢ (φ \land ψ) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
14	13	oveq1d	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} A$
15		srgcmn	$⊢ R \in SRing \to R \in CMnd$
16	7 15	syl	$⊢ φ \to R \in CMnd$
17		simpl	$⊢ (φ \land k \in (0 \dots N + 1)) \to φ$
18		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
19		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
20	11 18 19	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
21		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
22	21	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
23		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
24	23	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
25	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	$⊢ (φ \land ((\binom{N}{k}) \in ℕ_{0} \land N + 1 - k \in ℕ_{0} \land k \in ℕ_{0})) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
26	17 20 22 24 25	syl13anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
27	1 4 16 11 26	gsummptfzsplit	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} (\underset{k \in \{N + 1\}}{\sum_{R}}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
28		srgmnd	$⊢ R \in SRing \to R \in Mnd$
29	7 28	syl	$⊢ φ \to R \in Mnd$
30		ovexd	$⊢ φ \to N + 1 \in V$
31		id	$⊢ φ \to φ$
32	11	nn0zd	$⊢ φ \to N \in ℤ$
33	32	peano2zd	$⊢ φ \to N + 1 \in ℤ$
34		bccl	$⊢ (N \in ℕ_{0} \land N + 1 \in ℤ) \to (\binom{N}{N + 1}) \in ℕ_{0}$
35	11 33 34	syl2anc	$⊢ φ \to (\binom{N}{N + 1}) \in ℕ_{0}$
36	11	nn0cnd	$⊢ φ \to N \in ℂ$
37		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
38	36 37	syl	$⊢ φ \to N + 1 \in ℂ$
39	38	subidd	$⊢ φ \to N + 1 - (N + 1) = 0$
40		0nn0	$⊢ 0 \in ℕ_{0}$
41	39 40	eqeltrdi	$⊢ φ \to N + 1 - (N + 1) \in ℕ_{0}$
42		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
43	11 42	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
44	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	$⊢ (φ \land ((\binom{N}{N + 1}) \in ℕ_{0} \land N + 1 - (N + 1) \in ℕ_{0} \land N + 1 \in ℕ_{0})) \to (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) \in S$
45	31 35 41 43 44	syl13anc	$⊢ φ \to (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) \in S$
46		oveq2	$⊢ k = N + 1 \to (\binom{N}{k}) = (\binom{N}{N + 1})$
47		oveq2	$⊢ k = N + 1 \to N + 1 - k = N + 1 - (N + 1)$
48	47	oveq1d	$⊢ k = N + 1 \to (N + 1 - k) \underset{˙}{\times} A = (N + 1 - (N + 1)) \underset{˙}{\times} A$
49		oveq1	$⊢ k = N + 1 \to k \underset{˙}{\times} B = (N + 1) \underset{˙}{\times} B$
50	48 49	oveq12d	$⊢ k = N + 1 \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) = ((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)$
51	46 50	oveq12d	$⊢ k = N + 1 \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B))$
52	1 51	gsumsn	$⊢ (R \in Mnd \land N + 1 \in V \land (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) \in S) \to \underset{k \in \{N + 1\}}{\sum_{R}} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B))$
53	29 30 45 52	syl3anc	$⊢ φ \to \underset{k \in \{N + 1\}}{\sum_{R}} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B))$
54	11	nn0red	$⊢ φ \to N \in ℝ$
55	54	ltp1d	$⊢ φ \to N < N + 1$
56	55	olcd	$⊢ φ \to (N + 1 < 0 \lor N < N + 1)$
57		bcval4	$⊢ (N \in ℕ_{0} \land N + 1 \in ℤ \land (N + 1 < 0 \lor N < N + 1)) \to (\binom{N}{N + 1}) = 0$
58	11 33 56 57	syl3anc	$⊢ φ \to (\binom{N}{N + 1}) = 0$
59	58	oveq1d	$⊢ φ \to (\binom{N}{N + 1}) \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) = 0 \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B))$
60	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem1	$⊢ (φ \land (N + 1 - (N + 1) \in ℕ_{0} \land N + 1 \in ℕ_{0})) \to ((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B) \in S$
61	31 41 43 60	syl12anc	$⊢ φ \to ((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B) \in S$
62		eqid	$⊢ 0_{R} = 0_{R}$
63	1 62 3	mulg0	$⊢ ((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B) \in S \to 0 \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) = 0_{R}$
64	61 63	syl	$⊢ φ \to 0 \underset{˙}{\cdot} (((N + 1 - (N + 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((N + 1) \underset{˙}{\times} B)) = 0_{R}$
65	53 59 64	3eqtrd	$⊢ φ \to \underset{k \in \{N + 1\}}{\sum_{R}} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = 0_{R}$
66	65	oveq2d	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} (\underset{k \in \{N + 1\}}{\sum_{R}}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} 0_{R}$
67		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
68		simpl	$⊢ (φ \land k \in (0 \dots N)) \to φ$
69		bccl2	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \in ℕ$
70	69	nnnn0d	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \in ℕ_{0}$
71	70	adantl	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ_{0}$
72		fzelp1	$⊢ k \in (0 \dots N) \to k \in (0 \dots N + 1)$
73	72 22	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to N + 1 - k \in ℕ_{0}$
74		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
75	74	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
76	68 71 73 75 25	syl13anc	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
77	76	ralrimiva	$⊢ φ \to \forall k \in (0 \dots N) (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
78	1 16 67 77	gsummptcl	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S$
79	1 4 62	mndrid	$⊢ (R \in Mnd \land {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S) \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} 0_{R} = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
80	29 78 79	syl2anc	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} 0_{R} = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
81	27 66 80	3eqtrd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
82	7	adantr	$⊢ (φ \land k \in (0 \dots N)) \to R \in SRing$
83	8	adantr	$⊢ (φ \land k \in (0 \dots N)) \to A \in S$
84	9	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in S$
85	10	adantr	$⊢ (φ \land k \in (0 \dots N)) \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
86		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
87	86	adantl	$⊢ (φ \land k \in (0 \dots N)) \to N - k \in ℕ_{0}$
88	1 2 5 6 82 83 84 75 85 87 3 71	srgpcomppsc	$⊢ (φ \land k \in (0 \dots N)) \to ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} A = (\binom{N}{k}) \underset{˙}{\cdot} (((N - k + 1) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))$
89	36	adantr	$⊢ (φ \land k \in (0 \dots N)) \to N \in ℂ$
90		1cnd	$⊢ (φ \land k \in (0 \dots N)) \to 1 \in ℂ$
91		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
92	91	zcnd	$⊢ k \in (0 \dots N) \to k \in ℂ$
93	92	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℂ$
94	89 90 93	addsubd	$⊢ (φ \land k \in (0 \dots N)) \to N + 1 - k = N - k + 1$
95	94	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to (N + 1 - k) \underset{˙}{\times} A = (N - k + 1) \underset{˙}{\times} A$
96	95	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) = ((N - k + 1) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)$
97	96	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = (\binom{N}{k}) \underset{˙}{\cdot} (((N - k + 1) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))$
98	88 97	eqtr4d	$⊢ (φ \land k \in (0 \dots N)) \to ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} A = (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))$
99	98	mpteq2dva	$⊢ φ \to (k \in (0 \dots N) ⟼ ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} A) = (k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
100	99	oveq2d	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} A) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
101		ovexd	$⊢ φ \to (0 \dots N) \in V$
102	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	$⊢ (φ \land ((\binom{N}{k}) \in ℕ_{0} \land N - k \in ℕ_{0} \land k \in ℕ_{0})) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
103	68 71 87 75 102	syl13anc	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
104		eqid	$⊢ (k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
105		ovexd	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in V$
106		fvexd	$⊢ φ \to 0_{R} \in V$
107	104 67 105 106	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{R}} ((k \in (0 \dots N) ⟼ (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
108	1 62 4 2 7 101 8 103 107	srgsummulcr	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} A) = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} A$
109	81 100 108	3eqtr2rd	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} A = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
110	109	adantr	$⊢ (φ \land ψ) \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} A = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
111	14 110	eqtrd	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} A = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$

Metamath Proof Explorer

Theorem srgbinomlem3

Proof