Metamath Proof Explorer

Theorem srgbinomlem

Description: Lemma for srgbinom . Inductive step, analogous to binomlem . (Contributed by AV, 24-Aug-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 srgbinomlem ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 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 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
14 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
15 13 14 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
16 5 srgmgp ⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
17 7 16 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
18 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
19 7 18 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
20 1 4 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 + 𝐵 ) ∈ 𝑆 )
21 19 8 9 20 syl3anc ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ 𝑆 )
22 17 11 21 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) )
24 5 1 mgpbas ⊢ 𝑆 = ( Base ‘ 𝐺 )
25 5 2 mgpplusg ⊢ × = ( +g ‘ 𝐺 )
26 24 6 25 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) )
27 23 26 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) )
28 24 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 )
29 17 11 21 28 syl3anc ⊢ ( 𝜑 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 )
30 29 8 9 3jca ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
31 7 30 jca ⊢ ( 𝜑 → ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) )
33 1 4 2 srgdi ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
35 27 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
36 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
37 bcpasc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
38 11 36 37 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
39 38 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
40 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ Mnd )
41 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
42 11 36 41 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
43 36 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
44 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
46 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
47 11 45 46 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
48 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ SRing )
49 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
50 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
52 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
53 24 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
54 49 51 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
55 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
57 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
58 24 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
59 49 56 57 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
60 1 2 srgcl ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 )
61 48 54 59 60 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 )
62 1 3 4 mulgnn0dir ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
63 40 42 47 61 62 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
64 39 63 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
65 64 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
66 65 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
67 srgcmn ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
68 7 67 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
69 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
70 1 3 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
71 40 42 61 70 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
72 36 44 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
73 11 72 46 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
74 1 3 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
75 40 73 61 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
76 eqid ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
77 eqid ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
78 1 4 68 69 71 75 76 77 gsummptfidmadd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
79 66 78 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
81 15 35 80 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )