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 srgmgp ⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
67 7 66 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
69 0p1e1 ⊢ ( 0 + 1 ) = 1
70 69 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
71 70 eleq2i ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↔ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
72 fznn0sub ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 )
73 72 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 ) )
74 71 73 syl5bi ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 ) )
75 74 imp ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 )
76 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
77 5 1 mgpbas ⊢ 𝑆 = ( Base ‘ 𝐺 )
78 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 + 1 ) − 𝑗 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 )
79 68 75 76 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 )
80 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℕ )
81 nnm1nn0 ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
82 80 81 syl ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
83 71 82 sylbi ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
85 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
86 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑗 − 1 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 )
87 68 84 85 86 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 )
88 1 3 2 srgmulgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 C ( 𝑗 − 1 ) ) ∈ ℕ0 ∧ ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
89 61 65 79 87 88 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) )
90 89 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) )
91 90 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) )
92 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
93 7 92 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ Mnd )
95 1 3 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑁 C ( 𝑗 − 1 ) ) ∈ ℕ0 ∧ ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ∈ 𝑆 ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) ∈ 𝑆 )
96 94 65 79 95 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) ∈ 𝑆 )
97 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) ∈ 𝑆 ∧ ( ( 𝑗 − 1 ) ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) )
98 61 96 87 85 97 syl13anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) )
99 5 2 mgpplusg ⊢ × = ( +g ‘ 𝐺 )
100 77 6 99 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑗 − 1 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) = ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) )
101 100 eqcomd ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑗 − 1 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) = ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) )
102 68 84 85 101 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) = ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) )
103 102 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) ↑ 𝐵 ) × 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) ) )
104 52 zcnd ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℂ )
105 1cnd ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 1 ∈ ℂ )
106 104 105 npcand ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
108 107 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) = ( 𝑗 ↑ 𝐵 ) )
109 108 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( ( 𝑗 − 1 ) + 1 ) ↑ 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
110 98 103 109 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
111 60 91 110 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) = ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
112 111 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) ) = ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) )
113 112 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 − ( 𝑗 − 1 ) ) ↑ 𝐴 ) × ( ( 𝑗 − 1 ) ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) )
114 70 mpteq1i ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) )
115 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 − 1 ) = ( 𝑘 − 1 ) )
116 115 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑁 C ( 𝑗 − 1 ) ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
117 oveq2 ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 + 1 ) − 𝑗 ) = ( ( 𝑁 + 1 ) − 𝑘 ) )
118 117 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) )
119 116 118 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) )
120 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ↑ 𝐵 ) = ( 𝑘 ↑ 𝐵 ) )
121 119 120 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
122 121 cbvmptv ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
123 114 122 eqtri ⊢ ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) )
124 123 oveq2i ⊢ ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) )
125 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
126 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
127 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
128 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
129 127 128 syl ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
130 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
131 11 129 130 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
132 fznn0sub ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
134 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ )
135 134 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
136 135 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
137 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
138 126 131 133 136 137 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
139 138 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
140 1 33 125 139 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 )
141 1 4 14 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 ) → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
142 93 140 141 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
143 0nn0 ⊢ 0 ∈ ℕ0
144 143 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
145 id ⊢ ( 𝜑 → 𝜑 )
146 0z ⊢ 0 ∈ ℤ
147 146 34 pm3.2i ⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ )
148 zsubcl ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 − 1 ) ∈ ℤ )
149 147 148 mp1i ⊢ ( 𝜑 → ( 0 − 1 ) ∈ ℤ )
150 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 0 − 1 ) ) ∈ ℕ0 )
151 11 149 150 syl2anc ⊢ ( 𝜑 → ( 𝑁 C ( 0 − 1 ) ) ∈ ℕ0 )
152 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
153 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
154 152 153 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ )
155 154 subid1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 0 ) = ( 𝑁 + 1 ) )
156 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
157 155 156 eqeltrd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 )
158 11 157 syl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 )
159 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 ↑ 𝐵 ) ) ) ∈ 𝑆 )
160 145 151 158 144 159 syl13anc ⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
161 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
162 161 oveq2d ⊢ ( 𝑘 = 0 → ( 𝑁 C ( 𝑘 − 1 ) ) = ( 𝑁 C ( 0 − 1 ) ) )
163 oveq2 ⊢ ( 𝑘 = 0 → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 + 1 ) − 0 ) )
164 163 oveq1d ⊢ ( 𝑘 = 0 → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) = ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) )
165 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ↑ 𝐵 ) = ( 0 ↑ 𝐵 ) )
166 164 165 oveq12d ⊢ ( 𝑘 = 0 → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) )
167 162 166 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
168 1 167 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
169 93 144 160 168 syl3anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
170 0lt1 ⊢ 0 < 1
171 170 a1i ⊢ ( 𝜑 → 0 < 1 )
172 171 69 breqtrrdi ⊢ ( 𝜑 → 0 < ( 0 + 1 ) )
173 0re ⊢ 0 ∈ ℝ
174 1re ⊢ 1 ∈ ℝ
175 173 174 173 3pm3.2i ⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ )
176 ltsubadd ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 − 1 ) < 0 ↔ 0 < ( 0 + 1 ) ) )
177 175 176 mp1i ⊢ ( 𝜑 → ( ( 0 − 1 ) < 0 ↔ 0 < ( 0 + 1 ) ) )
178 172 177 mpbird ⊢ ( 𝜑 → ( 0 − 1 ) < 0 )
179 178 orcd ⊢ ( 𝜑 → ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) ) )
180 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ∧ ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) ) ) → ( 𝑁 C ( 0 − 1 ) ) = 0 )
181 11 149 179 180 syl3anc ⊢ ( 𝜑 → ( 𝑁 C ( 0 − 1 ) ) = 0 )
182 181 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) )
183 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 + 1 ) − 0 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) ∈ 𝑆 )
184 67 158 8 183 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) ∈ 𝑆 )
185 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( 0 ↑ 𝐵 ) ∈ 𝑆 )
186 67 144 9 185 syl3anc ⊢ ( 𝜑 → ( 0 ↑ 𝐵 ) ∈ 𝑆 )
187 1 2 srgcl ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 0 ↑ 𝐵 ) ∈ 𝑆 ) → ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 )
188 7 184 186 187 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 )
189 1 14 3 mulg0 ⊢ ( ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ∈ 𝑆 → ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
190 188 189 syl ⊢ ( 𝜑 → ( 0 · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) = ( 0g ‘ 𝑅 ) )
191 169 182 190 3eqtrrd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
192 191 oveq1d ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
193 142 192 eqtr3d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
194 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ SRing )
195 67 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
196 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
197 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
198 195 133 196 197 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
199 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
200 77 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
201 195 136 199 200 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
202 1 3 2 srgmulgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
203 194 131 198 201 202 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
204 203 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
205 204 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
206 11 156 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
207 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
208 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
209 208 128 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
210 11 209 130 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
211 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
212 211 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
213 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
214 213 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
215 207 210 212 214 137 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
216 1 4 33 206 215 gsummptfzsplitl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
217 snfi ⊢ { 0 } ∈ Fin
218 217 a1i ⊢ ( 𝜑 → { 0 } ∈ Fin )
219 167 eleq1d ⊢ ( 𝑘 = 0 → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) )
220 219 ralsng ⊢ ( 0 ∈ ℕ0 → ( ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 ) )
221 143 220 ax-mp ⊢ ( ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 ↔ ( ( 𝑁 C ( 0 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 0 ) ↑ 𝐴 ) × ( 0 ↑ 𝐵 ) ) ) ∈ 𝑆 )
222 160 221 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 0 } ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
223 1 33 218 222 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ∈ 𝑆 )
224 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 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
225 33 140 223 224 syl3anc ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
226 216 225 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 } ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
227 193 205 226 3eqtr4d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
228 124 227 eqtrid ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C ( 𝑗 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝑗 ) ↑ 𝐴 ) ) × ( 𝑗 ↑ 𝐵 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
229 49 113 228 3eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) × 𝐵 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
230 31 229 eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑁 − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
231 13 230 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )