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	srgmgp	$⊢ R \in SRing \to G \in Mnd$
67	7 66	syl	$⊢ φ \to G \in Mnd$
68	67	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to G \in Mnd$
69		0p1e1	$⊢ 0 + 1 = 1$
70	69	oveq1i	$⊢ (0 + 1 \dots N + 1) = (1 \dots N + 1)$
71	70	eleq2i	$⊢ j \in (0 + 1 \dots N + 1) \leftrightarrow j \in (1 \dots N + 1)$
72		fznn0sub	$⊢ j \in (1 \dots N + 1) \to N + 1 - j \in ℕ_{0}$
73	72	a1i	$⊢ φ \to (j \in (1 \dots N + 1) \to N + 1 - j \in ℕ_{0})$
74	71 73	syl5bi	$⊢ φ \to (j \in (0 + 1 \dots N + 1) \to N + 1 - j \in ℕ_{0})$
75	74	imp	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to N + 1 - j \in ℕ_{0}$
76	8	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to A \in S$
77	5 1	mgpbas	$⊢ S = {Base}_{G}$
78	77 6	mulgnn0cl	$⊢ (G \in Mnd \land N + 1 - j \in ℕ_{0} \land A \in S) \to (N + 1 - j) \underset{˙}{\times} A \in S$
79	68 75 76 78	syl3anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (N + 1 - j) \underset{˙}{\times} A \in S$
80		elfznn	$⊢ j \in (1 \dots N + 1) \to j \in ℕ$
81		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
82	80 81	syl	$⊢ j \in (1 \dots N + 1) \to j - 1 \in ℕ_{0}$
83	71 82	sylbi	$⊢ j \in (0 + 1 \dots N + 1) \to j - 1 \in ℕ_{0}$
84	83	adantl	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j - 1 \in ℕ_{0}$
85	9	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to B \in S$
86	77 6	mulgnn0cl	$⊢ (G \in Mnd \land j - 1 \in ℕ_{0} \land B \in S) \to (j - 1) \underset{˙}{\times} B \in S$
87	68 84 85 86	syl3anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (j - 1) \underset{˙}{\times} B \in S$
88	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))$
89	61 65 79 87 88	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))$
90	89	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)$
91	90	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$
92		srgmnd	$⊢ R \in SRing \to R \in Mnd$
93	7 92	syl	$⊢ φ \to R \in Mnd$
94	93	adantr	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to R \in Mnd$
95	1 3	mulgnn0cl	$⊢ (R \in Mnd \land (\binom{N}{j - 1}) \in ℕ_{0} \land (N + 1 - j) \underset{˙}{\times} A \in S) \to (\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A) \in S$
96	94 65 79 95	syl3anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (\binom{N}{j - 1}) \underset{˙}{\cdot} ((N + 1 - j) \underset{˙}{\times} A) \in S$
97	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)$
98	61 96 87 85 97	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)$
99	5 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
100	77 6 99	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$
101	100	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$
102	68 84 85 101	syl3anc	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to ((j - 1) \underset{˙}{\times} B) \underset{˙}{\times} B = (j - 1 + 1) \underset{˙}{\times} B$
103	102	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)$
104	52	zcnd	$⊢ j \in (0 + 1 \dots N + 1) \to j \in ℂ$
105		1cnd	$⊢ j \in (0 + 1 \dots N + 1) \to 1 \in ℂ$
106	104 105	npcand	$⊢ j \in (0 + 1 \dots N + 1) \to j - 1 + 1 = j$
107	106	adantl	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to j - 1 + 1 = j$
108	107	oveq1d	$⊢ (φ \land j \in (0 + 1 \dots N + 1)) \to (j - 1 + 1) \underset{˙}{\times} B = j \underset{˙}{\times} B$
109	108	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)$
110	98 103 109	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)$
111	60 91 110	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)$
112	111	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))$
113	112	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))$
114	70	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))$
115		oveq1	$⊢ j = k \to j - 1 = k - 1$
116	115	oveq2d	$⊢ j = k \to (\binom{N}{j - 1}) = (\binom{N}{k - 1})$
117		oveq2	$⊢ j = k \to N + 1 - j = N + 1 - k$
118	117	oveq1d	$⊢ j = k \to (N + 1 - j) \underset{˙}{\times} A = (N + 1 - k) \underset{˙}{\times} A$
119	116 118	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)$
120		oveq1	$⊢ j = k \to j \underset{˙}{\times} B = k \underset{˙}{\times} B$
121	119 120	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)$
122	121	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))$
123	114 122	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))$
124	123	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))$
125		fzfid	$⊢ φ \to (1 \dots N + 1) \in Fin$
126		simpl	$⊢ (φ \land k \in (1 \dots N + 1)) \to φ$
127		elfzelz	$⊢ k \in (1 \dots N + 1) \to k \in ℤ$
128		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
129	127 128	syl	$⊢ k \in (1 \dots N + 1) \to k - 1 \in ℤ$
130		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
131	11 129 130	syl2an	$⊢ (φ \land k \in (1 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
132		fznn0sub	$⊢ k \in (1 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
133	132	adantl	$⊢ (φ \land k \in (1 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
134		elfznn	$⊢ k \in (1 \dots N + 1) \to k \in ℕ$
135	134	nnnn0d	$⊢ k \in (1 \dots N + 1) \to k \in ℕ_{0}$
136	135	adantl	$⊢ (φ \land k \in (1 \dots N + 1)) \to k \in ℕ_{0}$
137	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$
138	126 131 133 136 137	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$
139	138	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$
140	1 33 125 139	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$
141	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)))$
142	93 140 141	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)))$
143		0nn0	$⊢ 0 \in ℕ_{0}$
144	143	a1i	$⊢ φ \to 0 \in ℕ_{0}$
145		id	$⊢ φ \to φ$
146		0z	$⊢ 0 \in ℤ$
147	146 34	pm3.2i	$⊢ (0 \in ℤ \land 1 \in ℤ)$
148		zsubcl	$⊢ (0 \in ℤ \land 1 \in ℤ) \to 0 - 1 \in ℤ$
149	147 148	mp1i	$⊢ φ \to 0 - 1 \in ℤ$
150		bccl	$⊢ (N \in ℕ_{0} \land 0 - 1 \in ℤ) \to (\binom{N}{0 - 1}) \in ℕ_{0}$
151	11 149 150	syl2anc	$⊢ φ \to (\binom{N}{0 - 1}) \in ℕ_{0}$
152		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
153		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
154	152 153	syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
155	154	subid1d	$⊢ N \in ℕ_{0} \to N + 1 - 0 = N + 1$
156		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
157	155 156	eqeltrd	$⊢ N \in ℕ_{0} \to N + 1 - 0 \in ℕ_{0}$
158	11 157	syl	$⊢ φ \to N + 1 - 0 \in ℕ_{0}$
159	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$
160	145 151 158 144 159	syl13anc	$⊢ φ \to (\binom{N}{0 - 1}) \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) \in S$
161		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
162	161	oveq2d	$⊢ k = 0 \to (\binom{N}{k - 1}) = (\binom{N}{0 - 1})$
163		oveq2	$⊢ k = 0 \to N + 1 - k = N + 1 - 0$
164	163	oveq1d	$⊢ k = 0 \to (N + 1 - k) \underset{˙}{\times} A = (N + 1 - 0) \underset{˙}{\times} A$
165		oveq1	$⊢ k = 0 \to k \underset{˙}{\times} B = 0 \underset{˙}{\times} B$
166	164 165	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)$
167	162 166	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))$
168	1 167	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))$
169	93 144 160 168	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))$
170		0lt1	$⊢ 0 < 1$
171	170	a1i	$⊢ φ \to 0 < 1$
172	171 69	breqtrrdi	$⊢ φ \to 0 < 0 + 1$
173		0re	$⊢ 0 \in ℝ$
174		1re	$⊢ 1 \in ℝ$
175	173 174 173	3pm3.2i	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \in ℝ)$
176		ltsubadd	$⊢ (0 \in ℝ \land 1 \in ℝ \land 0 \in ℝ) \to (0 - 1 < 0 \leftrightarrow 0 < 0 + 1)$
177	175 176	mp1i	$⊢ φ \to (0 - 1 < 0 \leftrightarrow 0 < 0 + 1)$
178	172 177	mpbird	$⊢ φ \to 0 - 1 < 0$
179	178	orcd	$⊢ φ \to (0 - 1 < 0 \lor N < 0 - 1)$
180		bcval4	$⊢ (N \in ℕ_{0} \land 0 - 1 \in ℤ \land (0 - 1 < 0 \lor N < 0 - 1)) \to (\binom{N}{0 - 1}) = 0$
181	11 149 179 180	syl3anc	$⊢ φ \to (\binom{N}{0 - 1}) = 0$
182	181	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))$
183	77 6	mulgnn0cl	$⊢ (G \in Mnd \land N + 1 - 0 \in ℕ_{0} \land A \in S) \to (N + 1 - 0) \underset{˙}{\times} A \in S$
184	67 158 8 183	syl3anc	$⊢ φ \to (N + 1 - 0) \underset{˙}{\times} A \in S$
185	77 6	mulgnn0cl	$⊢ (G \in Mnd \land 0 \in ℕ_{0} \land B \in S) \to 0 \underset{˙}{\times} B \in S$
186	67 144 9 185	syl3anc	$⊢ φ \to 0 \underset{˙}{\times} B \in S$
187	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$
188	7 184 186 187	syl3anc	$⊢ φ \to ((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B) \in S$
189	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}$
190	188 189	syl	$⊢ φ \to 0 \underset{˙}{\cdot} (((N + 1 - 0) \underset{˙}{\times} A) \underset{˙}{\times} (0 \underset{˙}{\times} B)) = 0_{R}$
191	169 182 190	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)))$
192	191	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))))$
193	142 192	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))))$
194	7	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to R \in SRing$
195	67	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to G \in Mnd$
196	8	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to A \in S$
197	77 6	mulgnn0cl	$⊢ (G \in Mnd \land N + 1 - k \in ℕ_{0} \land A \in S) \to (N + 1 - k) \underset{˙}{\times} A \in S$
198	195 133 196 197	syl3anc	$⊢ (φ \land k \in (1 \dots N + 1)) \to (N + 1 - k) \underset{˙}{\times} A \in S$
199	9	adantr	$⊢ (φ \land k \in (1 \dots N + 1)) \to B \in S$
200	77 6	mulgnn0cl	$⊢ (G \in Mnd \land k \in ℕ_{0} \land B \in S) \to k \underset{˙}{\times} B \in S$
201	195 136 199 200	syl3anc	$⊢ (φ \land k \in (1 \dots N + 1)) \to k \underset{˙}{\times} B \in S$
202	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))$
203	194 131 198 201 202	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))$
204	203	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)))$
205	204	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)))$
206	11 156	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
207		simpl	$⊢ (φ \land k \in (0 \dots N + 1)) \to φ$
208		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
209	208 128	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
210	11 209 130	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
211		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
212	211	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℕ_{0}$
213		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
214	213	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℕ_{0}$
215	207 210 212 214 137	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$
216	1 4 33 206 215	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))))$
217		snfi	$⊢ \{0\} \in Fin$
218	217	a1i	$⊢ φ \to \{0\} \in Fin$
219	167	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)$
220	219	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)$
221	143 220	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$
222	160 221	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$
223	1 33 218 222	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$
224	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))))$
225	33 140 223 224	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))))$
226	216 225	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))))$
227	193 205 226	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)))$
228	124 227	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)))$
229	49 113 228	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)))$
230	31 229	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)))$
231	13 230	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