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

Theorem srgbinomlem4 16629
Description: Lemma 4 for srgbinomlem 16630. (Contributed by AV, 24-Aug-2019.)
Hypotheses
Ref Expression
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  gsumg  ( k  e.  ( 0 ... N )  |->  ( ( N  _C  k ) 
.x.  ( ( ( N  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
Assertion
Ref Expression
srgbinomlem4  |-  ( (
ph  /\  ps )  ->  ( ( N  .^  ( A  .+  B ) )  .X.  B )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) )  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
Distinct variable groups:    A, k    B, k    k, N    R, k    S, k    .x. , k    .X. , k    .^ , k    ph, k
Allowed substitution hints:    ps( k)    .+ ( k)    G( k)

Proof of Theorem srgbinomlem4
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 srgbinomlem.i . . 3  |-  ( ps 
->  ( N  .^  ( A  .+  B ) )  =  ( R  gsumg  ( k  e.  ( 0 ... N )  |->  ( ( N  _C  k ) 
.x.  ( ( ( N  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
21oveq1d 6101 . 2  |-  ( ps 
->  ( ( N  .^  ( A  .+  B ) )  .X.  B )  =  ( ( R 
gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  .X.  B
) )
3 srgbinom.s . . . 4  |-  S  =  ( Base `  R
)
4 eqid 2438 . . . 4  |-  ( 0g
`  R )  =  ( 0g `  R
)
5 srgbinom.a . . . 4  |-  .+  =  ( +g  `  R )
6 srgbinom.m . . . 4  |-  .X.  =  ( .r `  R )
7 srgbinomlem.r . . . 4  |-  ( ph  ->  R  e. SRing )
8 ovex 6111 . . . . 5  |-  ( 0 ... N )  e. 
_V
98a1i 11 . . . 4  |-  ( ph  ->  ( 0 ... N
)  e.  _V )
10 srgbinomlem.b . . . 4  |-  ( ph  ->  B  e.  S )
11 simpl 457 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ph )
12 srgbinomlem.n . . . . . 6  |-  ( ph  ->  N  e.  NN0 )
13 elfzelz 11445 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  ZZ )
14 bccl 12090 . . . . . 6  |-  ( ( N  e.  NN0  /\  k  e.  ZZ )  ->  ( N  _C  k
)  e.  NN0 )
1512, 13, 14syl2an 477 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  _C  k )  e. 
NN0 )
16 fznn0sub 11479 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  ( N  -  k )  e.  NN0 )
1716adantl 466 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  -  k )  e.  NN0 )
18 elfznn0 11473 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
1918adantl 466 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  k  e.  NN0 )
20 srgbinom.t . . . . . 6  |-  .x.  =  (.g
`  R )
21 srgbinom.g . . . . . 6  |-  G  =  (mulGrp `  R )
22 srgbinom.e . . . . . 6  |-  .^  =  (.g
`  G )
23 srgbinomlem.a . . . . . 6  |-  ( ph  ->  A  e.  S )
24 srgbinomlem.c . . . . . 6  |-  ( ph  ->  ( A  .X.  B
)  =  ( B 
.X.  A ) )
253, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 16627 . . . . 5  |-  ( (
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 )
2611, 15, 17, 19, 25syl13anc 1220 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
27 eqid 2438 . . . . 5  |-  ( 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 )
) ) )
28 fzfid 11787 . . . . 5  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
29 ovex 6111 . . . . . 6  |-  ( ( N  _C  k ) 
.x.  ( ( ( N  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) )  e. 
_V
3029a1i 11 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e. 
_V )
31 fvex 5696 . . . . . 6  |-  ( 0g
`  R )  e. 
_V
3231a1i 11 . . . . 5  |-  ( ph  ->  ( 0g `  R
)  e.  _V )
3327, 28, 30, 32fsuppmptdm 7623 . . . 4  |-  ( ph  ->  ( k  e.  ( 0 ... N ) 
|->  ( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) finSupp  ( 0g `  R ) )
343, 4, 5, 6, 7, 9, 10, 26, 33srgsummulcr 16624 . . 3  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( ( N  _C  k )  .x.  ( ( ( N  -  k )  .^  A )  .X.  (
k  .^  B )
) )  .X.  B
) ) )  =  ( ( R  gsumg  ( k  e.  ( 0 ... N )  |->  ( ( N  _C  k ) 
.x.  ( ( ( N  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  .X.  B )
)
35 srgcmn 16598 . . . . . 6  |-  ( R  e. SRing  ->  R  e. CMnd )
367, 35syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
37 1z 10668 . . . . . 6  |-  1  e.  ZZ
3837a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
39 0zd 10650 . . . . 5  |-  ( ph  ->  0  e.  ZZ )
4012nn0zd 10737 . . . . 5  |-  ( ph  ->  N  e.  ZZ )
417adantr 465 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  R  e. SRing )
4210adantr 465 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  S )
433, 6srgcl 16602 . . . . . 6  |-  ( ( R  e. SRing  /\  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S  /\  B  e.  S )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  e.  S )
4441, 26, 42, 43syl3anc 1218 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  e.  S )
45 oveq2 6094 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  ( N  _C  k )  =  ( N  _C  (
j  -  1 ) ) )
46 oveq2 6094 . . . . . . . . 9  |-  ( k  =  ( j  - 
1 )  ->  ( N  -  k )  =  ( N  -  ( j  -  1 ) ) )
4746oveq1d 6101 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
( N  -  k
)  .^  A )  =  ( ( N  -  ( j  - 
1 ) )  .^  A ) )
48 oveq1 6093 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
k  .^  B )  =  ( ( j  -  1 )  .^  B ) )
4947, 48oveq12d 6104 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )
5045, 49oveq12d 6104 . . . . . 6  |-  ( k  =  ( j  - 
1 )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  =  ( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  -  ( j  -  1 ) )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) ) )
5150oveq1d 6101 . . . . 5  |-  ( k  =  ( j  - 
1 )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  =  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )  .X.  B
) )
523, 4, 36, 38, 39, 40, 44, 51gsummptshft 16419 . . . 4  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( ( N  _C  k )  .x.  ( ( ( N  -  k )  .^  A )  .X.  (
k  .^  B )
) )  .X.  B
) ) )  =  ( R  gsumg  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )  .X.  B
) ) ) )
5312nn0cnd 10630 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
5453adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  N  e.  CC )
55 elfzelz 11445 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  ZZ )
5655adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  ZZ )
5756zcnd 10740 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  CC )
58 1cnd 9394 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  1  e.  CC )
5954, 57, 58subsub3d 9741 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  -  ( j  -  1 ) )  =  ( ( N  +  1 )  -  j ) )
6059oveq1d 6101 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  -  (
j  -  1 ) )  .^  A )  =  ( ( ( N  +  1 )  -  j )  .^  A ) )
6160oveq1d 6101 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  -  ( j  -  1 ) )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) )  =  ( ( ( ( N  +  1 )  -  j ) 
.^  A )  .X.  ( ( j  - 
1 )  .^  B
) ) )
6261oveq2d 6102 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  -  (
j  -  1 ) )  .^  A )  .X.  ( ( j  - 
1 )  .^  B
) ) )  =  ( ( N  _C  ( j  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  j )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) ) )
6362oveq1d 6101 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  -  ( j  -  1 ) )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) )  .X.  B )  =  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  j ) 
.^  A )  .X.  ( ( j  - 
1 )  .^  B
) ) )  .X.  B ) )
647adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  R  e. SRing )
65 peano2zm 10680 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
6655, 65syl 16 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  ZZ )
67 bccl 12090 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( j  -  1 )  e.  ZZ )  ->  ( N  _C  ( j  -  1 ) )  e.  NN0 )
6812, 66, 67syl2an 477 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  _C  ( j  - 
1 ) )  e. 
NN0 )
6921srgmgp 16600 . . . . . . . . . . . . 13  |-  ( R  e. SRing  ->  G  e.  Mnd )
707, 69syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  G  e.  Mnd )
7170adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  G  e.  Mnd )
72 0p1e1 10425 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  =  1
7372oveq1i 6096 . . . . . . . . . . . . . 14  |-  ( ( 0  +  1 ) ... ( N  + 
1 ) )  =  ( 1 ... ( N  +  1 ) )
7473eleq2i 2502 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  <->  j  e.  ( 1 ... ( N  +  1 ) ) )
75 fznn0sub 11479 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  j )  e.  NN0 )
7675a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  ( ( N  +  1 )  -  j )  e.  NN0 ) )
7774, 76syl5bi 217 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  ( ( N  +  1 )  -  j )  e.  NN0 ) )
7877imp 429 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  j )  e.  NN0 )
7923adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  A  e.  S )
8021, 3mgpbas 16585 . . . . . . . . . . . 12  |-  S  =  ( Base `  G
)
8180, 22mulgnn0cl 15634 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  j
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S )
8271, 78, 79, 81syl3anc 1218 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  e.  S )
83 elfznn 11470 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  j  e.  NN )
84 nnm1nn0 10613 . . . . . . . . . . . . . 14  |-  ( j  e.  NN  ->  (
j  -  1 )  e.  NN0 )
8583, 84syl 16 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  NN0 )
8674, 85sylbi 195 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  NN0 )
8786adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
j  -  1 )  e.  NN0 )
8810adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  B  e.  S )
8980, 22mulgnn0cl 15634 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( j  - 
1 )  .^  B
)  e.  S )
9071, 87, 88, 89syl3anc 1218 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  .^  B )  e.  S )
913, 20, 6srgmulgass 16618 . . . . . . . . . 10  |-  ( ( R  e. SRing  /\  (
( N  _C  (
j  -  1 ) )  e.  NN0  /\  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S  /\  ( ( j  - 
1 )  .^  B
)  e.  S ) )  ->  ( (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) ) 
.X.  ( ( j  -  1 )  .^  B ) )  =  ( ( N  _C  ( j  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  j )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) ) )
9264, 68, 82, 90, 91syl13anc 1220 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( (
j  -  1 ) 
.^  B ) )  =  ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( ( N  +  1 )  -  j )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) ) )
9392eqcomd 2443 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  j
)  .^  A )  .X.  ( ( j  - 
1 )  .^  B
) ) )  =  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
( j  -  1 )  .^  B )
) )
9493oveq1d 6101 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  j )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) )  .X.  B )  =  ( ( ( ( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) ) 
.X.  ( ( j  -  1 )  .^  B ) )  .X.  B ) )
95 srgmnd 16599 . . . . . . . . . . . 12  |-  ( R  e. SRing  ->  R  e.  Mnd )
967, 95syl 16 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Mnd )
9796adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  R  e.  Mnd )
983, 20mulgnn0cl 15634 . . . . . . . . . 10  |-  ( ( R  e.  Mnd  /\  ( N  _C  (
j  -  1 ) )  e.  NN0  /\  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S )  ->  ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  e.  S
)
9997, 68, 82, 98syl3anc 1218 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  e.  S )
1003, 6srgass 16603 . . . . . . . . 9  |-  ( ( R  e. SRing  /\  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  e.  S  /\  ( ( j  - 
1 )  .^  B
)  e.  S  /\  B  e.  S )
)  ->  ( (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( (
j  -  1 ) 
.^  B ) ) 
.X.  B )  =  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
( ( j  - 
1 )  .^  B
)  .X.  B )
) )
10164, 99, 90, 88, 100syl13anc 1220 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
( j  -  1 )  .^  B )
)  .X.  B )  =  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( ( ( j  -  1 )  .^  B )  .X.  B
) ) )
10221, 6mgpplusg 16583 . . . . . . . . . . . 12  |-  .X.  =  ( +g  `  G )
10380, 22, 102mulgnn0p1 15629 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  +  1 )  .^  B
)  =  ( ( ( j  -  1 )  .^  B )  .X.  B ) )
104103eqcomd 2443 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  .^  B )  .X.  B
)  =  ( ( ( j  -  1 )  +  1 ) 
.^  B ) )
10571, 87, 88, 104syl3anc 1218 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  .^  B
)  .X.  B )  =  ( ( ( j  -  1 )  +  1 )  .^  B ) )
106105oveq2d 6102 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( (
( j  -  1 )  .^  B )  .X.  B ) )  =  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
( ( j  - 
1 )  +  1 )  .^  B )
) )
10755zcnd 10740 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  CC )
108 1cnd 9394 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  1  e.  CC )
109107, 108npcand 9715 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
( j  -  1 )  +  1 )  =  j )
110109adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  +  1 )  =  j )
111110oveq1d 6101 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  +  1 )  .^  B )  =  ( j  .^  B ) )
112111oveq2d 6102 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( (
( j  -  1 )  +  1 ) 
.^  B ) )  =  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( j  .^  B
) ) )
113101, 106, 1123eqtrd 2474 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
( j  -  1 )  .^  B )
)  .X.  B )  =  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( j  .^  B
) ) )
11463, 94, 1133eqtrd 2474 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  -  ( j  -  1 ) )  .^  A
)  .X.  ( (
j  -  1 ) 
.^  B ) ) )  .X.  B )  =  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( j  .^  B
) ) )
115114mpteq2dva 4373 . . . . 5  |-  ( ph  ->  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )  .X.  B
) )  =  ( j  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) )  |->  ( ( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( j  .^  B ) ) ) )
116115oveq2d 6102 . . . 4  |-  ( ph  ->  ( R  gsumg  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )  .X.  B
) ) )  =  ( R  gsumg  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
j  .^  B )
) ) ) )
117 mpteq1 4367 . . . . . . . 8  |-  ( ( ( 0  +  1 ) ... ( N  +  1 ) )  =  ( 1 ... ( N  +  1 ) )  ->  (
j  e.  ( ( 0  +  1 ) ... ( N  + 
1 ) )  |->  ( ( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( j  .^  B ) ) )  =  ( j  e.  ( 1 ... ( N  +  1 ) )  |->  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( j  .^  B
) ) ) )
11873, 117ax-mp 5 . . . . . . 7  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  |->  ( ( ( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) ) 
.X.  ( j  .^  B ) ) )  =  ( j  e.  ( 1 ... ( N  +  1 ) )  |->  ( ( ( N  _C  ( j  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  j )  .^  A ) )  .X.  ( j  .^  B
) ) )
119 oveq1 6093 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
j  -  1 )  =  ( k  - 
1 ) )
120119oveq2d 6102 . . . . . . . . . 10  |-  ( j  =  k  ->  ( N  _C  ( j  - 
1 ) )  =  ( N  _C  (
k  -  1 ) ) )
121 oveq2 6094 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( N  +  1 )  -  j )  =  ( ( N  +  1 )  -  k ) )
122121oveq1d 6101 . . . . . . . . . 10  |-  ( j  =  k  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  =  ( ( ( N  +  1 )  -  k )  .^  A ) )
123120, 122oveq12d 6104 . . . . . . . . 9  |-  ( j  =  k  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  =  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) ) )
124 oveq1 6093 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  .^  B )  =  ( k  .^  B ) )
125123, 124oveq12d 6104 . . . . . . . 8  |-  ( j  =  k  ->  (
( ( N  _C  ( j  -  1 ) )  .x.  (
( ( N  + 
1 )  -  j
)  .^  A )
)  .X.  ( j  .^  B ) )  =  ( ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) )  .X.  (
k  .^  B )
) )
126125cbvmptv 4378 . . . . . . 7  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  |->  ( ( ( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) ) 
.X.  ( j  .^  B ) ) )  =  ( k  e.  ( 1 ... ( N  +  1 ) )  |->  ( ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  k )  .^  A ) )  .X.  ( k  .^  B
) ) )
127118, 126eqtri 2458 . . . . . 6  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  |->  ( ( ( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) ) 
.X.  ( j  .^  B ) ) )  =  ( k  e.  ( 1 ... ( N  +  1 ) )  |->  ( ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( N  +  1 )  -  k )  .^  A ) )  .X.  ( k  .^  B
) ) )
128127oveq2i 6097 . . . . 5  |-  ( R 
gsumg  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
j  .^  B )
) ) )  =  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) )  .X.  (
k  .^  B )
) ) )
129 fzfid 11787 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  e.  Fin )
130 simpl 457 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ph )
131 elfzelz 11445 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  ZZ )
132 peano2zm 10680 . . . . . . . . . . . . 13  |-  ( k  e.  ZZ  ->  (
k  -  1 )  e.  ZZ )
133131, 132syl 16 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
134 bccl 12090 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( k  -  1 )  e.  ZZ )  ->  ( N  _C  ( k  -  1 ) )  e.  NN0 )
13512, 133, 134syl2an 477 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( N  _C  ( k  - 
1 ) )  e. 
NN0 )
136 fznn0sub 11479 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
137136adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
138 elfznn 11470 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN )
139138nnnn0d 10628 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN0 )
140139adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  k  e.  NN0 )
1413, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 16627 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( N  _C  ( k  - 
1 ) )  e. 
NN0  /\  ( ( N  +  1 )  -  k )  e. 
NN0  /\  k  e.  NN0 ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
142130, 135, 137, 140, 141syl13anc 1220 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
143142ralrimiva 2794 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  ( 1 ... ( N  +  1 ) ) ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) )  e.  S )
1443, 36, 129, 143gsummptcl 16446 . . . . . . . 8  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  e.  S
)
1453, 5, 4mndlid 15433 . . . . . . . 8  |-  ( ( R  e.  Mnd  /\  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  e.  S
)  ->  ( ( 0g `  R )  .+  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )  =  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
14696, 144, 145syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( 0g `  R )  .+  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )  =  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
147 0nn0 10586 . . . . . . . . . . 11  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  NN0 )
149 id 22 . . . . . . . . . . 11  |-  ( ph  ->  ph )
150 0z 10649 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
151150, 37pm3.2i 455 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  /\  1  e.  ZZ )
152 zsubcl 10679 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  1  e.  ZZ )  ->  ( 0  -  1 )  e.  ZZ )
153151, 152mp1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  e.  ZZ )
154 bccl 12090 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ )  ->  ( N  _C  ( 0  -  1 ) )  e.  NN0 )
15512, 153, 154syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  e.  NN0 )
156 nn0cn 10581 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  N  e.  CC )
157 peano2cn 9533 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  ( N  +  1 )  e.  CC )
158156, 157syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  CC )
159158subid1d 9700 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  =  ( N  +  1 ) )
160 peano2nn0 10612 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
161159, 160eqeltrd 2512 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  e. 
NN0 )
16212, 161syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  + 
1 )  -  0 )  e.  NN0 )
1633, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 16627 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( N  _C  ( 0  -  1 ) )  e. 
NN0  /\  ( ( N  +  1 )  -  0 )  e. 
NN0  /\  0  e.  NN0 ) )  ->  (
( N  _C  (
0  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  e.  S )
164149, 155, 162, 148, 163syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  e.  S )
165 oveq1 6093 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  -  1 )  =  ( 0  -  1 ) )
166165oveq2d 6102 . . . . . . . . . . . 12  |-  ( k  =  0  ->  ( N  _C  ( k  - 
1 ) )  =  ( N  _C  (
0  -  1 ) ) )
167 oveq2 6094 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( N  +  1 )  -  k )  =  ( ( N  +  1 )  - 
0 ) )
168167oveq1d 6101 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  =  ( ( ( N  +  1 )  -  0 )  .^  A ) )
169 oveq1 6093 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  .^  B )  =  ( 0  .^  B ) )
170168, 169oveq12d 6104 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
) )
171166, 170oveq12d 6104 . . . . . . . . . . 11  |-  ( k  =  0  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  =  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) ) )
1723, 171gsumsn 16439 . . . . . . . . . 10  |-  ( ( R  e.  Mnd  /\  0  e.  NN0  /\  (
( N  _C  (
0  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  e.  S )  ->  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  =  ( ( N  _C  ( 0  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  0 ) 
.^  A )  .X.  ( 0  .^  B
) ) ) )
17396, 148, 164, 172syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  =  ( ( N  _C  ( 0  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  0 ) 
.^  A )  .X.  ( 0  .^  B
) ) ) )
174 0lt1 9854 . . . . . . . . . . . . . . 15  |-  0  <  1
175174a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  1 )
176175, 72syl6breqr 4327 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 0  +  1 ) )
177 0re 9378 . . . . . . . . . . . . . . 15  |-  0  e.  RR
178 1re 9377 . . . . . . . . . . . . . . 15  |-  1  e.  RR
179177, 178, 1773pm3.2i 1166 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )
180 ltsubadd 9801 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )  ->  (
( 0  -  1 )  <  0  <->  0  <  ( 0  +  1 ) ) )
181179, 180mp1i 12 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 0  -  1 )  <  0  <->  0  <  ( 0  +  1 ) ) )
182176, 181mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  <  0 )
183182orcd 392 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )
184 bcval4 12075 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ  /\  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )  ->  ( N  _C  ( 0  -  1 ) )  =  0 )
18512, 153, 183, 184syl3anc 1218 . . . . . . . . . 10  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  =  0 )
186185oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  =  ( 0 
.x.  ( ( ( ( N  +  1 )  -  0 ) 
.^  A )  .X.  ( 0  .^  B
) ) ) )
18780, 22mulgnn0cl 15634 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  0 )  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18870, 162, 23, 187syl3anc 1218 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18980, 22mulgnn0cl 15634 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  0  e.  NN0  /\  B  e.  S )  ->  (
0  .^  B )  e.  S )
19070, 148, 10, 189syl3anc 1218 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  .^  B
)  e.  S )
1913, 6srgcl 16602 . . . . . . . . . . 11  |-  ( ( R  e. SRing  /\  (
( ( N  + 
1 )  -  0 )  .^  A )  e.  S  /\  (
0  .^  B )  e.  S )  ->  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) )  e.  S )
1927, 188, 190, 191syl3anc 1218 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
)  e.  S )
1933, 4, 20mulg0 15623 . . . . . . . . . 10  |-  ( ( ( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) )  e.  S  ->  (
0  .x.  ( (
( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  =  ( 0g `  R
) )
194192, 193syl 16 . . . . . . . . 9  |-  ( ph  ->  ( 0  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  =  ( 0g
`  R ) )
195173, 186, 1943eqtrrd 2475 . . . . . . . 8  |-  ( ph  ->  ( 0g `  R
)  =  ( R 
gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
196195oveq1d 6101 . . . . . . 7  |-  ( ph  ->  ( ( 0g `  R )  .+  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )  =  ( ( R  gsumg  ( k  e.  { 0 } 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  .+  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) ) )
197146, 196eqtr3d 2472 . . . . . 6  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  =  ( ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  .+  ( R 
gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) ) )
1987adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  R  e. SRing )
19970adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  G  e.  Mnd )
20023adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  A  e.  S )
20180, 22mulgnn0cl 15634 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  k
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  k )  .^  A
)  e.  S )
202199, 137, 200, 201syl3anc 1218 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  e.  S )
20310adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  B  e.  S )
20480, 22mulgnn0cl 15634 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  k  e.  NN0  /\  B  e.  S )  ->  (
k  .^  B )  e.  S )
205199, 140, 203, 204syl3anc 1218 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
k  .^  B )  e.  S )
2063, 20, 6srgmulgass 16618 . . . . . . . . 9  |-  ( ( R  e. SRing  /\  (
( N  _C  (
k  -  1 ) )  e.  NN0  /\  ( ( ( N  +  1 )  -  k )  .^  A
)  e.  S  /\  ( k  .^  B
)  e.  S ) )  ->  ( (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( N  +  1 )  -  k ) 
.^  A ) ) 
.X.  ( k  .^  B ) )  =  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) )
207198, 135, 202, 205, 206syl13anc 1220 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( ( N  _C  ( k  -  1 ) )  .x.  (
( ( N  + 
1 )  -  k
)  .^  A )
)  .X.  ( k  .^  B ) )  =  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) )
208207mpteq2dva 4373 . . . . . . 7  |-  ( ph  ->  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) )  .X.  (
k  .^  B )
) )  =  ( k  e.  ( 1 ... ( N  + 
1 ) )  |->  ( ( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) ) ) )
209208oveq2d 6102 . . . . . 6  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) )  .X.  (
k  .^  B )
) ) )  =  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
210 fzfid 11787 . . . . . . 7  |-  ( ph  ->  ( 0 ... ( N  +  1 ) )  e.  Fin )
211 simpl 457 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ph )
212 elfzelz 11445 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  ZZ )
213212, 132syl 16 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
21412, 213, 134syl2an 477 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ( N  _C  ( k  - 
1 ) )  e. 
NN0 )
215 fznn0sub 11479 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
216215adantl 466 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
217 elfznn0 11473 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  NN0 )
218217adantl 466 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  k  e.  NN0 )
219211, 214, 216, 218, 141syl13anc 1220 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
220 1e0p1 10775 . . . . . . . . . . 11  |-  1  =  ( 0  +  1 )
221220a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  =  ( 0  +  1 ) )
222221oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 0  +  1 ) ... ( N  + 
1 ) ) )
223222ineq2d 3547 . . . . . . . 8  |-  ( ph  ->  ( { 0 }  i^i  ( 1 ... ( N  +  1 ) ) )  =  ( { 0 }  i^i  ( ( 0  +  1 ) ... ( N  +  1 ) ) ) )
224 elnn0uz 10890 . . . . . . . . . . 11  |-  ( N  e.  NN0  <->  N  e.  ( ZZ>=
`  0 ) )
225 peano2uz 10900 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( N  +  1 )  e.  ( ZZ>= `  0 )
)
226224, 225sylbi 195 . . . . . . . . . 10  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  ( ZZ>= `  0 )
)
22712, 226syl 16 . . . . . . . . 9  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
228 fzpreddisj 11496 . . . . . . . . 9  |-  ( ( N  +  1 )  e.  ( ZZ>= `  0
)  ->  ( {
0 }  i^i  (
( 0  +  1 ) ... ( N  +  1 ) ) )  =  (/) )
229227, 228syl 16 . . . . . . . 8  |-  ( ph  ->  ( { 0 }  i^i  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  =  (/) )
230223, 229eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( { 0 }  i^i  ( 1 ... ( N  +  1 ) ) )  =  (/) )
231 fzpred 11495 . . . . . . . . 9  |-  ( ( N  +  1 )  e.  ( ZZ>= `  0
)  ->  ( 0 ... ( N  + 
1 ) )  =  ( { 0 }  u.  ( ( 0  +  1 ) ... ( N  +  1 ) ) ) )
232227, 231syl 16 . . . . . . . 8  |-  ( ph  ->  ( 0 ... ( N  +  1 ) )  =  ( { 0 }  u.  (
( 0  +  1 ) ... ( N  +  1 ) ) ) )
23372a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( 0  +  1 )  =  1 )
234233oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( 0  +  1 ) ... ( N  +  1 ) )  =  ( 1 ... ( N  + 
1 ) ) )
235234uneq2d 3505 . . . . . . . 8  |-  ( ph  ->  ( { 0 }  u.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  =  ( { 0 }  u.  ( 1 ... ( N  +  1 ) ) ) )
236232, 235eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( 0 ... ( N  +  1 ) )  =  ( { 0 }  u.  (
1 ... ( N  + 
1 ) ) ) )
2373, 5, 36, 210, 219, 230, 236gsummptfidmsplit 16415 . . . . . 6  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  =  ( ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  .+  ( R 
gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) ) )
238197, 209, 2373eqtr4d 2480 . . . . 5  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) )  .X.  (
k  .^  B )
) ) )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
239128, 238syl5eq 2482 . . . 4  |-  ( ph  ->  ( R  gsumg  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) 
|->  ( ( ( N  _C  ( j  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  j )  .^  A
) )  .X.  (
j  .^  B )
) ) )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
24052, 116, 2393eqtrd 2474 . . 3  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( ( N  _C  k )  .x.  ( ( ( N  -  k )  .^  A )  .X.  (
k  .^  B )
) )  .X.  B
) ) )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) ) )
24134, 240eqtr3d 2472 . 2  |-  ( ph  ->  ( ( R  gsumg  ( k  e.  ( 0 ... N )  |->  ( ( N  _C  k ) 
.x.  ( ( ( N  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  .X.  B )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) )  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
2422, 241sylan9eqr 2492 1  |-  ( (
ph  /\  ps )  ->  ( ( N  .^  ( A  .+  B ) )  .X.  B )  =  ( R  gsumg  ( k  e.  ( 0 ... ( N  +  1 ) )  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   _Vcvv 2967    u. cun 3321    i^i cin 3322   (/)c0 3632   {csn 3872   class class class wbr 4287    e. cmpt 4345   ` cfv 5413  (class class class)co 6086   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    < clt 9410    - cmin 9587   NNcn 10314   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   ...cfz 11429    _C cbc 12070   Basecbs 14166   +g cplusg 14230   .rcmulr 14231   0gc0g 14370    gsumg cgsu 14371   Mndcmnd 15401  .gcmg 15406  CMndccmn 16268  mulGrpcmgp 16579  SRingcsrg 16595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-n0 10572  df-z 10639  df-uz 10854  df-rp 10984  df-fz 11430  df-fzo 11541  df-seq 11799  df-fac 12044  df-bc 12071  df-hash 12096  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-0g 14372  df-gsum 14373  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-mulg 15539  df-cntz 15826  df-cmn 16270  df-mgp 16580  df-srg 16596
This theorem is referenced by:  srgbinomlem  16630
  Copyright terms: Public domain W3C validator