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 syl5eq ( 𝜑 → ( 𝑅 Σ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 ) − 𝑘 ) 𝐴 ) × ( 𝑘 𝐵 ) ) ) ) ) )