Theorem srgbinomlem4

Description: Lemma 4 for srgbinomlem . (Contributed by AV, 24-Aug-2019) (Proof shortened by AV, 19-Nov-2019)

	Ref	Expression
Hypotheses	srgbinom.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
	srgbinom.m	⊢ × = ( .r ‘ 𝑅 )
	srgbinom.t	⊢ · = ( .g ‘ 𝑅 )
	srgbinom.a	⊢ + = ( +g ‘ 𝑅 )
	srgbinom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	srgbinom.e	⊢ ↑ = ( .g ‘ 𝐺 )
	srgbinomlem.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
	srgbinomlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	srgbinomlem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	srgbinomlem.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
	srgbinomlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	srgbinomlem.i	⊢ ( 𝜓 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
Assertion	srgbinomlem4	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
2		srgbinom.m	⊢ × = ( .r ‘ 𝑅 )
3		srgbinom.t	⊢ · = ( .g ‘ 𝑅 )
4		srgbinom.a	⊢ + = ( +g ‘ 𝑅 )
5		srgbinom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6		srgbinom.e	⊢ ↑ = ( .g ‘ 𝐺 )
7		srgbinomlem.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
8		srgbinomlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
9		srgbinomlem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
10		srgbinomlem.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
11		srgbinomlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12		srgbinomlem.i	⊢ ( 𝜓 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
13	12	oveq1d	⊢ ( 𝜓 → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐵 ) )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
16		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
17		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
18		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
19	11 17 18	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
20		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
22		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
24	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	⊢ ( ( 𝜑 ∧ ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( 𝑁 − 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
25	16 19 21 23 24	syl13anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
26		eqid	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
27		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
28		ovexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ V )
29		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
30	26 27 28 29	fsuppmptdm	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
31	1 14 4 2 7 15 9 25 30	srgsummulcr	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐵 ) )
32		srgcmn	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
33	7 32	syl	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
34		1z	⊢ 1 ∈ ℤ
35	34	a1i	⊢ ( 𝜑 → 1 ∈ ℤ )
36		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
37	11	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
38	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑅 ∈ SRing )
39	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ 𝑆 )
40	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ∈ 𝑆 )
41	38 25 39 40	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ∈ 𝑆 )
42		oveq2	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑁 C 𝑘 ) = ( 𝑁 C ( 𝑗 − 1 ) ) )
43		oveq2	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑁 − 𝑘 ) = ( 𝑁 − ( 𝑗 − 1 ) ) )
44	43	oveq1d	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) = ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) )
45		oveq1	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑘 ↑ 𝐵 ) = ( ( 𝑗 − 1 ) ↑ 𝐵 ) )
46	44 45	oveq12d	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) )
47	42 46	oveq12d	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
48	47	oveq1d	⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) )
49	1 14 33 35 36 37 41 48	gsummptshft	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) ) ) )
50	11	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℂ )
52		elfzelz	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℤ )
53	52	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ℤ )
54	53	zcnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ℂ )
55		1cnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
56	51 54 55	subsub3d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − ( 𝑗 − 1 ) ) = ( ( 𝑁 + 1 ) − 𝑗 ) )
57	56	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) )
58	57	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) = ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) )
59	58	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
60	59	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) )
61	7	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ SRing )
62		peano2zm	⊢ ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ℤ )
63	52 62	syl	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℤ )
64		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑗 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑗 − 1 ) ) ∈ ℕ0 )
65	11 63 64	syl2an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑗 − 1 ) ) ∈ ℕ0 )
66	5 1	mgpbas	⊢ 𝑆 = ( Base ‘ 𝐺 )
67	5	srgmgp	⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
68	7 67	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
70		0p1e1	⊢ ( 0 + 1 ) = 1
71	70	oveq1i	⊢ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
72	71	eleq2i	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↔ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
73		fznn0sub	⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 )
74	73	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 ) )
75	72 74	biimtrid	⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 ) )
76	75	imp	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 )
77	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
78	66 6 69 76 77	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 )
79		elfznn	⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℕ )
80		nnm1nn0	⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
81	79 80	syl	⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
82	72 81	sylbi	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
83	82	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
84	9	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
85	66 6 69 83 84	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 )
86	1 3 2	srgmulgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 C ( 𝑗 − 1 ) ) ∈ ℕ0 ∧ ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
87	61 65 78 85 86	syl13anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
88	87	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) )
89	88	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) )
90		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
91	7 90	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
92	91	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ Mnd )
93	1 3 92 65 78	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) ∈ 𝑆 )
94	1 2	srgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) ∈ 𝑆 ∧ ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) )
95	61 93 85 84 94	syl13anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) )
96	5 2	mgpplusg	⊢ × = ( +g ‘ 𝐺 )
97	66 6 96	mulgnn0p1	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑗 − 1 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) = ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) )
98	97	eqcomd	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑗 − 1 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) = ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) )
99	69 83 84 98	syl3anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) = ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) )
100	99	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) ) )
101	52	zcnd	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℂ )
102		1cnd	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 1 ∈ ℂ )
103	101 102	npcand	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
104	103	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
105	104	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) = ( 𝑗 ↑ 𝐵 ) )
106	105	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
107	95 100 106	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
108	60 89 107	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
109	108	mpteq2dva	⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) ) = ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) )
110	109	oveq2d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) )
111	71	mpteq1i	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
112		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 − 1 ) = ( 𝑘 − 1 ) )
113	112	oveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑁 C ( 𝑗 − 1 ) ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
114		oveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 + 1 ) − 𝑗 ) = ( ( 𝑁 + 1 ) − 𝑘 ) )
115	114	oveq1d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) )
116	113 115	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) )
117		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 ↑ 𝐵 ) = ( 𝑘 ↑ 𝐵 ) )
118	116 117	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
119	118	cbvmptv	⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
120	111 119	eqtri	⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
121	120	oveq2i	⊢ ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) )
122		fzfid	⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
123		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
124		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
125		peano2zm	⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
126	124 125	syl	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
127		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
128	11 126 127	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
129		fznn0sub	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
130	129	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
131		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ )
132	131	nnnn0d	⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
133	132	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
134	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	⊢ ( ( 𝜑 ∧ ( ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
135	123 128 130 133 134	syl13anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
136	135	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
137	1 33 122 136	gsummptcl	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 )
138	1 4 14	mndlid	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 ) → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
139	91 137 138	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
140		0nn0	⊢ 0 ∈ ℕ0
141	140	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
142		id	⊢ ( 𝜑 → 𝜑 )
143		0z	⊢ 0 ∈ ℤ
144	143 34	pm3.2i	⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ )
145		zsubcl	⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 − 1 ) ∈ ℤ )
146	144 145	mp1i	⊢ ( 𝜑 → ( 0 − 1 ) ∈ ℤ )
147		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 0 − 1 ) ) ∈ ℕ0 )
148	11 146 147	syl2anc	⊢ ( 𝜑 → ( 𝑁 C ( 0 − 1 ) ) ∈ ℕ0 )
149		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
150		peano2cn	⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
151	149 150	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
152	151	subid1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 0 ) = ( 𝑁 + 1 ) )
153		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
154	152 153	eqeltrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 )
155	11 154	syl	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 )
156	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem2	⊢ ( ( 𝜑 ∧ ( ( 𝑁 C ( 0 − 1 ) ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) ) → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
157	142 148 155 141 156	syl13anc	⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
158		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
159	158	oveq2d	⊢ ( 𝑘 = 0 → ( 𝑁 C ( 𝑘 − 1 ) ) = ( 𝑁 C ( 0 − 1 ) ) )
160		oveq2	⊢ ( 𝑘 = 0 → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 + 1 ) − 0 ) )
161	160	oveq1d	⊢ ( 𝑘 = 0 → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) )
162		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 ↑ 𝐵 ) = ( 0 ↑ 𝐵 ) )
163	161 162	oveq12d	⊢ ( 𝑘 = 0 → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) )
164	159 163	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
165	1 164	gsumsn	⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
166	91 141 157 165	syl3anc	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
167		0lt1	⊢ 0 < 1
168	167	a1i	⊢ ( 𝜑 → 0 < 1 )
169	168 70	breqtrrdi	⊢ ( 𝜑 → 0 < ( 0 + 1 ) )
170		0re	⊢ 0 ∈ ℝ
171		1re	⊢ 1 ∈ ℝ
172	170 171 170	3pm3.2i	⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ )
173		ltsubadd	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 − 1 ) < 0 ↔ 0 < ( 0 + 1 ) ) )
174	172 173	mp1i	⊢ ( 𝜑 → ( ( 0 − 1 ) < 0 ↔ 0 < ( 0 + 1 ) ) )
175	169 174	mpbird	⊢ ( 𝜑 → ( 0 − 1 ) < 0 )
176	175	orcd	⊢ ( 𝜑 → ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) ) )
177		bcval4	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ∧ ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) ) ) → ( 𝑁 C ( 0 − 1 ) ) = 0 )
178	11 146 176 177	syl3anc	⊢ ( 𝜑 → ( 𝑁 C ( 0 − 1 ) ) = 0 )
179	178	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
180	66 6 68 155 8	mulgnn0cld	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) ∈ 𝑆 )
181	66 6 68 141 9	mulgnn0cld	⊢ ( 𝜑 → ( 0 ↑ 𝐵 ) ∈ 𝑆 )
182	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 0 ↑ 𝐵 ) ∈ 𝑆 ) → ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 )
183	7 180 181 182	syl3anc	⊢ ( 𝜑 → ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 )
184	1 14 3	mulg0	⊢ ( ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 → ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
185	183 184	syl	⊢ ( 𝜑 → ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
186	166 179 185	3eqtrrd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
187	186	oveq1d	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
188	139 187	eqtr3d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
189	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ SRing )
190	68	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
191	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
192	66 6 190 130 191	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
193	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
194	66 6 190 133 193	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
195	1 3 2	srgmulgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
196	189 128 192 194 195	syl13anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
197	196	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
198	197	oveq2d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
199	11 153	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
200		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
201		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
202	201 125	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
203	11 202 127	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
204		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
205	204	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
206		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
207	206	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
208	200 203 205 207 134	syl13anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
209	1 4 33 199 208	gsummptfzsplitl	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
210		snfi	⊢ { 0 } ∈ Fin
211	210	a1i	⊢ ( 𝜑 → { 0 } ∈ Fin )
212	164	eleq1d	⊢ ( 𝑘 = 0 → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) )
213	212	ralsng	⊢ ( 0 ∈ ℕ0 → ( ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) )
214	140 213	ax-mp	⊢ ( ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
215	157 214	sylibr	⊢ ( 𝜑 → ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
216	1 33 211 215	gsummptcl	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 )
217	1 4	cmncom	⊢ ( ( 𝑅 ∈ CMnd ∧ ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 ∧ ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 ) → ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
218	33 137 216 217	syl3anc	⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
219	209 218	eqtrd	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
220	188 198 219	3eqtr4d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
221	121 220	eqtrid	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
222	49 110 221	3eqtrd	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
223	31 222	eqtr3d	⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
224	13 223	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )