srgbinomlem4

Description: Lemma 4 for srgbinomlem . (Contributed by AV, 24-Aug-2019) (Proof shortened by AV, 19-Nov-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	srgbinomlem4	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \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	oveq1d	$⊢ ψ \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} B$
14		eqid	$⊢ 0_{R} = 0_{R}$
15		ovexd	$⊢ φ \to (0 \dots N) \in V$
16		simpl	$⊢ (φ \land k \in (0 \dots N)) \to φ$
17		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
18		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
19	11 17 18	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ_{0}$
20		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
21	20	adantl	$⊢ (φ \land k \in (0 \dots N)) \to N - k \in ℕ_{0}$
22		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
23	22	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
24	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$
25	16 19 21 23 24	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$
26		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)))$
27		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
28		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$
29		fvexd	$⊢ φ \to 0_{R} \in V$
30	26 27 28 29	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))))$
31	1 14 4 2 7 15 9 25 30	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} B) = ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} B$
32		srgcmn	$⊢ R \in SRing \to R \in CMnd$
33	7 32	syl	$⊢ φ \to R \in CMnd$
34		1z	$⊢ 1 \in ℤ$
35	34	a1i	$⊢ φ \to 1 \in ℤ$
36		0zd	$⊢ φ \to 0 \in ℤ$
37	11	nn0zd	$⊢ φ \to N \in ℤ$
38	7	adantr	$⊢ (φ \land k \in (0 \dots N)) \to R \in SRing$
39	9	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in S$
40	1 2	srgcl	$⊢ (R \in SRing \land (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S \land B \in S) \to ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} B \in S$
41	38 25 39 40	syl3anc	$⊢ (φ \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} B \in S$
42		oveq2	$⊢ k = j - 1 \to (\binom{N}{k}) = (\binom{N}{j - 1})$
43		oveq2	$⊢ k = j - 1 \to N - k = N - (j - 1)$
44	43	oveq1d	$⊢ k = j - 1 \to (N - k) \underset{˙}{\times} A = (N - (j - 1)) \underset{˙}{\times} A$
45		oveq1	$⊢ k = j - 1 \to k \underset{˙}{\times} B = (j - 1) \underset{˙}{\times} B$
46	44 45	oveq12d	$⊢ k = j - 1 \to ((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) = ((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)$
47	42 46	oveq12d	$⊢ k = j - 1 \to (\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))$
48	47	oveq1d	$⊢ k = j - 1 \to ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B$
49	1 14 33 35 36 37 41 48	gsummptshft	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} B) = {\sum_{R}}_{j = 0 + 1}^{N + 1} (((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B)$
50	11	nn0cnd	$⊢ φ \to N \in ℂ$
51	50	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to N \in ℂ$
52		elfzelz	$⊢ j \in (0 + 1 \dots N + 1) \to j \in ℤ$
53	52	adantl	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j \in ℤ$
54	53	zcnd	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j \in ℂ$
55		1cnd	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to 1 \in ℂ$
56	51 54 55	subsub3d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to N - (j - 1) = N + 1 - j$
57	56	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (N - (j - 1)) \underset{˙}{\times} A = (N + 1 - j) \underset{˙}{\times} A$
58	57	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B) = ((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)$
59	58	oveq2d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) = (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))$
60	59	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B$
61	7	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to R \in SRing$
62		peano2zm	$⊢ j \in ℤ \to j - 1 \in ℤ$
63	52 62	syl	$⊢ j \in (0 + 1 \dots N + 1) \to j - 1 \in ℤ$
64		bccl	$⊢ (N \in ℕ_{0} \land j - 1 \in ℤ) \to (\binom{N}{j - 1}) \in ℕ_{0}$
65	11 63 64	syl2an	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (\binom{N}{j - 1}) \in ℕ_{0}$
66	5 1	mgpbas	$⊢ S = {Base}_{G}$
67	5	srgmgp	$⊢ R \in SRing \to G \in Mnd$
68	7 67	syl	$⊢ φ \to G \in Mnd$
69	68	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to G \in Mnd$
70		0p1e1	$⊢ 0 + 1 = 1$
71	70	oveq1i	$⊢ (0 + 1 \dots N + 1) = (1 \dots N + 1)$
72	71	eleq2i	$⊢ j \in (0 + 1 \dots N + 1) \leftrightarrow j \in (1 \dots N + 1)$
73		fznn0sub	$⊢ j \in (1 \dots N + 1) \to N + 1 - j \in ℕ_{0}$
74	73	a1i	$⊢ φ \to (j \in (1 \dots N + 1) \to N + 1 - j \in ℕ_{0})$
75	72 74	biimtrid	$⊢ φ \to (j \in (0 + 1 \dots N + 1) \to N + 1 - j \in ℕ_{0})$
76	75	imp	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to N + 1 - j \in ℕ_{0}$
77	8	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to A \in S$
78	66 6 69 76 77	mulgnn0cld	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (N + 1 - j) \underset{˙}{\times} A \in S$
79		elfznn	$⊢ j \in (1 \dots N + 1) \to j \in ℕ$
80		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
81	79 80	syl	$⊢ j \in (1 \dots N + 1) \to j - 1 \in ℕ_{0}$
82	72 81	sylbi	$⊢ j \in (0 + 1 \dots N + 1) \to j - 1 \in ℕ_{0}$
83	82	adantl	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j - 1 \in ℕ_{0}$
84	9	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to B \in S$
85	66 6 69 83 84	mulgnn0cld	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (j - 1) \underset{˙}{\times} B \in S$
86	1 3 2	srgmulgass	$⊢ (R \in SRing \land ((\binom{N}{j - 1}) \in ℕ_{0} \land (N + 1 - j) \underset{˙}{\times} A \in S \land (j - 1) \underset{˙}{\times} B \in S)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B) = (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))$
87	61 65 78 85 86	syl13anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B) = (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))$
88	87	eqcomd	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)$
89	88	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N + 1 - j) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B = (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) \underset{˙}{\times} B$
90		srgmnd	$⊢ R \in SRing \to R \in Mnd$
91	7 90	syl	$⊢ φ \to R \in Mnd$
92	91	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to R \in Mnd$
93	1 3 92 65 78	mulgnn0cld	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A) \in S$
94	1 2	srgass	$⊢ (R \in SRing \land ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A) \in S \land (j - 1) \underset{˙}{\times} B \in S \land B \in S)) \to (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B)$
95	61 93 85 84 94	syl13anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B)$
96	5 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
97	66 6 96	mulgnn0p1	$⊢ (G \in Mnd \land j - 1 \in ℕ_{0} \land B \in S) \to (j - 1 + 1) \underset{˙}{\times} B = ((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B$
98	97	eqcomd	$⊢ (G \in Mnd \land j - 1 \in ℕ_{0} \land B \in S) \to ((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B = (j - 1 + 1) \underset{˙}{\times} B$
99	69 83 84 98	syl3anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B = (j - 1 + 1) \underset{˙}{\times} B$
100	99	oveq2d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B) = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1 + 1) \underset{˙}{\times} B)$
101	52	zcnd	$⊢ j \in (0 + 1 \dots N + 1) \to j \in ℂ$
102		1cnd	$⊢ j \in (0 + 1 \dots N + 1) \to 1 \in ℂ$
103	101 102	npcand	$⊢ j \in (0 + 1 \dots N + 1) \to j - 1 + 1 = j$
104	103	adantl	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j - 1 + 1 = j$
105	104	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (j - 1 + 1) \underset{˙}{\times} B = j \underset{˙}{\times} B$
106	105	oveq2d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1 + 1) \underset{˙}{\times} B) = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)$
107	95 100 106	3eqtrd	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B)) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)$
108	60 89 107	3eqtrd	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B = ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)$
109	108	mpteq2dva	$⊢ φ \to (j \in (0 + 1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B) = (j \in (0 + 1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B))$
110	109	oveq2d	$⊢ φ \to {\sum_{R}}_{j = 0 + 1}^{N + 1} (((\binom{N}{j - 1}) \underset{˙}{\cdot} (((N - (j - 1)) \underset{˙}{\times} A) \underset{˙}{\times} ((j - 1) \underset{˙}{\times} B))) \underset{˙}{\times} B) = {\sum_{R}}_{j = 0 + 1}^{N + 1} (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B))$
111	71	mpteq1i	$⊢ (j \in (0 + 1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)) = (j \in (1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B))$
112		oveq1	$⊢ j = k \to j - 1 = k - 1$
113	112	oveq2d	$⊢ j = k \to (\binom{N}{j - 1}) = (\binom{N}{k - 1})$
114		oveq2	$⊢ j = k \to N + 1 - j = N + 1 - k$
115	114	oveq1d	$⊢ j = k \to (N + 1 - j) \underset{˙}{\times} A = (N + 1 - k) \underset{˙}{\times} A$
116	113 115	oveq12d	$⊢ j = k \to (\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A) = (\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)$
117		oveq1	$⊢ j = k \to j \underset{˙}{\times} B = k \underset{˙}{\times} B$
118	116 117	oveq12d	$⊢ j = k \to ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B) = ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B)$
119	118	cbvmptv	$⊢ (j \in (1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)) = (k \in (1 \dots N + 1) ⟼ ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B))$
120	111 119	eqtri	$⊢ (j \in (0 + 1 \dots N + 1) ⟼ ((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)) = (k \in (1 \dots N + 1) ⟼ ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B))$
121	120	oveq2i	$⊢ {\sum_{R}}_{j = 0 + 1}^{N + 1} (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)) = {\sum_{R}}_{k = 1}^{N + 1} (((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B))$
122		fzfid	$⊢ φ \to (1 \dots N + 1) \in Fin$
123		simpl	$⊢ (φ \land k \in (1 \dots N + 1)) \to φ$
124		elfzelz	$⊢ k \in (1 \dots N + 1) \to k \in ℤ$
125		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
126	124 125	syl	$⊢ k \in (1 \dots N + 1) \to k - 1 \in ℤ$
127		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
128	11 126 127	syl2an	$⊢ (φ \land k \in (1 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
129		fznn0sub	$⊢ k \in (1 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
130	129	adantl	$⊢ (φ \land k \in (1 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
131		elfznn	$⊢ k \in (1 \dots N + 1) \to k \in ℕ$
132	131	nnnn0d	$⊢ k \in (1 \dots N + 1) \to k \in ℕ_{0}$
133	132	adantl	$⊢ (φ \land k \in (1 \dots N + 1)) \to k \in ℕ_{0}$
134	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	$⊢ (φ \land ((\binom{N}{k - 1}) \in ℕ_{0} \land N + 1 - k \in ℕ_{0} \land k \in ℕ_{0})) \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
135	123 128 130 133 134	syl13anc	$⊢ (φ \land k \in (1 \dots N + 1)) \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
136	135	ralrimiva	$⊢ φ \to \forall k \in (1 \dots N + 1) (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
137	1 33 122 136	gsummptcl	$⊢ φ \to {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S$
138	1 4 14	mndlid	$⊢ (R \in Mnd \land {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S) \to 0_{R} \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
139	91 137 138	syl2anc	$⊢ φ \to 0_{R} \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
140		0nn0	$⊢ 0 \in ℕ_{0}$
141	140	a1i	$⊢ φ \to 0 \in ℕ_{0}$
142		id	$⊢ φ \to φ$
143		0z	$⊢ 0 \in ℤ$
144	143 34	pm3.2i	$⊢ (0 \in ℤ \land 1 \in ℤ)$
145		zsubcl	$⊢ (0 \in ℤ \land 1 \in ℤ) \to 0 - 1 \in ℤ$
146	144 145	mp1i	$⊢ φ \to 0 - 1 \in ℤ$
147		bccl	$⊢ (N \in ℕ_{0} \land 0 - 1 \in ℤ) \to (\binom{N}{0 - 1}) \in ℕ_{0}$
148	11 146 147	syl2anc	$⊢ φ \to (\binom{N}{0 - 1}) \in ℕ_{0}$
149		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
150		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
151	149 150	syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
152	151	subid1d	$⊢ N \in ℕ_{0} \to N + 1 - 0 = N + 1$
153		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
154	152 153	eqeltrd	$⊢ N \in ℕ_{0} \to N + 1 - 0 \in ℕ_{0}$
155	11 154	syl	$⊢ φ \to N + 1 - 0 \in ℕ_{0}$
156	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	$⊢ (φ \land ((\binom{N}{0 - 1}) \in ℕ_{0} \land N + 1 - 0 \in ℕ_{0} \land 0 \in ℕ_{0})) \to (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S$
157	142 148 155 141 156	syl13anc	$⊢ φ \to (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S$
158		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
159	158	oveq2d	$⊢ k = 0 \to (\binom{N}{k - 1}) = (\binom{N}{0 - 1})$
160		oveq2	$⊢ k = 0 \to N + 1 - k = N + 1 - 0$
161	160	oveq1d	$⊢ k = 0 \to (N + 1 - k) \underset{˙}{\times} A = (N + 1 - 0) \underset{˙}{\times} A$
162		oveq1	$⊢ k = 0 \to k \underset{˙}{\times} B = 0 \underset{˙}{\times} B$
163	161 162	oveq12d	$⊢ k = 0 \to ((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B) = ((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)$
164	159 163	oveq12d	$⊢ k = 0 \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) = (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B))$
165	1 164	gsumsn	$⊢ (R \in Mnd \land 0 \in ℕ_{0} \land (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S) \to \underset{k \in \{0\}}{\sum_{R}} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B))$
166	91 141 157 165	syl3anc	$⊢ φ \to \underset{k \in \{0\}}{\sum_{R}} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B))$
167		0lt1	$⊢ 0 < 1$
168	167	a1i	$⊢ φ \to 0 < 1$
169	168 70	breqtrrdi	$⊢ φ \to 0 < 0 + 1$
170		0re	$⊢ 0 \in ℝ$
171		1re	$⊢ 1 \in ℝ$
172	170 171 170	3pm3.2i	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \in ℝ)$
173		ltsubadd	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \in ℝ) \to (0 - 1 < 0 \leftrightarrow 0 < 0 + 1)$
174	172 173	mp1i	$⊢ φ \to (0 - 1 < 0 \leftrightarrow 0 < 0 + 1)$
175	169 174	mpbird	$⊢ φ \to 0 - 1 < 0$
176	175	orcd	$⊢ φ \to (0 - 1 < 0 \lor N < 0 - 1)$
177		bcval4	$⊢ (N \in ℕ_{0} \land 0 - 1 \in ℤ \land (0 - 1 < 0 \lor N < 0 - 1)) \to (\binom{N}{0 - 1}) = 0$
178	11 146 176 177	syl3anc	$⊢ φ \to (\binom{N}{0 - 1}) = 0$
179	178	oveq1d	$⊢ φ \to (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) = 0 \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B))$
180	66 6 68 155 8	mulgnn0cld	$⊢ φ \to (N + 1 - 0) \underset{˙}{\times} A \in S$
181	66 6 68 141 9	mulgnn0cld	$⊢ φ \to 0 \underset{˙}{\times} B \in S$
182	1 2	srgcl	$⊢ (R \in SRing \land (N + 1 - 0) \underset{˙}{\times} A \in S \land 0 \underset{˙}{\times} B \in S) \to ((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B) \in S$
183	7 180 181 182	syl3anc	$⊢ φ \to ((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B) \in S$
184	1 14 3	mulg0	$⊢ ((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B) \in S \to 0 \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) = 0_{R}$
185	183 184	syl	$⊢ φ \to 0 \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) = 0_{R}$
186	166 179 185	3eqtrrd	$⊢ φ \to 0_{R} = \underset{k \in \{0\}}{\sum_{R}} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
187	186	oveq1d	$⊢ φ \to 0_{R} \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
188	139 187	eqtr3d	$⊢ φ \to {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
189	7	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to R \in SRing$
190	68	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to G \in Mnd$
191	8	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to A \in S$
192	66 6 190 130 191	mulgnn0cld	$⊢ (φ \land k \in (1 \dots N + 1)) \to (N + 1 - k) \underset{˙}{\times} A \in S$
193	9	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to B \in S$
194	66 6 190 133 193	mulgnn0cld	$⊢ (φ \land k \in (1 \dots N + 1)) \to k \underset{˙}{\times} B \in S$
195	1 3 2	srgmulgass	$⊢ (R \in SRing \land ((\binom{N}{k - 1}) \in ℕ_{0} \land (N + 1 - k) \underset{˙}{\times} A \in S \land k \underset{˙}{\times} B \in S)) \to ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B) = (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))$
196	189 128 192 194 195	syl13anc	$⊢ (φ \land k \in (1 \dots N + 1)) \to ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B) = (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))$
197	196	mpteq2dva	$⊢ φ \to (k \in (1 \dots N + 1) ⟼ ((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B)) = (k \in (1 \dots N + 1) ⟼ (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
198	197	oveq2d	$⊢ φ \to {\sum_{R}}_{k = 1}^{N + 1} (((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B)) = {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
199	11 153	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
200		simpl	$⊢ (φ \land k \in (0 \dots N + 1)) \to φ$
201		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
202	201 125	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
203	11 202 127	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
204		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
205	204	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
206		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
207	206	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
208	200 203 205 207 134	syl13anc	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
209	1 4 33 199 208	gsummptfzsplitl	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
210		snfi	$⊢ \{0\} \in Fin$
211	210	a1i	$⊢ φ \to \{0\} \in Fin$
212	164	eleq1d	$⊢ k = 0 \to ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S \leftrightarrow (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S)$
213	212	ralsng	$⊢ 0 \in ℕ_{0} \to (\forall k \in \{0\} (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S \leftrightarrow (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S)$
214	140 213	ax-mp	$⊢ \forall k \in \{0\} (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S \leftrightarrow (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S$
215	157 214	sylibr	$⊢ φ \to \forall k \in \{0\} (\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)) \in S$
216	1 33 211 215	gsummptcl	$⊢ φ \to \underset{k \in \{0\}}{\sum_{R}} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S$
217	1 4	cmncom	$⊢ (R \in CMnd \land {\sum_{R}}_{k = 1}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S \land \underset{k \in \{0\}}{\sum_{R}} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \in S) \to ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
218	33 137 216 217	syl3anc	$⊢ φ \to ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) = (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
219	209 218	eqtrd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) = (\underset{k \in \{0\}}{\sum_{R}}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{+} ({\sum_{R}}_{k = 1}^{N + 1}, ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))))$
220	188 198 219	3eqtr4d	$⊢ φ \to {\sum_{R}}_{k = 1}^{N + 1} (((\binom{N}{k - 1}) \underset{˙}{\cdot} ((N + 1 - k) \underset{˙}{\times} A)) \underset{˙}{\times} (k \underset{˙}{\times} B)) = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
221	121 220	eqtrid	$⊢ φ \to {\sum_{R}}_{j = 0 + 1}^{N + 1} (((\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A)) \underset{˙}{\times} (j \underset{˙}{\times} B)) = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
222	49 110 221	3eqtrd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B))) \underset{˙}{\times} B) = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
223	31 222	eqtr3d	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))) \underset{˙}{\times} B = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
224	13 223	sylan9eqr	$⊢ (φ \land ψ) \to (N \underset{˙}{\times} (A \underset{˙}{+} B)) \underset{˙}{\times} B = {\sum_{R}}_{k = 0}^{N + 1} ((\binom{N}{k - 1}) \underset{˙}{\cdot} (((N + 1 - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$

Metamath Proof Explorer

Theorem srgbinomlem4

Proof