This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )