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

Theorem srgbinomlem4 16767
Description: Lemma 4 for srgbinomlem 16768. (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 6218 . 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 2454 . . . 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 6228 . . . . 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 11573 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  ZZ )
14 bccl 12218 . . . . . 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 11607 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  ( N  -  k )  e.  NN0 )
1716adantl 466 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  -  k )  e.  NN0 )
18 elfznn0 11601 . . . . . 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 16765 . . . . 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 1221 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
27 eqid 2454 . . . . 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 11915 . . . . 5  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
29 ovex 6228 . . . . . 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 5812 . . . . . 6  |-  ( 0g
`  R )  e. 
_V
3231a1i 11 . . . . 5  |-  ( ph  ->  ( 0g `  R
)  e.  _V )
3327, 28, 30, 32fsuppmptdm 7745 . . . 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 16761 . . 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 16735 . . . . . 6  |-  ( R  e. SRing  ->  R  e. CMnd )
367, 35syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
37 1z 10790 . . . . . 6  |-  1  e.  ZZ
3837a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
39 0zd 10772 . . . . 5  |-  ( ph  ->  0  e.  ZZ )
4012nn0zd 10859 . . . . 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 16739 . . . . . 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 1219 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  e.  S )
45 oveq2 6211 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  ( N  _C  k )  =  ( N  _C  (
j  -  1 ) ) )
46 oveq2 6211 . . . . . . . . 9  |-  ( k  =  ( j  - 
1 )  ->  ( N  -  k )  =  ( N  -  ( j  -  1 ) ) )
4746oveq1d 6218 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
( N  -  k
)  .^  A )  =  ( ( N  -  ( j  - 
1 ) )  .^  A ) )
48 oveq1 6210 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
k  .^  B )  =  ( ( j  -  1 )  .^  B ) )
4947, 48oveq12d 6221 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )
5045, 49oveq12d 6221 . . . . . 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 6218 . . . . 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 16554 . . . 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 10752 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
5453adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  N  e.  CC )
55 elfzelz 11573 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  ZZ )
5655adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  ZZ )
5756zcnd 10862 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  CC )
58 1cnd 9516 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  1  e.  CC )
5954, 57, 58subsub3d 9863 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  -  ( j  -  1 ) )  =  ( ( N  +  1 )  -  j ) )
6059oveq1d 6218 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  -  (
j  -  1 ) )  .^  A )  =  ( ( ( N  +  1 )  -  j )  .^  A ) )
6160oveq1d 6218 . . . . . . . . 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 6219 . . . . . . . 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 6218 . . . . . . 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 10802 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
6655, 65syl 16 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  ZZ )
67 bccl 12218 . . . . . . . . . . 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 16737 . . . . . . . . . . . . 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 10547 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  =  1
7372oveq1i 6213 . . . . . . . . . . . . . 14  |-  ( ( 0  +  1 ) ... ( N  + 
1 ) )  =  ( 1 ... ( N  +  1 ) )
7473eleq2i 2532 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  <->  j  e.  ( 1 ... ( N  +  1 ) ) )
75 fznn0sub 11607 . . . . . . . . . . . . . 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 16722 . . . . . . . . . . . 12  |-  S  =  ( Base `  G
)
8180, 22mulgnn0cl 15765 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  j
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S )
8271, 78, 79, 81syl3anc 1219 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  e.  S )
83 elfznn 11598 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  j  e.  NN )
84 nnm1nn0 10735 . . . . . . . . . . . . . 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 15765 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( j  - 
1 )  .^  B
)  e.  S )
9071, 87, 88, 89syl3anc 1219 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  .^  B )  e.  S )
913, 20, 6srgmulgass 16755 . . . . . . . . . 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 1221 . . . . . . . . 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 2462 . . . . . . . 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 6218 . . . . . . 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 16736 . . . . . . . . . . . 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 15765 . . . . . . . . . 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 1219 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  e.  S )
1003, 6srgass 16740 . . . . . . . . 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 1221 . . . . . . . 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 16720 . . . . . . . . . . . 12  |-  .X.  =  ( +g  `  G )
10380, 22, 102mulgnn0p1 15760 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  +  1 )  .^  B
)  =  ( ( ( j  -  1 )  .^  B )  .X.  B ) )
104103eqcomd 2462 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  .^  B )  .X.  B
)  =  ( ( ( j  -  1 )  +  1 ) 
.^  B ) )
10571, 87, 88, 104syl3anc 1219 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  .^  B
)  .X.  B )  =  ( ( ( j  -  1 )  +  1 )  .^  B ) )
106105oveq2d 6219 . . . . . . . 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 10862 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  CC )
108 1cnd 9516 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  1  e.  CC )
109107, 108npcand 9837 . . . . . . . . . . 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 6218 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  +  1 )  .^  B )  =  ( j  .^  B ) )
112111oveq2d 6219 . . . . . . . 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 2499 . . . . . . 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 2499 . . . . . 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 4489 . . . . 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 6219 . . . 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 4483 . . . . . . . 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 6210 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
j  -  1 )  =  ( k  - 
1 ) )
120119oveq2d 6219 . . . . . . . . . 10  |-  ( j  =  k  ->  ( N  _C  ( j  - 
1 ) )  =  ( N  _C  (
k  -  1 ) ) )
121 oveq2 6211 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( N  +  1 )  -  j )  =  ( ( N  +  1 )  -  k ) )
122121oveq1d 6218 . . . . . . . . . 10  |-  ( j  =  k  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  =  ( ( ( N  +  1 )  -  k )  .^  A ) )
123120, 122oveq12d 6221 . . . . . . . . 9  |-  ( j  =  k  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  =  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) ) )
124 oveq1 6210 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  .^  B )  =  ( k  .^  B ) )
125123, 124oveq12d 6221 . . . . . . . 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 4494 . . . . . . 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 2483 . . . . . 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 6214 . . . . 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 11915 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  e.  Fin )
130 simpl 457 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ph )
131 elfzelz 11573 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  ZZ )
132 peano2zm 10802 . . . . . . . . . . . . 13  |-  ( k  e.  ZZ  ->  (
k  -  1 )  e.  ZZ )
133131, 132syl 16 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
134 bccl 12218 . . . . . . . . . . . 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 11607 . . . . . . . . . . . 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 11598 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN )
139138nnnn0d 10750 . . . . . . . . . . . 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 16765 . . . . . . . . . . 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 1221 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
143142ralrimiva 2830 . . . . . . . . 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 16583 . . . . . . . 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 15563 . . . . . . . 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 10708 . . . . . . . . . . 11  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  NN0 )
149 id 22 . . . . . . . . . . 11  |-  ( ph  ->  ph )
150 0z 10771 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
151150, 37pm3.2i 455 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  /\  1  e.  ZZ )
152 zsubcl 10801 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  1  e.  ZZ )  ->  ( 0  -  1 )  e.  ZZ )
153151, 152mp1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  e.  ZZ )
154 bccl 12218 . . . . . . . . . . . 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 10703 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  N  e.  CC )
157 peano2cn 9655 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  ( N  +  1 )  e.  CC )
158156, 157syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  CC )
159158subid1d 9822 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  =  ( N  +  1 ) )
160 peano2nn0 10734 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
161159, 160eqeltrd 2542 . . . . . . . . . . . 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 16765 . . . . . . . . . . 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 1221 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  e.  S )
165 oveq1 6210 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  -  1 )  =  ( 0  -  1 ) )
166165oveq2d 6219 . . . . . . . . . . . 12  |-  ( k  =  0  ->  ( N  _C  ( k  - 
1 ) )  =  ( N  _C  (
0  -  1 ) ) )
167 oveq2 6211 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( N  +  1 )  -  k )  =  ( ( N  +  1 )  - 
0 ) )
168167oveq1d 6218 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  =  ( ( ( N  +  1 )  -  0 )  .^  A ) )
169 oveq1 6210 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  .^  B )  =  ( 0  .^  B ) )
170168, 169oveq12d 6221 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
) )
171166, 170oveq12d 6221 . . . . . . . . . . 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 16574 . . . . . . . . . 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 1219 . . . . . . . . 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 9976 . . . . . . . . . . . . . . 15  |-  0  <  1
175174a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  1 )
176175, 72syl6breqr 4443 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 0  +  1 ) )
177 0re 9500 . . . . . . . . . . . . . . 15  |-  0  e.  RR
178 1re 9499 . . . . . . . . . . . . . . 15  |-  1  e.  RR
179177, 178, 1773pm3.2i 1166 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )
180 ltsubadd 9923 . . . . . . . . . . . . . 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 12203 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ  /\  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )  ->  ( N  _C  ( 0  -  1 ) )  =  0 )
18512, 153, 183, 184syl3anc 1219 . . . . . . . . . 10  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  =  0 )
186185oveq1d 6218 . . . . . . . . 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 15765 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  0 )  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18870, 162, 23, 187syl3anc 1219 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18980, 22mulgnn0cl 15765 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  0  e.  NN0  /\  B  e.  S )  ->  (
0  .^  B )  e.  S )
19070, 148, 10, 189syl3anc 1219 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  .^  B
)  e.  S )
1913, 6srgcl 16739 . . . . . . . . . . 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 1219 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
)  e.  S )
1933, 4, 20mulg0 15754 . . . . . . . . . 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 2500 . . . . . . . 8  |-  ( ph  ->  ( 0g `  R
)  =  ( R 
gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) ) )
196195oveq1d 6218 . . . . . . 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 2497 . . . . . 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 15765 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  k
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  k )  .^  A
)  e.  S )
202199, 137, 200, 201syl3anc 1219 . . . . . . . . 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 15765 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  k  e.  NN0  /\  B  e.  S )  ->  (
k  .^  B )  e.  S )
205199, 140, 203, 204syl3anc 1219 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
k  .^  B )  e.  S )
2063, 20, 6srgmulgass 16755 . . . . . . . . 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 1221 . . . . . . . 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 4489 . . . . . . 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 6219 . . . . . 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 11573 . . . . . . . . . . 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 11607 . . . . . . . . . 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 11601 . . . . . . . . . 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 1221 . . . . . . . 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 16551 . . . . . . 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 7503 . . . . . . . . . 10  |-  { 0 }  e.  Fin
222221a1i 11 . . . . . . . . 9  |-  ( ph  ->  { 0 }  e.  Fin )
223171eleq1d 2523 . . . . . . . . . . . 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 4023 . . . . . . . . . . 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 16583 . . . . . . . 8  |-  ( ph  ->  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  e.  S )
2283, 5cmncom 16417 . . . . . . . 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 1219 . . . . . . 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 2495 . . . . . 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 2505 . . . . 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 2507 . . . 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 2499 . . 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 2497 . 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 2517 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 1370    e. wcel 1758   A.wral 2799   _Vcvv 3078   {csn 3988   class class class wbr 4403    |-> cmpt 4461   ` cfv 5529  (class class class)co 6203   Fincfn 7423   CCcc 9394   RRcr 9395   0cc0 9396   1c1 9397    + caddc 9399    < clt 9532    - cmin 9709   NNcn 10436   NN0cn0 10693   ZZcz 10760   ...cfz 11557    _C cbc 12198   Basecbs 14295   +g cplusg 14360   .rcmulr 14361   0gc0g 14500    gsumg cgsu 14501   Mndcmnd 15531  .gcmg 15536  CMndccmn 16401  mulGrpcmgp 16716  SRingcsrg 16732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-inf2 7961  ax-cnex 9452  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-iin 4285  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-of 6433  df-om 6590  df-1st 6690  df-2nd 6691  df-supp 6804  df-recs 6945  df-rdg 6979  df-1o 7033  df-oadd 7037  df-er 7214  df-map 7329  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-fsupp 7735  df-oi 7838  df-card 8223  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-div 10108  df-nn 10437  df-2 10494  df-n0 10694  df-z 10761  df-uz 10976  df-rp 11106  df-fz 11558  df-fzo 11669  df-seq 11927  df-fac 12172  df-bc 12199  df-hash 12224  df-ndx 14298  df-slot 14299  df-base 14300  df-sets 14301  df-ress 14302  df-plusg 14373  df-0g 14502  df-gsum 14503  df-mre 14646  df-mrc 14647  df-acs 14649  df-mnd 15537  df-mhm 15586  df-submnd 15587  df-mulg 15670  df-cntz 15957  df-cmn 16403  df-mgp 16717  df-srg 16733
This theorem is referenced by:  srgbinomlem  16768
  Copyright terms: Public domain W3C validator