Metamath Proof Explorer

Theorem srgbinomlem4

Description: Lemma 4 for srgbinomlem . (Contributed by AV, 24-Aug-2019) (Proof shortened by AV, 19-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 srgbinom.s 
 |-  S = ( Base ` R )
2 srgbinom.m 
 |-  .X. = ( .r ` R )
3 srgbinom.t 
 |-  .x. = ( .g ` R )
4 srgbinom.a 
 |-  .+ = ( +g ` R )
5 srgbinom.g 
 |-  G = ( mulGrp ` R )
6 srgbinom.e 
 |-  .^ = ( .g ` G )
7 srgbinomlem.r 
 |-  ( ph -> R e. SRing )
8 srgbinomlem.a 
 |-  ( ph -> A e. S )
9 srgbinomlem.b 
 |-  ( ph -> B e. S )
10 srgbinomlem.c 
 |-  ( ph -> ( A .X. B ) = ( B .X. A ) )
11 srgbinomlem.n 
 |-  ( ph -> N e. NN0 )
12 srgbinomlem.i 
 |-  ( ps -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
13 12 oveq1d 
 |-  ( ps -> ( ( N .^ ( A .+ B ) ) .X. B ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. B ) )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
16 simpl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ph )
17 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
18 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
19 11 17 18 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
20 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
21 20 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
22 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
23 22 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
24 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( ph /\ ( ( N _C k ) e. NN0 /\ ( N - k ) e. NN0 /\ k e. NN0 ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
25 16 19 21 23 24 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
26 eqid 
 |-  ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) = ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) )
27 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
28 ovexd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) e. _V )
29 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
30 26 27 28 29 fsuppmptdm 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) finSupp ( 0g ` R ) )
31 1 14 4 2 7 15 9 25 30 srgsummulcr 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. B ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. B ) )
32 srgcmn 
 |-  ( R e. SRing -> R e. CMnd )
33 7 32 syl 
 |-  ( ph -> R e. CMnd )
34 1z 
 |-  1 e. ZZ
35 34 a1i 
 |-  ( ph -> 1 e. ZZ )
36 0zd 
 |-  ( ph -> 0 e. ZZ )
37 11 nn0zd 
 |-  ( ph -> N e. ZZ )
38 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> R e. SRing )
39 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. S )
40 1 2 srgcl 
 |-  ( ( 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 )
41 38 25 39 40 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. B ) e. S )
42 oveq2 
 |-  ( k = ( j - 1 ) -> ( N _C k ) = ( N _C ( j - 1 ) ) )
43 oveq2 
 |-  ( k = ( j - 1 ) -> ( N - k ) = ( N - ( j - 1 ) ) )
44 43 oveq1d 
 |-  ( k = ( j - 1 ) -> ( ( N - k ) .^ A ) = ( ( N - ( j - 1 ) ) .^ A ) )
45 oveq1 
 |-  ( k = ( j - 1 ) -> ( k .^ B ) = ( ( j - 1 ) .^ B ) )
46 44 45 oveq12d 
 |-  ( k = ( j - 1 ) -> ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( N - ( j - 1 ) ) .^ A ) .X. ( ( j - 1 ) .^ B ) ) )
47 42 46 oveq12d 
 |-  ( 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 ) ) ) )
48 47 oveq1d 
 |-  ( 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 ) )
49 1 14 33 35 36 37 41 48 gsummptshft 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. B ) ) ) = ( R gsum ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) |-> ( ( ( N _C ( j - 1 ) ) .x. ( ( ( N - ( j - 1 ) ) .^ A ) .X. ( ( j - 1 ) .^ B ) ) ) .X. B ) ) ) )
50 11 nn0cnd 
 |-  ( ph -> N e. CC )
51 50 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> N e. CC )
52 elfzelz 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> j e. ZZ )
53 52 adantl 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> j e. ZZ )
54 53 zcnd 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> j e. CC )
55 1cnd 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> 1 e. CC )
56 51 54 55 subsub3d 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( N - ( j - 1 ) ) = ( ( N + 1 ) - j ) )
57 56 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N - ( j - 1 ) ) .^ A ) = ( ( ( N + 1 ) - j ) .^ A ) )
58 57 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N - ( j - 1 ) ) .^ A ) .X. ( ( j - 1 ) .^ B ) ) = ( ( ( ( N + 1 ) - j ) .^ A ) .X. ( ( j - 1 ) .^ B ) ) )
59 58 oveq2d 
 |-  ( ( 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 ) ) ) )
60 59 oveq1d 
 |-  ( ( 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 ) )
61 7 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> R e. SRing )
62 peano2zm 
 |-  ( j e. ZZ -> ( j - 1 ) e. ZZ )
63 52 62 syl 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( j - 1 ) e. ZZ )
64 bccl 
 |-  ( ( N e. NN0 /\ ( j - 1 ) e. ZZ ) -> ( N _C ( j - 1 ) ) e. NN0 )
65 11 63 64 syl2an 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( N _C ( j - 1 ) ) e. NN0 )
66 5 srgmgp 
 |-  ( R e. SRing -> G e. Mnd )
67 7 66 syl 
 |-  ( ph -> G e. Mnd )
68 67 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> G e. Mnd )
69 0p1e1 
 |-  ( 0 + 1 ) = 1
70 69 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) )
71 70 eleq2i 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) <-> j e. ( 1 ... ( N + 1 ) ) )
72 fznn0sub 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 )
73 72 a1i 
 |-  ( ph -> ( j e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 ) )
74 71 73 syl5bi 
 |-  ( ph -> ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 ) )
75 74 imp 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N + 1 ) - j ) e. NN0 )
76 8 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> A e. S )
77 5 1 mgpbas 
 |-  S = ( Base ` G )
