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

Theorem srgbinomlem4 17066
Description: Lemma 4 for srgbinomlem 17067. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-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 6310 . 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 2467 . . . 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 6320 . . . . 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 11700 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  ZZ )
14 bccl 12380 . . . . . 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 11728 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  ( N  -  k )  e.  NN0 )
1716adantl 466 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  -  k )  e.  NN0 )
18 elfznn0 11782 . . . . . 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 17064 . . . . 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 1230 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
27 eqid 2467 . . . . 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 12063 . . . . 5  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
29 ovex 6320 . . . . . 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 5882 . . . . . 6  |-  ( 0g
`  R )  e. 
_V
3231a1i 11 . . . . 5  |-  ( ph  ->  ( 0g `  R
)  e.  _V )
3327, 28, 30, 32fsuppmptdm 7852 . . . 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 17060 . . 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 17032 . . . . . 6  |-  ( R  e. SRing  ->  R  e. CMnd )
367, 35syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
37 1z 10906 . . . . . 6  |-  1  e.  ZZ
3837a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
39 0zd 10888 . . . . 5  |-  ( ph  ->  0  e.  ZZ )
4012nn0zd 10976 . . . . 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 17036 . . . . . 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 1228 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  e.  S )
45 oveq2 6303 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  ( N  _C  k )  =  ( N  _C  (
j  -  1 ) ) )
46 oveq2 6303 . . . . . . . . 9  |-  ( k  =  ( j  - 
1 )  ->  ( N  -  k )  =  ( N  -  ( j  -  1 ) ) )
4746oveq1d 6310 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
( N  -  k
)  .^  A )  =  ( ( N  -  ( j  - 
1 ) )  .^  A ) )
48 oveq1 6302 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
k  .^  B )  =  ( ( j  -  1 )  .^  B ) )
4947, 48oveq12d 6313 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )
5045, 49oveq12d 6313 . . . . . 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 6310 . . . . 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 16829 . . . 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 10866 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
5453adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  N  e.  CC )
55 elfzelz 11700 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  ZZ )
5655adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  ZZ )
5756zcnd 10979 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  CC )
58 1cnd 9624 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  1  e.  CC )
5954, 57, 58subsub3d 9972 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  -  ( j  -  1 ) )  =  ( ( N  +  1 )  -  j ) )
6059oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  -  (
j  -  1 ) )  .^  A )  =  ( ( ( N  +  1 )  -  j )  .^  A ) )
6160oveq1d 6310 . . . . . . . . 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 6311 . . . . . . . 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 6310 . . . . . . 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 10918 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
6655, 65syl 16 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  ZZ )
67 bccl 12380 . . . . . . . . . . 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 17034 . . . . . . . . . . . . 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 10659 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  =  1
7372oveq1i 6305 . . . . . . . . . . . . . 14  |-  ( ( 0  +  1 ) ... ( N  + 
1 ) )  =  ( 1 ... ( N  +  1 ) )
7473eleq2i 2545 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  <->  j  e.  ( 1 ... ( N  +  1 ) ) )
75 fznn0sub 11728 . . . . . . . . . . . . . 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 17019 . . . . . . . . . . . 12  |-  S  =  ( Base `  G
)
8180, 22mulgnn0cl 16030 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  j
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S )
8271, 78, 79, 81syl3anc 1228 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  e.  S )
83 elfznn 11726 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  j  e.  NN )
84 nnm1nn0 10849 . . . . . . . . . . . . . 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 16030 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( j  - 
1 )  .^  B
)  e.  S )
9071, 87, 88, 89syl3anc 1228 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  .^  B )  e.  S )
913, 20, 6srgmulgass 17054 . . . . . . . . . 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 1230 . . . . . . . . 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 2475 . . . . . . . 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 6310 . . . . . . 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 17033 . . . . . . . . . . . 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 16030 . . . . . . . . . 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 1228 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  e.  S )
1003, 6srgass 17037 . . . . . . . . 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 1230 . . . . . . . 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 17017 . . . . . . . . . . . 12  |-  .X.  =  ( +g  `  G )
10380, 22, 102mulgnn0p1 16025 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  +  1 )  .^  B
)  =  ( ( ( j  -  1 )  .^  B )  .X.  B ) )
104103eqcomd 2475 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  .^  B )  .X.  B
)  =  ( ( ( j  -  1 )  +  1 ) 
.^  B ) )
10571, 87, 88, 104syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  .^  B
)  .X.  B )  =  ( ( ( j  -  1 )  +  1 )  .^  B ) )
106105oveq2d 6311 . . . . . . . 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 10979 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  CC )
108 1cnd 9624 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  1  e.  CC )
109107, 108npcand 9946 . . . . . . . . . . 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 6310 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  +  1 )  .^  B )  =  ( j  .^  B ) )
112111oveq2d 6311 . . . . . . . 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 2512 . . . . . . 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 2512 . . . . . 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 4539 . . . . 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 6311 . . . 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 4533 . . . . . . . 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 6302 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
j  -  1 )  =  ( k  - 
1 ) )
120119oveq2d 6311 . . . . . . . . . 10  |-  ( j  =  k  ->  ( N  _C  ( j  - 
1 ) )  =  ( N  _C  (
k  -  1 ) ) )
121 oveq2 6303 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( N  +  1 )  -  j )  =  ( ( N  +  1 )  -  k ) )
122121oveq1d 6310 . . . . . . . . . 10  |-  ( j  =  k  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  =  ( ( ( N  +  1 )  -  k )  .^  A ) )
123120, 122oveq12d 6313 . . . . . . . . 9  |-  ( j  =  k  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  =  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) ) )
124 oveq1 6302 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  .^  B )  =  ( k  .^  B ) )
125123, 124oveq12d 6313 . . . . . . . 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 4544 . . . . . . 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 2496 . . . . . 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 6306 . . . . 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 12063 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  e.  Fin )
130 simpl 457 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ph )
131 elfzelz 11700 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  ZZ )
132 peano2zm 10918 . . . . . . . . . . . . 13  |-  ( k  e.  ZZ  ->  (
k  -  1 )  e.  ZZ )
133131, 132syl 16 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
134 bccl 12380 . . . . . . . . . . . 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 11728 . . . . . . . . . . . 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 11726 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN )
139138nnnn0d 10864 . . . . . . . . . . . 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 17064 . . . . . . . . . . 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 1230 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
143142ralrimiva 2881 . . . . . . . . 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 16867 . . . . . . . 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 15814 . . . . . . . 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 10822 . . . . . . . . . . 11  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  NN0 )
149 id 22 . . . . . . . . . . 11  |-  ( ph  ->  ph )
150 0z 10887 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
151150, 37pm3.2i 455 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  /\  1  e.  ZZ )
152 zsubcl 10917 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  1  e.  ZZ )  ->  ( 0  -  1 )  e.  ZZ )
153151, 152mp1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  e.  ZZ )
154 bccl 12380 . . . . . . . . . . . 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 10817 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  N  e.  CC )
157 peano2cn 9763 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  ( N  +  1 )  e.  CC )
158156, 157syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  CC )
159158subid1d 9931 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  =  ( N  +  1 ) )
160 peano2nn0 10848 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
161159, 160eqeltrd 2555 . . . . . . . . . . . 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 17064 . . . . . . . . . . 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 1230 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  e.  S )
165 oveq1 6302 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  -  1 )  =  ( 0  -  1 ) )
166165oveq2d 6311 . . . . . . . . . . . 12  |-  ( k  =  0  ->  ( N  _C  ( k  - 
1 ) )  =  ( N  _C  (
0  -  1 ) ) )
167 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( N  +  1 )  -  k )  =  ( ( N  +  1 )  - 
0 ) )
168167oveq1d 6310 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  =  ( ( ( N  +  1 )  -  0 )  .^  A ) )
169 oveq1 6302 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  .^  B )  =  ( 0  .^  B ) )
170168, 169oveq12d 6313 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
) )
171166, 170oveq12d 6313 . . . . . . . . . . 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 16854 . . . . . . . . . 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 1228 . . . . . . . . 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 10087 . . . . . . . . . . . . . . 15  |-  0  <  1
175174a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  1 )
176175, 72syl6breqr 4493 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 0  +  1 ) )
177 0re 9608 . . . . . . . . . . . . . . 15  |-  0  e.  RR
178 1re 9607 . . . . . . . . . . . . . . 15  |-  1  e.  RR
179177, 178, 1773pm3.2i 1174 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )
180 ltsubadd 10034 . . . . . . . . . . . . . 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 12365 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ  /\  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )  ->  ( N  _C  ( 0  -  1 ) )  =  0 )
18512, 153, 183, 184syl3anc 1228 . . . . . . . . . 10  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  =  0 )
186185oveq1d 6310 . . . . . . . . 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 16030 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  0 )  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18870, 162, 23, 187syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18980, 22mulgnn0cl 16030 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  0  e.  NN0  /\  B  e.  S )  ->  (
0  .^  B )  e.  S )
19070, 148, 10, 189syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  .^  B
)  e.  S )
1913, 6srgcl 17036 . . . . . . . . . . 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 1228 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
)  e.  S )
1933, 4, 20mulg0 16019 . . . . . . . . . 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 2513 . . . . . . . 8  |-  ( ph  ->  ( 0g `  R
)  =  ( R 
gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
196195oveq1d 6310 . . . . . . 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 2510 . . . . . 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 16030 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  k
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  k )  .^  A
)  e.  S )
202199, 137, 200, 201syl3anc 1228 . . . . . . . . 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 16030 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  k  e.  NN0  /\  B  e.  S )  ->  (
k  .^  B )  e.  S )
205199, 140, 203, 204syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
k  .^  B )  e.  S )
2063, 20, 6srgmulgass 17054 . . . . . . . . 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 1230 . . . . . . . 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 4539 . . . . . . 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 6311 . . . . . 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 ) ) ) ) ) )
21012, 160syl 16 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
211 simpl 457 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ph )
212 elfzelz 11700 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  ZZ )
213212, 132syl 16 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
21412, 213, 134syl2an 477 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ( N  _C  ( k  - 
1 ) )  e. 
NN0 )
215 fznn0sub 11728 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
216215adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
217 elfznn0 11782 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  NN0 )
218217adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  k  e.  NN0 )
219211, 214, 216, 218, 141syl13anc 1230 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
2203, 5, 36, 210, 219gsummptfzsplitl 16826 . . . . . . 7  |-  ( ph  ->  ( R  gsumg  ( k  e.  ( 0 ... ( 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 ) ) ) ) )  .+  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) ) )
221 snfi 7608 . . . . . . . . . 10  |-  { 0 }  e.  Fin
222221a1i 11 . . . . . . . . 9  |-  ( ph  ->  { 0 }  e.  Fin )
223171eleq1d 2536 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) )  e.  S  <->  ( ( N  _C  ( 0  -  1 ) )  .x.  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
) )  e.  S
) )
224223ralsng 4068 . . . . . . . . . . 11  |-  ( 0  e.  NN0  ->  ( A. k  e.  { 0 }  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( ( N  +  1 )  -  k )  .^  A )  .X.  (
k  .^  B )
) )  e.  S  <->  ( ( N  _C  (
0  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  e.  S ) )
225147, 224ax-mp 5 . . . . . . . . . 10  |-  ( A. k  e.  { 0 }  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( ( N  +  1 )  -  k )  .^  A )  .X.  (
k  .^  B )
) )  e.  S  <->  ( ( N  _C  (
0  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  e.  S )
226164, 225sylibr 212 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  {
0 }  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) )  e.  S )
2273, 36, 222, 226gsummptcl 16867 . . . . . . . 8  |-  ( ph  ->  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  e.  S )
2283, 5cmncom 16687 . . . . . . . 8  |-  ( ( R  e. CMnd  /\  ( R  gsumg  ( k  e.  ( 1 ... ( N  +  1 ) ) 
|->  ( ( N  _C  ( k  -  1 ) )  .x.  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) ) )  e.  S  /\  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  e.  S )  ->  ( ( 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.  {
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 ) ) ) ) ) ) )
22936, 144, 227, 228syl3anc 1228 . . . . . . 7  |-  ( 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.  {
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 ) ) ) ) ) ) )
230220, 229eqtrd 2508 . . . . . 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 ) ) ) ) ) ) )
231197, 209, 2303eqtr4d 2518 . . . . 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 ) ) ) ) ) )
232128, 231syl5eq 2520 . . . 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 ) ) ) ) ) )
23352, 116, 2323eqtrd 2512 . . 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 ) ) ) ) ) )
23434, 233eqtr3d 2510 . 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
) ) ) ) ) )
2352, 234sylan9eqr 2530 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 973    = wceq 1379    e. wcel 1767   A.wral 2817   _Vcvv 3118   {csn 4033   class class class wbr 4453    |-> cmpt 4511   ` cfv 5594  (class class class)co 6295   Fincfn 7528   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505    + caddc 9507    < clt 9640    - cmin 9817   NNcn 10548   NN0cn0 10807   ZZcz 10876   ...cfz 11684    _C cbc 12360   Basecbs 14507   +g cplusg 14572   .rcmulr 14573   0gc0g 14712    gsumg cgsu 14713   Mndcmnd 15793  .gcmg 15928  CMndccmn 16671  mulGrpcmgp 17013  SRingcsrg 17029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-n0 10808  df-z 10877  df-uz 11095  df-rp 11233  df-fz 11685  df-fzo 11805  df-seq 12088  df-fac 12334  df-bc 12361  df-hash 12386  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-0g 14714  df-gsum 14715  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-mhm 15839  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-mgp 17014  df-srg 17030
This theorem is referenced by:  srgbinomlem  17067
  Copyright terms: Public domain W3C validator