Metamath Proof Explorer

Theorem srgbinomlem3

Description: Lemma 3 for srgbinomlem . (Contributed by AV, 23-Aug-2019) (Proof shortened by AV, 27-Oct-2019)

Ref Expression
Hypotheses srgbinom.s 
|- S = ( Base ` R )
srgbinom.m 
|- .X. = ( .r ` R )
srgbinom.t 
|- .x. = ( .g ` R )
srgbinom.a 
|- .+ = ( +g ` R )
srgbinom.g 
|- G = ( mulGrp ` R )
srgbinom.e 
|- .^ = ( .g ` G )
srgbinomlem.r 
|- ( ph -> R e. SRing )
srgbinomlem.a 
|- ( ph -> A e. S )
srgbinomlem.b 
|- ( ph -> B e. S )
srgbinomlem.c 
|- ( ph -> ( A .X. B ) = ( B .X. A ) )
srgbinomlem.n 
|- ( ph -> N e. NN0 )
srgbinomlem.i 
|- ( ps -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
Assertion srgbinomlem3 
|- ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. A ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 srgbinom.s 
 |-  S = ( Base ` R )
2 srgbinom.m 
 |-  .X. = ( .r ` R )
3 srgbinom.t 
 |-  .x. = ( .g ` R )
4 srgbinom.a 
 |-  .+ = ( +g ` R )
5 srgbinom.g 
 |-  G = ( mulGrp ` R )
6 srgbinom.e 
 |-  .^ = ( .g ` G )
7 srgbinomlem.r 
 |-  ( ph -> R e. SRing )
8 srgbinomlem.a 
 |-  ( ph -> A e. S )
9 srgbinomlem.b 
 |-  ( ph -> B e. S )
10 srgbinomlem.c 
 |-  ( ph -> ( A .X. B ) = ( B .X. A ) )
11 srgbinomlem.n 
 |-  ( ph -> N e. NN0 )
12 srgbinomlem.i 
 |-  ( ps -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
13 12 adantl 
 |-  ( ( ph /\ ps ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
14 13 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. A ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. A ) )
15 srgcmn 
 |-  ( R e. SRing -> R e. CMnd )
16 7 15 syl 
 |-  ( ph -> R e. CMnd )
17 simpl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ph )
18 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
19 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
20 11 18 19 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
21 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
22 21 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
23 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
24 23 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
25 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( ph /\ ( ( N _C k ) e. NN0 /\ ( ( N + 1 ) - k ) e. NN0 /\ k e. NN0 ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
26 17 20 22 24 25 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
27 1 4 16 11 26 gsummptfzsplit 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. { ( N + 1 ) } |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
28 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
29 7 28 syl 
 |-  ( ph -> R e. Mnd )
30 ovexd 
 |-  ( ph -> ( N + 1 ) e. _V )
31 id 
 |-  ( ph -> ph )
32 11 nn0zd 
 |-  ( ph -> N e. ZZ )
33 32 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
34 bccl 
 |-  ( ( N e. NN0 /\ ( N + 1 ) e. ZZ ) -> ( N _C ( N + 1 ) ) e. NN0 )
35 11 33 34 syl2anc 
 |-  ( ph -> ( N _C ( N + 1 ) ) e. NN0 )
36 11 nn0cnd 
 |-  ( ph -> N e. CC )
37 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
38 36 37 syl 
 |-  ( ph -> ( N + 1 ) e. CC )
39 38 subidd 
 |-  ( ph -> ( ( N + 1 ) - ( N + 1 ) ) = 0 )
40 0nn0 
 |-  0 e. NN0
41 39 40 eqeltrdi 
 |-  ( ph -> ( ( N + 1 ) - ( N + 1 ) ) e. NN0 )
42 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
43 11 42 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
44 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( ph /\ ( ( N _C ( N + 1 ) ) e. NN0 /\ ( ( N + 1 ) - ( N + 1 ) ) e. NN0 /\ ( N + 1 ) e. NN0 ) ) -> ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) e. S )
45 31 35 41 43 44 syl13anc 
 |-  ( ph -> ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) e. S )
46 oveq2 
 |-  ( k = ( N + 1 ) -> ( N _C k ) = ( N _C ( N + 1 ) ) )
47 oveq2 
 |-  ( k = ( N + 1 ) -> ( ( N + 1 ) - k ) = ( ( N + 1 ) - ( N + 1 ) ) )
48 47 oveq1d 
 |-  ( k = ( N + 1 ) -> ( ( ( N + 1 ) - k ) .^ A ) = ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) )
49 oveq1 
 |-  ( k = ( N + 1 ) -> ( k .^ B ) = ( ( N + 1 ) .^ B ) )