78 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( ( N + 1 ) - j ) e. NN0 /\ A e. S ) -> ( ( ( N + 1 ) - j ) .^ A ) e. S )
79 68 75 76 78 syl3anc 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - j ) .^ A ) e. S )
80 elfznn 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. NN )
81 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
82 80 81 syl 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( j - 1 ) e. NN0 )
83 71 82 sylbi 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( j - 1 ) e. NN0 )
84 83 adantl 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( j - 1 ) e. NN0 )
85 9 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> B e. S )
86 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( j - 1 ) e. NN0 /\ B e. S ) -> ( ( j - 1 ) .^ B ) e. S )
87 68 84 85 86 syl3anc 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( j - 1 ) .^ B ) e. S )
88 1 3 2 srgmulgass 
 |-  ( ( 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 ) ) ) )
89 61 65 79 87 88 syl13anc 
 |-  ( ( 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 ) ) ) )
90 89 eqcomd 
 |-  ( ( 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 ) ) )
91 90 oveq1d 
 |-  ( ( 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 ) )
92 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
93 7 92 syl 
 |-  ( ph -> R e. Mnd )
94 93 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> R e. Mnd )
95 1 3 mulgnn0cl 
 |-  ( ( 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 )
96 94 65 79 95 syl3anc 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) e. S )
97 1 2 srgass 
 |-  ( ( 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 ) ) )
98 61 96 87 85 97 syl13anc 
 |-  ( ( 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 ) ) )
