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

Theorem srgbinomlem4 17711
Description: Lemma 4 for srgbinomlem 17712. (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 6320 . 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 2429 . . . 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 6333 . . . . 5  |-  ( 0 ... N )  e. 
_V
98a1i 11 . . . 4  |-  ( ph  ->  ( 0 ... N
)  e.  _V )
10 srgbinomlem.b . . . 4  |-  ( ph  ->  B  e.  S )
11 simpl 458 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ph )
12 srgbinomlem.n . . . . . 6  |-  ( ph  ->  N  e.  NN0 )
13 elfzelz 11798 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  ZZ )
14 bccl 12504 . . . . . 6  |-  ( ( N  e.  NN0  /\  k  e.  ZZ )  ->  ( N  _C  k
)  e.  NN0 )
1512, 13, 14syl2an 479 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  _C  k )  e. 
NN0 )
16 fznn0sub 11829 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  ( N  -  k )  e.  NN0 )
1716adantl 467 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( N  -  k )  e.  NN0 )
18 elfznn0 11885 . . . . . 6  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
1918adantl 467 . . . . 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 17709 . . . . 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 1266 . . . 4  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( N  _C  k
)  .x.  ( (
( N  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
27 eqid 2429 . . . . 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 12183 . . . . 5  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
29 ovex 6333 . . . . . 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 5891 . . . . . 6  |-  ( 0g
`  R )  e. 
_V
3231a1i 11 . . . . 5  |-  ( ph  ->  ( 0g `  R
)  e.  _V )
3327, 28, 30, 32fsuppmptdm 7900 . . . 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 17705 . . 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 17677 . . . . . 6  |-  ( R  e. SRing  ->  R  e. CMnd )
367, 35syl 17 . . . . 5  |-  ( ph  ->  R  e. CMnd )
37 1z 10967 . . . . . 6  |-  1  e.  ZZ
3837a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
39 0zd 10949 . . . . 5  |-  ( ph  ->  0  e.  ZZ )
4012nn0zd 11038 . . . . 5  |-  ( ph  ->  N  e.  ZZ )
417adantr 466 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  R  e. SRing )
4210adantr 466 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  S )
433, 6srgcl 17681 . . . . . 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 1264 . . . . 5  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( N  _C  k )  .x.  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) ) ) 
.X.  B )  e.  S )
45 oveq2 6313 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  ( N  _C  k )  =  ( N  _C  (
j  -  1 ) ) )
46 oveq2 6313 . . . . . . . . 9  |-  ( k  =  ( j  - 
1 )  ->  ( N  -  k )  =  ( N  -  ( j  -  1 ) ) )
4746oveq1d 6320 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
( N  -  k
)  .^  A )  =  ( ( N  -  ( j  - 
1 ) )  .^  A ) )
48 oveq1 6312 . . . . . . . 8  |-  ( k  =  ( j  - 
1 )  ->  (
k  .^  B )  =  ( ( j  -  1 )  .^  B ) )
4947, 48oveq12d 6323 . . . . . . 7  |-  ( k  =  ( j  - 
1 )  ->  (
( ( N  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( N  -  ( j  - 
1 ) )  .^  A )  .X.  (
( j  -  1 )  .^  B )
) )
5045, 49oveq12d 6323 . . . . . 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 6320 . . . . 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 17504 . . . 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 10927 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  CC )
5453adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  N  e.  CC )
55 elfzelz 11798 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  ZZ )
5655adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  ZZ )
5756zcnd 11041 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  j  e.  CC )
58 1cnd 9658 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  1  e.  CC )
5954, 57, 58subsub3d 10015 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  -  ( j  -  1 ) )  =  ( ( N  +  1 )  -  j ) )
6059oveq1d 6320 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  -  (
j  -  1 ) )  .^  A )  =  ( ( ( N  +  1 )  -  j )  .^  A ) )
6160oveq1d 6320 . . . . . . . . 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 6321 . . . . . . . 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 6320 . . . . . . 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 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  R  e. SRing )
65 peano2zm 10980 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
6655, 65syl 17 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  ZZ )
67 bccl 12504 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( j  -  1 )  e.  ZZ )  ->  ( N  _C  ( j  -  1 ) )  e.  NN0 )
6812, 66, 67syl2an 479 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  ( N  _C  ( j  - 
1 ) )  e. 
NN0 )
6921srgmgp 17679 . . . . . . . . . . . . 13  |-  ( R  e. SRing  ->  G  e.  Mnd )
707, 69syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  G  e.  Mnd )
7170adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  G  e.  Mnd )
72 0p1e1 10721 . . . . . . . . . . . . . . 15  |-  ( 0  +  1 )  =  1
7372oveq1i 6315 . . . . . . . . . . . . . 14  |-  ( ( 0  +  1 ) ... ( N  + 
1 ) )  =  ( 1 ... ( N  +  1 ) )
7473eleq2i 2507 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  <->  j  e.  ( 1 ... ( N  +  1 ) ) )
75 fznn0sub 11829 . . . . . . . . . . . . . 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 220 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  ( ( N  +  1 )  -  j )  e.  NN0 ) )
7877imp 430 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  j )  e.  NN0 )
7923adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  A  e.  S )
8021, 3mgpbas 17664 . . . . . . . . . . . 12  |-  S  =  ( Base `  G
)
8180, 22mulgnn0cl 16725 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  j
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  j )  .^  A
)  e.  S )
8271, 78, 79, 81syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  e.  S )
83 elfznn 11826 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  j  e.  NN )
84 nnm1nn0 10911 . . . . . . . . . . . . . 14  |-  ( j  e.  NN  ->  (
j  -  1 )  e.  NN0 )
8583, 84syl 17 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  NN0 )
8674, 85sylbi 198 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
j  -  1 )  e.  NN0 )
8786adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
j  -  1 )  e.  NN0 )
8810adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  B  e.  S )
8980, 22mulgnn0cl 16725 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( j  - 
1 )  .^  B
)  e.  S )
9071, 87, 88, 89syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  .^  B )  e.  S )
913, 20, 6srgmulgass 17699 . . . . . . . . . 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 1266 . . . . . . . . 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 2437 . . . . . . . 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 6320 . . . . . . 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 17678 . . . . . . . . . . . 12  |-  ( R  e. SRing  ->  R  e.  Mnd )
967, 95syl 17 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Mnd )
9796adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  R  e.  Mnd )
983, 20mulgnn0cl 16725 . . . . . . . . . 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 1264 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  e.  S )
1003, 6srgass 17682 . . . . . . . . 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 1266 . . . . . . . 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 17662 . . . . . . . . . . . 12  |-  .X.  =  ( +g  `  G )
10380, 22, 102mulgnn0p1 16720 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  +  1 )  .^  B
)  =  ( ( ( j  -  1 )  .^  B )  .X.  B ) )
104103eqcomd 2437 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( j  -  1 )  e.  NN0  /\  B  e.  S )  ->  ( ( ( j  -  1 )  .^  B )  .X.  B
)  =  ( ( ( j  -  1 )  +  1 ) 
.^  B ) )
10571, 87, 88, 104syl3anc 1264 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  .^  B
)  .X.  B )  =  ( ( ( j  -  1 )  +  1 )  .^  B ) )
106105oveq2d 6321 . . . . . . . 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 11041 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  j  e.  CC )
108 1cnd 9658 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  1  e.  CC )
109107, 108npcand 9989 . . . . . . . . . . 11  |-  ( j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) )  ->  (
( j  -  1 )  +  1 )  =  j )
110109adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( j  -  1 )  +  1 )  =  j )
111110oveq1d 6320 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( 0  +  1 ) ... ( N  +  1 ) ) )  ->  (
( ( j  - 
1 )  +  1 )  .^  B )  =  ( j  .^  B ) )
112111oveq2d 6321 . . . . . . . 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 4512 . . . . 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 6321 . . . 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 4506 . . . . . . . 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 6312 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
j  -  1 )  =  ( k  - 
1 ) )
120119oveq2d 6321 . . . . . . . . . 10  |-  ( j  =  k  ->  ( N  _C  ( j  - 
1 ) )  =  ( N  _C  (
k  -  1 ) ) )
121 oveq2 6313 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( N  +  1 )  -  j )  =  ( ( N  +  1 )  -  k ) )
122121oveq1d 6320 . . . . . . . . . 10  |-  ( j  =  k  ->  (
( ( N  + 
1 )  -  j
)  .^  A )  =  ( ( ( N  +  1 )  -  k )  .^  A ) )
123120, 122oveq12d 6323 . . . . . . . . 9  |-  ( j  =  k  ->  (
( N  _C  (
j  -  1 ) )  .x.  ( ( ( N  +  1 )  -  j ) 
.^  A ) )  =  ( ( N  _C  ( k  - 
1 ) )  .x.  ( ( ( N  +  1 )  -  k )  .^  A
) ) )
124 oveq1 6312 . . . . . . . . 9  |-  ( j  =  k  ->  (
j  .^  B )  =  ( k  .^  B ) )
125123, 124oveq12d 6323 . . . . . . . 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 4518 . . . . . . 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 6316 . . . . 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 12183 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  e.  Fin )
130 simpl 458 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ph )
131 elfzelz 11798 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  ZZ )
132 peano2zm 10980 . . . . . . . . . . . . 13  |-  ( k  e.  ZZ  ->  (
k  -  1 )  e.  ZZ )
133131, 132syl 17 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
134 bccl 12504 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( k  -  1 )  e.  ZZ )  ->  ( N  _C  ( k  -  1 ) )  e.  NN0 )
13512, 133, 134syl2an 479 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( N  _C  ( k  - 
1 ) )  e. 
NN0 )
136 fznn0sub 11829 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
137136adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
138 elfznn 11826 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN )
139138nnnn0d 10925 . . . . . . . . . . . 12  |-  ( k  e.  ( 1 ... ( N  +  1 ) )  ->  k  e.  NN0 )
140139adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  k  e.  NN0 )
1413, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 17709 . . . . . . . . . . 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 1266 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( N  _C  (
k  -  1 ) )  .x.  ( ( ( ( N  + 
1 )  -  k
)  .^  A )  .X.  ( k  .^  B
) ) )  e.  S )
143142ralrimiva 2846 . . . . . . . . 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 17534 . . . . . . . 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 16508 . . . . . . . 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 665 . . . . . . 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 10884 . . . . . . . . . . 11  |-  0  e.  NN0
148147a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  NN0 )
149 id 23 . . . . . . . . . . 11  |-  ( ph  ->  ph )
150 0z 10948 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
151150, 37pm3.2i 456 . . . . . . . . . . . . 13  |-  ( 0  e.  ZZ  /\  1  e.  ZZ )
152 zsubcl 10979 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  1  e.  ZZ )  ->  ( 0  -  1 )  e.  ZZ )
153151, 152mp1i 13 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  e.  ZZ )
154 bccl 12504 . . . . . . . . . . . 12  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ )  ->  ( N  _C  ( 0  -  1 ) )  e.  NN0 )
15512, 153, 154syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  e.  NN0 )
156 nn0cn 10879 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  N  e.  CC )
157 peano2cn 9804 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  ( N  +  1 )  e.  CC )
158156, 157syl 17 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  CC )
159158subid1d 9974 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  =  ( N  +  1 ) )
160 peano2nn0 10910 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
161159, 160eqeltrd 2517 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( ( N  +  1 )  -  0 )  e. 
NN0 )
16212, 161syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  + 
1 )  -  0 )  e.  NN0 )
1633, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 17709 . . . . . . . . . . 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 1266 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  _C  ( 0  -  1 ) )  .x.  (
( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) ) )  e.  S )
165 oveq1 6312 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  -  1 )  =  ( 0  -  1 ) )
166165oveq2d 6321 . . . . . . . . . . . 12  |-  ( k  =  0  ->  ( N  _C  ( k  - 
1 ) )  =  ( N  _C  (
0  -  1 ) ) )
167 oveq2 6313 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( N  +  1 )  -  k )  =  ( ( N  +  1 )  - 
0 ) )
168167oveq1d 6320 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  =  ( ( ( N  +  1 )  -  0 )  .^  A ) )
169 oveq1 6312 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  .^  B )  =  ( 0  .^  B ) )
170168, 169oveq12d 6323 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( ( N  +  1 )  -  k )  .^  A
)  .X.  ( k  .^  B ) )  =  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
) )
171166, 170oveq12d 6323 . . . . . . . . . . 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 17522 . . . . . . . . . 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 1264 . . . . . . . . 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 10135 . . . . . . . . . . . . . . 15  |-  0  <  1
175174a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  1 )
176175, 72syl6breqr 4466 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( 0  +  1 ) )
177 0re 9642 . . . . . . . . . . . . . . 15  |-  0  e.  RR
178 1re 9641 . . . . . . . . . . . . . . 15  |-  1  e.  RR
179177, 178, 1773pm3.2i 1183 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )
180 ltsubadd 10083 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  0  e.  RR )  ->  (
( 0  -  1 )  <  0  <->  0  <  ( 0  +  1 ) ) )
181179, 180mp1i 13 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 0  -  1 )  <  0  <->  0  <  ( 0  +  1 ) ) )
182176, 181mpbird 235 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  -  1 )  <  0 )
183182orcd 393 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )
184 bcval4 12489 . . . . . . . . . . 11  |-  ( ( N  e.  NN0  /\  ( 0  -  1 )  e.  ZZ  /\  ( ( 0  -  1 )  <  0  \/  N  <  ( 0  -  1 ) ) )  ->  ( N  _C  ( 0  -  1 ) )  =  0 )
18512, 153, 183, 184syl3anc 1264 . . . . . . . . . 10  |-  ( ph  ->  ( N  _C  (
0  -  1 ) )  =  0 )
186185oveq1d 6320 . . . . . . . . 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 16725 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  0 )  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18870, 162, 23, 187syl3anc 1264 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  +  1 )  - 
0 )  .^  A
)  e.  S )
18980, 22mulgnn0cl 16725 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  0  e.  NN0  /\  B  e.  S )  ->  (
0  .^  B )  e.  S )
19070, 148, 10, 189syl3anc 1264 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  .^  B
)  e.  S )
1913, 6srgcl 17681 . . . . . . . . . . 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 1264 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( N  +  1 )  -  0 )  .^  A )  .X.  (
0  .^  B )
)  e.  S )
1933, 4, 20mulg0 16714 . . . . . . . . . 10  |-  ( ( ( ( ( N  +  1 )  - 
0 )  .^  A
)  .X.  ( 0 
.^  B ) )  e.  S  ->  (
0  .x.  ( (
( ( N  + 
1 )  -  0 )  .^  A )  .X.  ( 0  .^  B
) ) )  =  ( 0g `  R
) )
194192, 193syl 17 . . . . . . . . 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 6320 . . . . . . 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 466 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  R  e. SRing )
19970adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  G  e.  Mnd )
20023adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  A  e.  S )
20180, 22mulgnn0cl 16725 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  ( ( N  + 
1 )  -  k
)  e.  NN0  /\  A  e.  S )  ->  ( ( ( N  +  1 )  -  k )  .^  A
)  e.  S )
202199, 137, 200, 201syl3anc 1264 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( ( N  + 
1 )  -  k
)  .^  A )  e.  S )
20310adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  B  e.  S )
20480, 22mulgnn0cl 16725 . . . . . . . . . 10  |-  ( ( G  e.  Mnd  /\  k  e.  NN0  /\  B  e.  S )  ->  (
k  .^  B )  e.  S )
205199, 140, 203, 204syl3anc 1264 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
k  .^  B )  e.  S )
2063, 20, 6srgmulgass 17699 . . . . . . . . 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 1266 . . . . . . . 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 4512 . . . . . . 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 6321 . . . . . 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 17 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
211 simpl 458 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ph )
212 elfzelz 11798 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  ZZ )
213212, 132syl 17 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
k  -  1 )  e.  ZZ )
21412, 213, 134syl2an 479 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  ( N  _C  ( k  - 
1 ) )  e. 
NN0 )
215 fznn0sub 11829 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
216215adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  (
( N  +  1 )  -  k )  e.  NN0 )
217 elfznn0 11885 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( N  +  1 ) )  ->  k  e.  NN0 )
218217adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... ( N  +  1 ) ) )  ->  k  e.  NN0 )
219211, 214, 216, 218, 141syl13anc 1266 . . . . . . . 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 17501 . . . . . . 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 7657 . . . . . . . . . 10  |-  { 0 }  e.  Fin
222221a1i 11 . . . . . . . . 9  |-  ( ph  ->  { 0 }  e.  Fin )
223171eleq1d 2498 . . . . . . . . . . . 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 4037 . . . . . . . . . . 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 215 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  {
0 }  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) )  e.  S )
2273, 36, 222, 226gsummptcl 17534 . . . . . . . 8  |-  ( ph  ->  ( R  gsumg  ( k  e.  {
0 }  |->  ( ( N  _C  ( k  -  1 ) ) 
.x.  ( ( ( ( N  +  1 )  -  k ) 
.^  A )  .X.  ( k  .^  B
) ) ) ) )  e.  S )
2283, 5cmncom 17381 . . . . . . . 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 1264 . . . . . . 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 2470 . . . . . 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 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 ) ) ) ) ) )
232128, 231syl5eq 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 ) ) ) ) ) )
23352, 116, 2323eqtrd 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 ) ) ) ) ) )
23434, 233eqtr3d 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
) ) ) ) ) )
2352, 234sylan9eqr 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 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   A.wral 2782   _Vcvv 3087   {csn 4002   class class class wbr 4426    |-> cmpt 4484   ` cfv 5601  (class class class)co 6305   Fincfn 7577   CCcc 9536   RRcr 9537   0cc0 9538   1c1 9539    + caddc 9541    < clt 9674    - cmin 9859   NNcn 10609   NN0cn0 10869   ZZcz 10937   ...cfz 11782    _C cbc 12484   Basecbs 15084   +g cplusg 15152   .rcmulr 15153   0gc0g 15297    gsumg cgsu 15298   Mndcmnd 16486  .gcmg 16623  CMndccmn 17365  mulGrpcmgp 17658  SRingcsrg 17674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fsupp 7890  df-oi 8025  df-card 8372  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-fz 11783  df-fzo 11914  df-seq 12211  df-fac 12457  df-bc 12485  df-hash 12513  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-0g 15299  df-gsum 15300  df-mre 15443  df-mrc 15444  df-acs 15446  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-mhm 16533  df-submnd 16534  df-mulg 16627  df-cntz 16922  df-cmn 17367  df-mgp 17659  df-srg 17675
This theorem is referenced by:  srgbinomlem  17712
  Copyright terms: Public domain W3C validator