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 17 11 21 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 )
29 28 8 9 3jca ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
30 7 29 jca ⊢ ( 𝜑 → ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) )
32 1 4 2 srgdi ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
33 31 32 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
34 27 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐴 ) + ( ( 𝑁 ↑ ( 𝐴 + 𝐵 ) ) × 𝐵 ) ) )
35 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
36 bcpasc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
37 11 35 36 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
38 37 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
39 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ Mnd )
40 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
41 11 35 40 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
42 35 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
43 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
45 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
46 11 44 45 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
47 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑅 ∈ SRing )
48 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐺 ∈ Mnd )
49 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℕ0 )
51 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ 𝑆 )
52 24 6 48 50 51 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 )
53 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
55 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ 𝑆 )
56 24 6 48 54 55 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 )
57 1 2 srgcl ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝑘 ↑ 𝐵 ) ∈ 𝑆 ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 )
58 47 52 56 57 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 )
59 1 3 4 mulgnn0dir ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( 𝑁 C 𝑘 ) ∈ ℕ0 ∧ ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ∧ ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ∈ 𝑆 ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
60 39 41 46 58 59 syl13anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
61 38 60 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) )
62 61 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )
63 62 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
64 srgcmn ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
65 7 64 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
66 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
67 1 3 39 41 58 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
68 35 43 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
69 11 68 45 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
70 1 3 39 69 58 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ∈ 𝑆 )
71 eqid ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
72 eqid ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) )
73 1 4 65 66 67 70 71 72 gsummptfidmadd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) + ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
74 63 73 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) ) )
76 15 34 75 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 + 1 ) ↑ ( 𝐴 + 𝐵 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( ( ( 𝑁 + 1 ) − 𝑘 ) ↑ 𝐴 ) × ( 𝑘 ↑ 𝐵 ) ) ) ) ) )