99 5 2 mgpplusg 
 |-  .X. = ( +g ` G )
100 77 6 99 mulgnn0p1 
 |-  ( ( G e. Mnd /\ ( j - 1 ) e. NN0 /\ B e. S ) -> ( ( ( j - 1 ) + 1 ) .^ B ) = ( ( ( j - 1 ) .^ B ) .X. B ) )
101 100 eqcomd 
 |-  ( ( G e. Mnd /\ ( j - 1 ) e. NN0 /\ B e. S ) -> ( ( ( j - 1 ) .^ B ) .X. B ) = ( ( ( j - 1 ) + 1 ) .^ B ) )
102 68 84 85 101 syl3anc 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( j - 1 ) .^ B ) .X. B ) = ( ( ( j - 1 ) + 1 ) .^ B ) )
103 102 oveq2d 
 |-  ( ( 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 ) ) )
104 52 zcnd 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> j e. CC )
105 1cnd 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> 1 e. CC )
106 104 105 npcand 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
107 106 adantl 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( j - 1 ) + 1 ) = j )
108 107 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( j - 1 ) + 1 ) .^ B ) = ( j .^ B ) )
109 108 oveq2d 
 |-  ( ( 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 ) ) )
110 98 103 109 3eqtrd 
 |-  ( ( 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 ) ) )
111 60 91 110 3eqtrd 
 |-  ( ( 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 ) ) )
112 111 mpteq2dva 
 |-  ( 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 ) ) ) )
113 112 oveq2d 
 |-  ( ph -> ( R gsum ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) |-> ( ( ( N _C ( j - 1 ) ) .x. ( ( ( N - ( j - 1 ) ) .^ A ) .X. ( ( j - 1 ) .^ B ) ) ) .X. B ) ) ) = ( R gsum ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) |-> ( ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) .X. ( j .^ B ) ) ) ) )
114 70 mpteq1i 
 |-  ( 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 ) ) )
115 oveq1 
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
116 115 oveq2d 
 |-  ( j = k -> ( N _C ( j - 1 ) ) = ( N _C ( k - 1 ) ) )
117 oveq2 
 |-  ( j = k -> ( ( N + 1 ) - j ) = ( ( N + 1 ) - k ) )
118 117 oveq1d 
 |-  ( j = k -> ( ( ( N + 1 ) - j ) .^ A ) = ( ( ( N + 1 ) - k ) .^ A ) )
119 116 118 oveq12d 
 |-  ( j = k -> ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) = ( ( N _C ( k - 1 ) ) .x. ( ( ( N + 1 ) - k ) .^ A ) ) )
120 oveq1 
 |-  ( j = k -> ( j .^ B ) = ( k .^ B ) )
121 119 120 oveq12d 
 |-  ( 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 ) ) )
122 121 cbvmptv 
 |-  ( 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 ) ) )
123 114 122 eqtri 
 |-  ( 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 ) ) )
124 123 oveq2i 
 |-  ( R gsum ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) |-> ( ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) .X. ( j .^ B ) ) ) ) = ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( ( N _C ( k - 1 ) ) .x. ( ( ( N + 1 ) - k ) .^ A ) ) .X. ( k .^ B ) ) ) )
125 fzfid 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) e. Fin )
126 simpl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ph )
127 elfzelz 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. ZZ )
128 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
129 127 128 syl 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
130 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
131 11 129 130 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
132 fznn0sub 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
133 132 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
134 elfznn 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN )
135 134 nnnn0d 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN0 )
136 135 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. NN0 )
137 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( 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 )
138 126 131 133 136 137 syl13anc 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
139 138 ralrimiva 
 |-  ( ph -> A. k e. ( 1 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
140 1 33 125 139 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S )
141 1 4 14 mndlid 
 |-  ( ( R e. Mnd /\ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S ) -> ( ( 0g ` R ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
142 93 140 141 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
143 0nn0 
 |-  0 e. NN0
144 143 a1i 
 |-  ( ph -> 0 e. NN0 )
145 id 
 |-  ( ph -> ph )
146 0z 
 |-  0 e. ZZ
147 146 34 pm3.2i 
 |-  ( 0 e. ZZ /\ 1 e. ZZ )
148 zsubcl 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( 0 - 1 ) e. ZZ )
149 147 148 mp1i 
 |-  ( ph -> ( 0 - 1 ) e. ZZ )
150 bccl 
 |-  ( ( N e. NN0 /\ ( 0 - 1 ) e. ZZ ) -> ( N _C ( 0 - 1 ) ) e. NN0 )
151 11 149 150 syl2anc 
 |-  ( ph -> ( N _C ( 0 - 1 ) ) e. NN0 )
152 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
153 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
154 152 153 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
155 154 subid1d 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 0 ) = ( N + 1 ) )
156 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
157 155 156 eqeltrd 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 0 ) e. NN0 )
158 11 157 syl 
 |-  ( ph -> ( ( N + 1 ) - 0 ) e. NN0 )
159 1 2 3 4 5 6 7 8 9 10 11 srgbinomlem2 
 |-  ( ( 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 )
160 145 151 158 144 159 syl13anc 
 |-  ( ph -> ( ( N _C ( 0 - 1 ) ) .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) e. S )
161 oveq1 
 |-  ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
162 161 oveq2d 
 |-  ( k = 0 -> ( N _C ( k - 1 ) ) = ( N _C ( 0 - 1 ) ) )
163 oveq2 
 |-  ( k = 0 -> ( ( N + 1 ) - k ) = ( ( N + 1 ) - 0 ) )
164 163 oveq1d 
 |-  ( k = 0 -> ( ( ( N + 1 ) - k ) .^ A ) = ( ( ( N + 1 ) - 0 ) .^ A ) )
165 oveq1 
 |-  ( k = 0 -> ( k .^ B ) = ( 0 .^ B ) )
166 164 165 oveq12d 
 |-  ( k = 0 -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) )
167 162 166 oveq12d 
 |-  ( 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 ) ) ) )
168 1 167 gsumsn 
 |-  ( ( R e. Mnd /\ 0 e. NN0 /\ ( ( N _C ( 0 - 1 ) ) .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) e. S ) -> ( R gsum ( 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 ) ) ) )
169 93 144 160 168 syl3anc 
 |-  ( ph -> ( R gsum ( 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 ) ) ) )
170 0lt1 
 |-  0 < 1
171 170 a1i 
 |-  ( ph -> 0 < 1 )
172 171 69 breqtrrdi 
 |-  ( ph -> 0 < ( 0 + 1 ) )
173 0re 
 |-  0 e. RR
174 1re 
 |-  1 e. RR
175 173 174 173 3pm3.2i 
 |-  ( 0 e. RR /\ 1 e. RR /\ 0 e. RR )