50 48 49 oveq12d 
 |-  ( k = ( N + 1 ) -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) )
51 46 50 oveq12d 
 |-  ( k = ( N + 1 ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) )
52 1 51 gsumsn 
 |-  ( ( R e. Mnd /\ ( N + 1 ) e. _V /\ ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) e. S ) -> ( R gsum ( k e. { ( N + 1 ) } |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) )
53 29 30 45 52 syl3anc 
 |-  ( ph -> ( R gsum ( k e. { ( N + 1 ) } |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) )
54 11 nn0red 
 |-  ( ph -> N e. RR )
55 54 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
56 55 olcd 
 |-  ( ph -> ( ( N + 1 ) < 0 \/ N < ( N + 1 ) ) )
57 bcval4 
 |-  ( ( N e. NN0 /\ ( N + 1 ) e. ZZ /\ ( ( N + 1 ) < 0 \/ N < ( N + 1 ) ) ) -> ( N _C ( N + 1 ) ) = 0 )
58 11 33 56 57 syl3anc 
 |-  ( ph -> ( N _C ( N + 1 ) ) = 0 )
59 58 oveq1d 
 |-  ( ph -> ( ( N _C ( N + 1 ) ) .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) = ( 0 .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) )
60 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem1 
 |-  ( ( ph /\ ( ( ( N + 1 ) - ( N + 1 ) ) e. NN0 /\ ( N + 1 ) e. NN0 ) ) -> ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) e. S )
61 31 41 43 60 syl12anc 
 |-  ( ph -> ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) e. S )
62 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
63 1 62 3 mulg0 
 |-  ( ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) e. S -> ( 0 .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) = ( 0g ` R ) )
64 61 63 syl 
 |-  ( ph -> ( 0 .x. ( ( ( ( N + 1 ) - ( N + 1 ) ) .^ A ) .X. ( ( N + 1 ) .^ B ) ) ) = ( 0g ` R ) )
65 53 59 64 3eqtrd 
 |-  ( ph -> ( R gsum ( k e. { ( N + 1 ) } |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( 0g ` R ) )
66 65 oveq2d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. { ( N + 1 ) } |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( 0g ` R ) ) )
67 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
68 simpl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ph )
69 bccl2 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) e. NN )
70 69 nnnn0d 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) e. NN0 )
71 70 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
72 fzelp1 
 |-  ( k e. ( 0 ... N ) -> k e. ( 0 ... ( N + 1 ) ) )
73 72 22 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N + 1 ) - k ) e. NN0 )
74 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
75 74 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
76 68 71 73 75 25 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
77 76 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... N ) ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
78 1 16 67 77 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S )
79 1 4 62 mndrid 
 |-  ( ( R e. Mnd /\ ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S ) -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( 0g ` R ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
80 29 78 79 syl2anc 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( 0g ` R ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
81 27 66 80 3eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
82 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> R e. SRing )
83 8 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. S )
84 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. S )
85 10 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A .X. B ) = ( B .X. A ) )
86 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
87 86 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
88 1 2 5 6 82 83 84 75 85 87 3 71 srgpcomppsc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. A ) = ( ( N _C k ) .x. ( ( ( ( N - k ) + 1 ) .^ A ) .X. ( k .^ B ) ) ) )
89 36 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> N e. CC )
90 1cnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> 1 e. CC )
91 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
92 91 zcnd 
 |-  ( k e. ( 0 ... N ) -> k e. CC )
93 92 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
94 89 90 93 addsubd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N + 1 ) - k ) = ( ( N - k ) + 1 ) )
95 94 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N + 1 ) - k ) .^ A ) = ( ( ( N - k ) + 1 ) .^ A ) )
96 95 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( ( N - k ) + 1 ) .^ A ) .X. ( k .^ B ) ) )
97 96 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) = ( ( N _C k ) .x. ( ( ( ( N - k ) + 1 ) .^ A ) .X. ( k .^ B ) ) ) )
98 88 97 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. A ) = ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) )
99 98 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. A ) ) = ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) )
100 99 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. A ) ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
101 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
102 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( ph /\ ( ( N _C k ) e. NN0 /\ ( N - k ) e. NN0 /\ k e. NN0 ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
103 68 71 87 75 102 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
104 eqid 
 |-  ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) )
105 ovexd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. _V )
106 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
107 104 67 105 106 fsuppmptdm 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) finSupp ( 0g ` R ) )
108 1 62 4 2 7 101 8 103 107 srgsummulcr 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. A ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. A ) )
109 81 100 108 3eqtr2rd 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. A ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
110 109 adantr 
 |-  ( ( ph /\ ps ) -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. A ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
111 14 110 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. A ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C k ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )