MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  srgbinomlem4 Structured version   Visualization version   GIF version

Theorem srgbinomlem4 18312
Description: Lemma 4 for srgbinomlem 18313. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.)
Hypotheses
Ref Expression
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
Ref Expression
srgbinomlem4 ((𝜑𝜓) → ((𝑁 (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝑁   𝑅,𝑘   𝑆,𝑘   · ,𝑘   × ,𝑘   ,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜓(𝑘)   + (𝑘)   𝐺(𝑘)

Proof of Theorem srgbinomlem4
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 srgbinomlem.i . . 3 (𝜓 → (𝑁 (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))))))
21oveq1d 6542 . 2 (𝜓 → ((𝑁 (𝐴 + 𝐵)) × 𝐵) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))))) × 𝐵))
3 srgbinom.s . . . 4 𝑆 = (Base‘𝑅)
4 eqid 2609 . . . 4 (0g𝑅) = (0g𝑅)
5 srgbinom.a . . . 4 + = (+g𝑅)
6 srgbinom.m . . . 4 × = (.r𝑅)
7 srgbinomlem.r . . . 4 (𝜑𝑅 ∈ SRing)
8 ovex 6555 . . . . 5 (0...𝑁) ∈ V
98a1i 11 . . . 4 (𝜑 → (0...𝑁) ∈ V)
10 srgbinomlem.b . . . 4 (𝜑𝐵𝑆)
11 simpl 471 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → 𝜑)
12 srgbinomlem.n . . . . . 6 (𝜑𝑁 ∈ ℕ0)
13 elfzelz 12168 . . . . . 6 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
14 bccl 12926 . . . . . 6 ((𝑁 ∈ ℕ0𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ0)
1512, 13, 14syl2an 492 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℕ0)
16 fznn0sub 12199 . . . . . 6 (𝑘 ∈ (0...𝑁) → (𝑁𝑘) ∈ ℕ0)
1716adantl 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑁𝑘) ∈ ℕ0)
18 elfznn0 12257 . . . . . 6 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
1918adantl 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
20 srgbinom.t . . . . . 6 · = (.g𝑅)
21 srgbinom.g . . . . . 6 𝐺 = (mulGrp‘𝑅)
22 srgbinom.e . . . . . 6 = (.g𝐺)
23 srgbinomlem.a . . . . . 6 (𝜑𝐴𝑆)
24 srgbinomlem.c . . . . . 6 (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴))
253, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 18310 . . . . 5 ((𝜑 ∧ ((𝑁C𝑘) ∈ ℕ0 ∧ (𝑁𝑘) ∈ ℕ0𝑘 ∈ ℕ0)) → ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
2611, 15, 17, 19, 25syl13anc 1319 . . . 4 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
27 eqid 2609 . . . . 5 (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵)))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))))
28 fzfid 12589 . . . . 5 (𝜑 → (0...𝑁) ∈ Fin)
29 ovex 6555 . . . . . 6 ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) ∈ V
3029a1i 11 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) ∈ V)
31 fvex 6098 . . . . . 6 (0g𝑅) ∈ V
3231a1i 11 . . . . 5 (𝜑 → (0g𝑅) ∈ V)
3327, 28, 30, 32fsuppmptdm 8146 . . . 4 (𝜑 → (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵)))) finSupp (0g𝑅))
343, 4, 5, 6, 7, 9, 10, 26, 33srgsummulcr 18306 . . 3 (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵))) = ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))))) × 𝐵))
35 srgcmn 18277 . . . . . 6 (𝑅 ∈ SRing → 𝑅 ∈ CMnd)
367, 35syl 17 . . . . 5 (𝜑𝑅 ∈ CMnd)
37 1z 11240 . . . . . 6 1 ∈ ℤ
3837a1i 11 . . . . 5 (𝜑 → 1 ∈ ℤ)
39 0zd 11222 . . . . 5 (𝜑 → 0 ∈ ℤ)
4012nn0zd 11312 . . . . 5 (𝜑𝑁 ∈ ℤ)
417adantr 479 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑅 ∈ SRing)
4210adantr 479 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → 𝐵𝑆)
433, 6srgcl 18281 . . . . . 6 ((𝑅 ∈ SRing ∧ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆𝐵𝑆) → (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵) ∈ 𝑆)
4441, 26, 42, 43syl3anc 1317 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵) ∈ 𝑆)
45 oveq2 6535 . . . . . . 7 (𝑘 = (𝑗 − 1) → (𝑁C𝑘) = (𝑁C(𝑗 − 1)))
46 oveq2 6535 . . . . . . . . 9 (𝑘 = (𝑗 − 1) → (𝑁𝑘) = (𝑁 − (𝑗 − 1)))
4746oveq1d 6542 . . . . . . . 8 (𝑘 = (𝑗 − 1) → ((𝑁𝑘) 𝐴) = ((𝑁 − (𝑗 − 1)) 𝐴))
48 oveq1 6534 . . . . . . . 8 (𝑘 = (𝑗 − 1) → (𝑘 𝐵) = ((𝑗 − 1) 𝐵))
4947, 48oveq12d 6545 . . . . . . 7 (𝑘 = (𝑗 − 1) → (((𝑁𝑘) 𝐴) × (𝑘 𝐵)) = (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵)))
5045, 49oveq12d 6545 . . . . . 6 (𝑘 = (𝑗 − 1) → ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) = ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))))
5150oveq1d 6542 . . . . 5 (𝑘 = (𝑗 − 1) → (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵))
523, 4, 36, 38, 39, 40, 44, 51gsummptshft 18105 . . . 4 (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵))))
5312nn0cnd 11200 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
5453adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ)
55 elfzelz 12168 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℤ)
5655adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℤ)
5756zcnd 11315 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑗 ∈ ℂ)
58 1cnd 9912 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈ ℂ)
5954, 57, 58subsub3d 10273 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑗 − 1)) = ((𝑁 + 1) − 𝑗))
6059oveq1d 6542 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 − (𝑗 − 1)) 𝐴) = (((𝑁 + 1) − 𝑗) 𝐴))
6160oveq1d 6542 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵)) = ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵)))
6261oveq2d 6543 . . . . . . . 8 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))))
6362oveq1d 6542 . . . . . . 7 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵))
647adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ SRing)
65 peano2zm 11253 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
6655, 65syl 17 . . . . . . . . . . 11 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
67 bccl 12926 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑗 − 1) ∈ ℤ) → (𝑁C(𝑗 − 1)) ∈ ℕ0)
6812, 66, 67syl2an 492 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁C(𝑗 − 1)) ∈ ℕ0)
6921srgmgp 18279 . . . . . . . . . . . . 13 (𝑅 ∈ SRing → 𝐺 ∈ Mnd)
707, 69syl 17 . . . . . . . . . . . 12 (𝜑𝐺 ∈ Mnd)
7170adantr 479 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐺 ∈ Mnd)
72 0p1e1 10979 . . . . . . . . . . . . . . 15 (0 + 1) = 1
7372oveq1i 6537 . . . . . . . . . . . . . 14 ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
7473eleq2i 2679 . . . . . . . . . . . . 13 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↔ 𝑗 ∈ (1...(𝑁 + 1)))
75 fznn0sub 12199 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈ ℕ0)
7675a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈ ℕ0))
7774, 76syl5bi 230 . . . . . . . . . . . 12 (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁 + 1) − 𝑗) ∈ ℕ0))
7877imp 443 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁 + 1) − 𝑗) ∈ ℕ0)
7923adantr 479 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐴𝑆)
8021, 3mgpbas 18264 . . . . . . . . . . . 12 𝑆 = (Base‘𝐺)
8180, 22mulgnn0cl 17327 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑗) ∈ ℕ0𝐴𝑆) → (((𝑁 + 1) − 𝑗) 𝐴) ∈ 𝑆)
8271, 78, 79, 81syl3anc 1317 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁 + 1) − 𝑗) 𝐴) ∈ 𝑆)
83 elfznn 12196 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
84 nnm1nn0 11181 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
8583, 84syl 17 . . . . . . . . . . . . 13 (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ0)
8674, 85sylbi 205 . . . . . . . . . . . 12 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ0)
8786adantl 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ0)
8810adantr 479 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐵𝑆)
8980, 22mulgnn0cl 17327 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈ ℕ0𝐵𝑆) → ((𝑗 − 1) 𝐵) ∈ 𝑆)
9071, 87, 88, 89syl3anc 1317 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) 𝐵) ∈ 𝑆)
913, 20, 6srgmulgass 18300 . . . . . . . . . 10 ((𝑅 ∈ SRing ∧ ((𝑁C(𝑗 − 1)) ∈ ℕ0 ∧ (((𝑁 + 1) − 𝑗) 𝐴) ∈ 𝑆 ∧ ((𝑗 − 1) 𝐵) ∈ 𝑆)) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))))
9264, 68, 82, 90, 91syl13anc 1319 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) = ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))))
9392eqcomd 2615 . . . . . . . 8 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)))
9493oveq1d 6542 . . . . . . 7 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · ((((𝑁 + 1) − 𝑗) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵) = ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) × 𝐵))
95 srgmnd 18278 . . . . . . . . . . . 12 (𝑅 ∈ SRing → 𝑅 ∈ Mnd)
967, 95syl 17 . . . . . . . . . . 11 (𝜑𝑅 ∈ Mnd)
9796adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑅 ∈ Mnd)
983, 20mulgnn0cl 17327 . . . . . . . . . 10 ((𝑅 ∈ Mnd ∧ (𝑁C(𝑗 − 1)) ∈ ℕ0 ∧ (((𝑁 + 1) − 𝑗) 𝐴) ∈ 𝑆) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) ∈ 𝑆)
9997, 68, 82, 98syl3anc 1317 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) ∈ 𝑆)
1003, 6srgass 18282 . . . . . . . . 9 ((𝑅 ∈ SRing ∧ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) ∈ 𝑆 ∧ ((𝑗 − 1) 𝐵) ∈ 𝑆𝐵𝑆)) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (((𝑗 − 1) 𝐵) × 𝐵)))
10164, 99, 90, 88, 100syl13anc 1319 . . . . . . . 8 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (((𝑗 − 1) 𝐵) × 𝐵)))
10221, 6mgpplusg 18262 . . . . . . . . . . . 12 × = (+g𝐺)
10380, 22, 102mulgnn0p1 17321 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈ ℕ0𝐵𝑆) → (((𝑗 − 1) + 1) 𝐵) = (((𝑗 − 1) 𝐵) × 𝐵))
104103eqcomd 2615 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝑗 − 1) ∈ ℕ0𝐵𝑆) → (((𝑗 − 1) 𝐵) × 𝐵) = (((𝑗 − 1) + 1) 𝐵))
10571, 87, 88, 104syl3anc 1317 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) 𝐵) × 𝐵) = (((𝑗 − 1) + 1) 𝐵))
106105oveq2d 6543 . . . . . . . 8 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (((𝑗 − 1) 𝐵) × 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (((𝑗 − 1) + 1) 𝐵)))
10755zcnd 11315 . . . . . . . . . . . 12 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑗 ∈ ℂ)
108 1cnd 9912 . . . . . . . . . . . 12 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → 1 ∈ ℂ)
109107, 108npcand 10247 . . . . . . . . . . 11 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑗 − 1) + 1) = 𝑗)
110109adantl 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑗 − 1) + 1) = 𝑗)
111110oveq1d 6542 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑗 − 1) + 1) 𝐵) = (𝑗 𝐵))
112111oveq2d 6543 . . . . . . . 8 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (((𝑗 − 1) + 1) 𝐵)) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))
113101, 106, 1123eqtrd 2647 . . . . . . 7 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → ((((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × ((𝑗 − 1) 𝐵)) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))
11463, 94, 1133eqtrd 2647 . . . . . 6 ((𝜑𝑗 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵) = (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))
115114mpteq2dva 4666 . . . . 5 (𝜑 → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵)) = (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))))
116115oveq2d 6543 . . . 4 (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 − (𝑗 − 1)) 𝐴) × ((𝑗 − 1) 𝐵))) × 𝐵))) = (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))))
117 mpteq1 4659 . . . . . . . 8 (((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)) → (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))))
11873, 117ax-mp 5 . . . . . . 7 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))) = (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))
119 oveq1 6534 . . . . . . . . . . 11 (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
120119oveq2d 6543 . . . . . . . . . 10 (𝑗 = 𝑘 → (𝑁C(𝑗 − 1)) = (𝑁C(𝑘 − 1)))
121 oveq2 6535 . . . . . . . . . . 11 (𝑗 = 𝑘 → ((𝑁 + 1) − 𝑗) = ((𝑁 + 1) − 𝑘))
122121oveq1d 6542 . . . . . . . . . 10 (𝑗 = 𝑘 → (((𝑁 + 1) − 𝑗) 𝐴) = (((𝑁 + 1) − 𝑘) 𝐴))
123120, 122oveq12d 6545 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) = ((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)))
124 oveq1 6534 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 𝐵) = (𝑘 𝐵))
125123, 124oveq12d 6545 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)) = (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)))
126125cbvmptv 4672 . . . . . . 7 (𝑗 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)))
127118, 126eqtri 2631 . . . . . 6 (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)))
128127oveq2i 6538 . . . . 5 (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵))))
129 fzfid 12589 . . . . . . . . 9 (𝜑 → (1...(𝑁 + 1)) ∈ Fin)
130 simpl 471 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝜑)
131 elfzelz 12168 . . . . . . . . . . . . 13 (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℤ)
132 peano2zm 11253 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
133131, 132syl 17 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ)
134 bccl 12926 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑘 − 1) ∈ ℤ) → (𝑁C(𝑘 − 1)) ∈ ℕ0)
13512, 133, 134syl2an 492 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℕ0)
136 fznn0sub 12199 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈ ℕ0)
137136adantl 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈ ℕ0)
138 elfznn 12196 . . . . . . . . . . . . 13 (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ)
139138nnnn0d 11198 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ0)
140139adantl 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ0)
1413, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 18310 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0𝑘 ∈ ℕ0)) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
142130, 135, 137, 140, 141syl13anc 1319 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
143142ralrimiva 2948 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ (1...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
1443, 36, 129, 143gsummptcl 18135 . . . . . . . 8 (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) ∈ 𝑆)
1453, 5, 4mndlid 17080 . . . . . . . 8 ((𝑅 ∈ Mnd ∧ (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) ∈ 𝑆) → ((0g𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
14696, 144, 145syl2anc 690 . . . . . . 7 (𝜑 → ((0g𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
147 0nn0 11154 . . . . . . . . . . 11 0 ∈ ℕ0
148147a1i 11 . . . . . . . . . 10 (𝜑 → 0 ∈ ℕ0)
149 id 22 . . . . . . . . . . 11 (𝜑𝜑)
150 0z 11221 . . . . . . . . . . . . . 14 0 ∈ ℤ
151150, 37pm3.2i 469 . . . . . . . . . . . . 13 (0 ∈ ℤ ∧ 1 ∈ ℤ)
152 zsubcl 11252 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
153151, 152mp1i 13 . . . . . . . . . . . 12 (𝜑 → (0 − 1) ∈ ℤ)
154 bccl 12926 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (0 − 1) ∈ ℤ) → (𝑁C(0 − 1)) ∈ ℕ0)
15512, 153, 154syl2anc 690 . . . . . . . . . . 11 (𝜑 → (𝑁C(0 − 1)) ∈ ℕ0)
156 nn0cn 11149 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
157 peano2cn 10059 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
158156, 157syl 17 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
159158subid1d 10232 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → ((𝑁 + 1) − 0) = (𝑁 + 1))
160 peano2nn0 11180 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
161159, 160eqeltrd 2687 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → ((𝑁 + 1) − 0) ∈ ℕ0)
16212, 161syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑁 + 1) − 0) ∈ ℕ0)
1633, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 18310 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑁C(0 − 1)) ∈ ℕ0 ∧ ((𝑁 + 1) − 0) ∈ ℕ0 ∧ 0 ∈ ℕ0)) → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆)
164149, 155, 162, 148, 163syl13anc 1319 . . . . . . . . . 10 (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆)
165 oveq1 6534 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
166165oveq2d 6543 . . . . . . . . . . . 12 (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1)))
167 oveq2 6535 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((𝑁 + 1) − 𝑘) = ((𝑁 + 1) − 0))
168167oveq1d 6542 . . . . . . . . . . . . 13 (𝑘 = 0 → (((𝑁 + 1) − 𝑘) 𝐴) = (((𝑁 + 1) − 0) 𝐴))
169 oveq1 6534 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 𝐵) = (0 𝐵))
170168, 169oveq12d 6545 . . . . . . . . . . . 12 (𝑘 = 0 → ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)) = ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵)))
171166, 170oveq12d 6545 . . . . . . . . . . 11 (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))))
1723, 171gsumsn 18123 . . . . . . . . . 10 ((𝑅 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆) → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))))
17396, 148, 164, 172syl3anc 1317 . . . . . . . . 9 (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) = ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))))
174 0lt1 10399 . . . . . . . . . . . . . . 15 0 < 1
175174a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 1)
176175, 72syl6breqr 4619 . . . . . . . . . . . . 13 (𝜑 → 0 < (0 + 1))
177 0re 9896 . . . . . . . . . . . . . . 15 0 ∈ ℝ
178 1re 9895 . . . . . . . . . . . . . . 15 1 ∈ ℝ
179177, 178, 1773pm3.2i 1231 . . . . . . . . . . . . . 14 (0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ)
180 ltsubadd 10347 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 − 1) < 0 ↔ 0 < (0 + 1)))
181179, 180mp1i 13 . . . . . . . . . . . . 13 (𝜑 → ((0 − 1) < 0 ↔ 0 < (0 + 1)))
182176, 181mpbird 245 . . . . . . . . . . . 12 (𝜑 → (0 − 1) < 0)
183182orcd 405 . . . . . . . . . . 11 (𝜑 → ((0 − 1) < 0 ∨ 𝑁 < (0 − 1)))
184 bcval4 12911 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
18512, 153, 183, 184syl3anc 1317 . . . . . . . . . 10 (𝜑 → (𝑁C(0 − 1)) = 0)
186185oveq1d 6542 . . . . . . . . 9 (𝜑 → ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) = (0 · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))))
18780, 22mulgnn0cl 17327 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 0) ∈ ℕ0𝐴𝑆) → (((𝑁 + 1) − 0) 𝐴) ∈ 𝑆)
18870, 162, 23, 187syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (((𝑁 + 1) − 0) 𝐴) ∈ 𝑆)
18980, 22mulgnn0cl 17327 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 0 ∈ ℕ0𝐵𝑆) → (0 𝐵) ∈ 𝑆)
19070, 148, 10, 189syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (0 𝐵) ∈ 𝑆)
1913, 6srgcl 18281 . . . . . . . . . . 11 ((𝑅 ∈ SRing ∧ (((𝑁 + 1) − 0) 𝐴) ∈ 𝑆 ∧ (0 𝐵) ∈ 𝑆) → ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵)) ∈ 𝑆)
1927, 188, 190, 191syl3anc 1317 . . . . . . . . . 10 (𝜑 → ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵)) ∈ 𝑆)
1933, 4, 20mulg0 17315 . . . . . . . . . 10 (((((𝑁 + 1) − 0) 𝐴) × (0 𝐵)) ∈ 𝑆 → (0 · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) = (0g𝑅))
194192, 193syl 17 . . . . . . . . 9 (𝜑 → (0 · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) = (0g𝑅))
195173, 186, 1943eqtrrd 2648 . . . . . . . 8 (𝜑 → (0g𝑅) = (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
196195oveq1d 6542 . . . . . . 7 (𝜑 → ((0g𝑅) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
197146, 196eqtr3d 2645 . . . . . 6 (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
1987adantr 479 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝑅 ∈ SRing)
19970adantr 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝐺 ∈ Mnd)
20023adantr 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝐴𝑆)
20180, 22mulgnn0cl 17327 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ0𝐴𝑆) → (((𝑁 + 1) − 𝑘) 𝐴) ∈ 𝑆)
202199, 137, 200, 201syl3anc 1317 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁 + 1) − 𝑘) 𝐴) ∈ 𝑆)
20310adantr 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → 𝐵𝑆)
20480, 22mulgnn0cl 17327 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0𝐵𝑆) → (𝑘 𝐵) ∈ 𝑆)
205199, 140, 203, 204syl3anc 1317 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 𝐵) ∈ 𝑆)
2063, 20, 6srgmulgass 18300 . . . . . . . . 9 ((𝑅 ∈ SRing ∧ ((𝑁C(𝑘 − 1)) ∈ ℕ0 ∧ (((𝑁 + 1) − 𝑘) 𝐴) ∈ 𝑆 ∧ (𝑘 𝐵) ∈ 𝑆)) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))
207198, 135, 202, 205, 206syl13anc 1319 . . . . . . . 8 ((𝜑𝑘 ∈ (1...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)) = ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))
208207mpteq2dva 4666 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵))) = (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))
209208oveq2d 6543 . . . . . 6 (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)))) = (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
21012, 160syl 17 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℕ0)
211 simpl 471 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝜑)
212 elfzelz 12168 . . . . . . . . . . 11 (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ)
213212, 132syl 17 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ)
21412, 213, 134syl2an 492 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℕ0)
215 fznn0sub 12199 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈ ℕ0)
216215adantl 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈ ℕ0)
217 elfznn0 12257 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0)
218217adantl 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0)
219211, 214, 216, 218, 141syl13anc 1319 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
2203, 5, 36, 210, 219gsummptfzsplitl 18102 . . . . . . 7 (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) = ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
221 snfi 7900 . . . . . . . . . 10 {0} ∈ Fin
222221a1i 11 . . . . . . . . 9 (𝜑 → {0} ∈ Fin)
223171eleq1d 2671 . . . . . . . . . . . 12 (𝑘 = 0 → (((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆))
224223ralsng 4164 . . . . . . . . . . 11 (0 ∈ ℕ0 → (∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆))
225147, 224ax-mp 5 . . . . . . . . . 10 (∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆 ↔ ((𝑁C(0 − 1)) · ((((𝑁 + 1) − 0) 𝐴) × (0 𝐵))) ∈ 𝑆)
226164, 225sylibr 222 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ {0} ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))) ∈ 𝑆)
2273, 36, 222, 226gsummptcl 18135 . . . . . . . 8 (𝜑 → (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) ∈ 𝑆)
2283, 5cmncom 17978 . . . . . . . 8 ((𝑅 ∈ 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) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
22936, 144, 227, 228syl3anc 1317 . . . . . . 7 (𝜑 → ((𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
230220, 229eqtrd 2643 . . . . . 6 (𝜑 → (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) = ((𝑅 Σg (𝑘 ∈ {0} ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))) + (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵)))))))
231197, 209, 2303eqtr4d 2653 . . . . 5 (𝜑 → (𝑅 Σg (𝑘 ∈ (1...(𝑁 + 1)) ↦ (((𝑁C(𝑘 − 1)) · (((𝑁 + 1) − 𝑘) 𝐴)) × (𝑘 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
232128, 231syl5eq 2655 . . . 4 (𝜑 → (𝑅 Σg (𝑗 ∈ ((0 + 1)...(𝑁 + 1)) ↦ (((𝑁C(𝑗 − 1)) · (((𝑁 + 1) − 𝑗) 𝐴)) × (𝑗 𝐵)))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
23352, 116, 2323eqtrd 2647 . . 3 (𝜑 → (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ (((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))) × 𝐵))) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
23434, 233eqtr3d 2645 . 2 (𝜑 → ((𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁𝑘) 𝐴) × (𝑘 𝐵))))) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
2352, 234sylan9eqr 2665 1 ((𝜑𝜓) → ((𝑁 (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) 𝐴) × (𝑘 𝐵))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  Vcvv 3172  {csn 4124   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  Fincfn 7818  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cmin 10117  cn 10867  0cn0 11139  cz 11210  ...cfz 12152  Ccbc 12906  Basecbs 15641  +gcplusg 15714  .rcmulr 15715  0gc0g 15869   Σg cgsu 15870  Mndcmnd 17063  .gcmg 17309  CMndccmn 17962  mulGrpcmgp 18258  SRingcsrg 18274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-oi 8275  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-fz 12153  df-fzo 12290  df-seq 12619  df-fac 12878  df-bc 12907  df-hash 12935  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-0g 15871  df-gsum 15872  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-mhm 17104  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-mgp 18259  df-srg 18275
This theorem is referenced by:  srgbinomlem  18313
  Copyright terms: Public domain W3C validator