176 ltsubadd 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 0 e. RR ) -> ( ( 0 - 1 ) < 0 <-> 0 < ( 0 + 1 ) ) )
177 175 176 mp1i 
 |-  ( ph -> ( ( 0 - 1 ) < 0 <-> 0 < ( 0 + 1 ) ) )
178 172 177 mpbird 
 |-  ( ph -> ( 0 - 1 ) < 0 )
179 178 orcd 
 |-  ( ph -> ( ( 0 - 1 ) < 0 \/ N < ( 0 - 1 ) ) )
180 bcval4 
 |-  ( ( N e. NN0 /\ ( 0 - 1 ) e. ZZ /\ ( ( 0 - 1 ) < 0 \/ N < ( 0 - 1 ) ) ) -> ( N _C ( 0 - 1 ) ) = 0 )
181 11 149 179 180 syl3anc 
 |-  ( ph -> ( N _C ( 0 - 1 ) ) = 0 )
182 181 oveq1d 
 |-  ( ph -> ( ( N _C ( 0 - 1 ) ) .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) )
183 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( ( N + 1 ) - 0 ) e. NN0 /\ A e. S ) -> ( ( ( N + 1 ) - 0 ) .^ A ) e. S )
184 67 158 8 183 syl3anc 
 |-  ( ph -> ( ( ( N + 1 ) - 0 ) .^ A ) e. S )
185 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ 0 e. NN0 /\ B e. S ) -> ( 0 .^ B ) e. S )
186 67 144 9 185 syl3anc 
 |-  ( ph -> ( 0 .^ B ) e. S )
187 1 2 srgcl 
 |-  ( ( R e. SRing /\ ( ( ( N + 1 ) - 0 ) .^ A ) e. S /\ ( 0 .^ B ) e. S ) -> ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) e. S )
188 7 184 186 187 syl3anc 
 |-  ( ph -> ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) e. S )
189 1 14 3 mulg0 
 |-  ( ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) e. S -> ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0g ` R ) )
190 188 189 syl 
 |-  ( ph -> ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0g ` R ) )
191 169 182 190 3eqtrrd 
 |-  ( ph -> ( 0g ` R ) = ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
192 191 oveq1d 
 |-  ( ph -> ( ( 0g ` R ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
193 142 192 eqtr3d 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
194 7 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> R e. SRing )
195 67 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> G e. Mnd )
196 8 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> A e. S )
197 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( ( N + 1 ) - k ) e. NN0 /\ A e. S ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
198 195 133 196 197 syl3anc 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
199 9 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> B e. S )
200 77 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ k e. NN0 /\ B e. S ) -> ( k .^ B ) e. S )
201 195 136 199 200 syl3anc 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( k .^ B ) e. S )
202 1 3 2 srgmulgass 
 |-  ( ( 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 ) ) ) )
203 194 131 198 201 202 syl13anc 
 |-  ( ( 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 ) ) ) )
204 203 mpteq2dva 
 |-  ( 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 ) ) ) ) )
205 204 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( ( N _C ( k - 1 ) ) .x. ( ( ( N + 1 ) - k ) .^ A ) ) .X. ( k .^ B ) ) ) ) = ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
206 11 156 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
207 simpl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ph )
208 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
209 208 128 syl 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
210 11 209 130 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
211 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
212 211 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
213 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
214 213 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
215 207 210 212 214 137 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
216 1 4 33 206 215 gsummptfzsplitl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
217 snfi 
 |-  { 0 } e. Fin
218 217 a1i 
 |-  ( ph -> { 0 } e. Fin )
219 167 eleq1d 
 |-  ( 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 ) )
220 219 ralsng 
 |-  ( 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 ) )
221 143 220 ax-mp 
 |-  ( 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 )
222 160 221 sylibr 
 |-  ( ph -> A. k e. { 0 } ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
223 1 33 218 222 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S )
224 1 4 cmncom 
 |-  ( ( R e. CMnd /\ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S /\ ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S ) -> ( ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
225 33 140 223 224 syl3anc 
 |-  ( ph -> ( ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) = ( ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
226 216 225 eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) = ( ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .+ ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) ) )
227 193 205 226 3eqtr4d 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( ( N _C ( k - 1 ) ) .x. ( ( ( N + 1 ) - k ) .^ A ) ) .X. ( k .^ B ) ) ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
228 124 227 syl5eq 
 |-  ( ph -> ( R gsum ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) |-> ( ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) .X. ( j .^ B ) ) ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
229 49 113 228 3eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) .X. B ) ) ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
230 31 229 eqtr3d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) .X. B ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
231 13 230 sylan9eqr 
 |-  ( ( ph /\ ps ) -> ( ( N .^ ( A .+ B ) ) .X. B ) = ( R gsum ( k e. ( 0 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )