This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 1 mgpbas 
 |-  S = ( Base ` G )
67 5 srgmgp 
 |-  ( R e. SRing -> G e. Mnd )
68 7 67 syl 
 |-  ( ph -> G e. Mnd )
69 68 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> G e. Mnd )
70 0p1e1 
 |-  ( 0 + 1 ) = 1
71 70 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) )
72 71 eleq2i 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) <-> j e. ( 1 ... ( N + 1 ) ) )
73 fznn0sub 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 )
74 73 a1i 
 |-  ( ph -> ( j e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 ) )
75 72 74 biimtrid 
 |-  ( ph -> ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( ( N + 1 ) - j ) e. NN0 ) )
76 75 imp 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N + 1 ) - j ) e. NN0 )
77 8 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> A e. S )
78 66 6 69 76 77 mulgnn0cld 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - j ) .^ A ) e. S )
79 elfznn 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. NN )
80 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
81 79 80 syl 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( j - 1 ) e. NN0 )
82 72 81 sylbi 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( j - 1 ) e. NN0 )
83 82 adantl 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( j - 1 ) e. NN0 )
84 9 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> B e. S )
85 66 6 69 83 84 mulgnn0cld 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( j - 1 ) .^ B ) e. S )
86 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 ) ) ) )
87 61 65 78 85 86 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 ) ) ) )
88 87 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 ) ) )
89 88 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 ) )
90 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
91 7 90 syl 
 |-  ( ph -> R e. Mnd )
92 91 adantr 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> R e. Mnd )
93 1 3 92 65 78 mulgnn0cld 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) e. S )
94 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 ) ) )
95 61 93 85 84 94 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 ) ) )
96 5 2 mgpplusg 
 |-  .X. = ( +g ` G )
97 66 6 96 mulgnn0p1 
 |-  ( ( G e. Mnd /\ ( j - 1 ) e. NN0 /\ B e. S ) -> ( ( ( j - 1 ) + 1 ) .^ B ) = ( ( ( j - 1 ) .^ B ) .X. B ) )
98 97 eqcomd 
 |-  ( ( G e. Mnd /\ ( j - 1 ) e. NN0 /\ B e. S ) -> ( ( ( j - 1 ) .^ B ) .X. B ) = ( ( ( j - 1 ) + 1 ) .^ B ) )
99 69 83 84 98 syl3anc 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( j - 1 ) .^ B ) .X. B ) = ( ( ( j - 1 ) + 1 ) .^ B ) )
100 99 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 ) ) )
101 52 zcnd 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> j e. CC )
102 1cnd 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> 1 e. CC )
103 101 102 npcand 
 |-  ( j e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
104 103 adantl 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( j - 1 ) + 1 ) = j )
105 104 oveq1d 
 |-  ( ( ph /\ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( j - 1 ) + 1 ) .^ B ) = ( j .^ B ) )
106 105 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 ) ) )
107 95 100 106 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 ) ) )
108 60 89 107 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 ) ) )
109 108 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 ) ) ) )
110 109 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 ) ) ) ) )
111 71 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 ) ) )
112 oveq1 
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
113 112 oveq2d 
 |-  ( j = k -> ( N _C ( j - 1 ) ) = ( N _C ( k - 1 ) ) )
114 oveq2 
 |-  ( j = k -> ( ( N + 1 ) - j ) = ( ( N + 1 ) - k ) )
115 114 oveq1d 
 |-  ( j = k -> ( ( ( N + 1 ) - j ) .^ A ) = ( ( ( N + 1 ) - k ) .^ A ) )
116 113 115 oveq12d 
 |-  ( j = k -> ( ( N _C ( j - 1 ) ) .x. ( ( ( N + 1 ) - j ) .^ A ) ) = ( ( N _C ( k - 1 ) ) .x. ( ( ( N + 1 ) - k ) .^ A ) ) )
117 oveq1 
 |-  ( j = k -> ( j .^ B ) = ( k .^ B ) )
118 116 117 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 ) ) )
119 118 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 ) ) )
120 111 119 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 ) ) )
121 120 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 ) ) ) )
122 fzfid 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) e. Fin )
123 simpl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ph )
124 elfzelz 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. ZZ )
125 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
126 124 125 syl 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
127 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
128 11 126 127 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
129 fznn0sub 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
130 129 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
131 elfznn 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN )
132 131 nnnn0d 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN0 )
133 132 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. NN0 )
134 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 )
135 123 128 130 133 134 syl13anc 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
136 135 ralrimiva 
 |-  ( ph -> A. k e. ( 1 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
137 1 33 122 136 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... ( N + 1 ) ) |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S )
138 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 ) ) ) ) ) )
139 91 137 138 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 ) ) ) ) ) )
140 0nn0 
 |-  0 e. NN0
141 140 a1i 
 |-  ( ph -> 0 e. NN0 )
142 id 
 |-  ( ph -> ph )
143 0z 
 |-  0 e. ZZ
144 143 34 pm3.2i 
 |-  ( 0 e. ZZ /\ 1 e. ZZ )
145 zsubcl 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( 0 - 1 ) e. ZZ )
146 144 145 mp1i 
 |-  ( ph -> ( 0 - 1 ) e. ZZ )
147 bccl 
 |-  ( ( N e. NN0 /\ ( 0 - 1 ) e. ZZ ) -> ( N _C ( 0 - 1 ) ) e. NN0 )
148 11 146 147 syl2anc 
 |-  ( ph -> ( N _C ( 0 - 1 ) ) e. NN0 )
149 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
150 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
151 149 150 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
152 151 subid1d 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 0 ) = ( N + 1 ) )
153 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
154 152 153 eqeltrd 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 0 ) e. NN0 )
155 11 154 syl 
 |-  ( ph -> ( ( N + 1 ) - 0 ) e. NN0 )
156 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 )
157 142 148 155 141 156 syl13anc 
 |-  ( ph -> ( ( N _C ( 0 - 1 ) ) .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) e. S )
158 oveq1 
 |-  ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
159 158 oveq2d 
 |-  ( k = 0 -> ( N _C ( k - 1 ) ) = ( N _C ( 0 - 1 ) ) )
160 oveq2 
 |-  ( k = 0 -> ( ( N + 1 ) - k ) = ( ( N + 1 ) - 0 ) )
161 160 oveq1d 
 |-  ( k = 0 -> ( ( ( N + 1 ) - k ) .^ A ) = ( ( ( N + 1 ) - 0 ) .^ A ) )
162 oveq1 
 |-  ( k = 0 -> ( k .^ B ) = ( 0 .^ B ) )
163 161 162 oveq12d 
 |-  ( k = 0 -> ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) = ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) )
164 159 163 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 ) ) ) )
165 1 164 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 ) ) ) )
166 91 141 157 165 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 ) ) ) )
167 0lt1 
 |-  0 < 1
168 167 a1i 
 |-  ( ph -> 0 < 1 )
169 168 70 breqtrrdi 
 |-  ( ph -> 0 < ( 0 + 1 ) )
170 0re 
 |-  0 e. RR
171 1re 
 |-  1 e. RR
172 170 171 170 3pm3.2i 
 |-  ( 0 e. RR /\ 1 e. RR /\ 0 e. RR )
173 ltsubadd 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 0 e. RR ) -> ( ( 0 - 1 ) < 0 <-> 0 < ( 0 + 1 ) ) )
174 172 173 mp1i 
 |-  ( ph -> ( ( 0 - 1 ) < 0 <-> 0 < ( 0 + 1 ) ) )
175 169 174 mpbird 
 |-  ( ph -> ( 0 - 1 ) < 0 )
176 175 orcd 
 |-  ( ph -> ( ( 0 - 1 ) < 0 \/ N < ( 0 - 1 ) ) )
177 bcval4 
 |-  ( ( N e. NN0 /\ ( 0 - 1 ) e. ZZ /\ ( ( 0 - 1 ) < 0 \/ N < ( 0 - 1 ) ) ) -> ( N _C ( 0 - 1 ) ) = 0 )
178 11 146 176 177 syl3anc 
 |-  ( ph -> ( N _C ( 0 - 1 ) ) = 0 )
179 178 oveq1d 
 |-  ( ph -> ( ( N _C ( 0 - 1 ) ) .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) )
180 66 6 68 155 8 mulgnn0cld 
 |-  ( ph -> ( ( ( N + 1 ) - 0 ) .^ A ) e. S )
181 66 6 68 141 9 mulgnn0cld 
 |-  ( ph -> ( 0 .^ B ) e. S )
182 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 )
183 7 180 181 182 syl3anc 
 |-  ( ph -> ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) e. S )
184 1 14 3 mulg0 
 |-  ( ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) e. S -> ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0g ` R ) )
185 183 184 syl 
 |-  ( ph -> ( 0 .x. ( ( ( ( N + 1 ) - 0 ) .^ A ) .X. ( 0 .^ B ) ) ) = ( 0g ` R ) )
186 166 179 185 3eqtrrd 
 |-  ( ph -> ( 0g ` R ) = ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
187 186 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 ) ) ) ) ) ) )
188 139 187 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 ) ) ) ) ) ) )
189 7 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> R e. SRing )
190 68 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> G e. Mnd )
191 8 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> A e. S )
192 66 6 190 130 191 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) - k ) .^ A ) e. S )
193 9 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> B e. S )
194 66 6 190 133 193 mulgnn0cld 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( k .^ B ) e. S )
195 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 ) ) ) )
196 189 128 192 194 195 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 ) ) ) )
197 196 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 ) ) ) ) )
198 197 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 ) ) ) ) ) )
199 11 153 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
200 simpl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ph )
201 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
202 201 125 syl 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
203 11 202 127 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
204 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
205 204 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. NN0 )
206 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
207 206 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
208 200 203 205 207 134 syl13anc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
209 1 4 33 199 208 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 ) ) ) ) ) ) )
210 snfi 
 |-  { 0 } e. Fin
211 210 a1i 
 |-  ( ph -> { 0 } e. Fin )
212 164 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 ) )
213 212 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 ) )
214 140 213 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 )
215 157 214 sylibr 
 |-  ( ph -> A. k e. { 0 } ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) e. S )
216 1 33 211 215 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. { 0 } |-> ( ( N _C ( k - 1 ) ) .x. ( ( ( ( N + 1 ) - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) e. S )
217 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 ) ) ) ) ) ) )
218 33 137 216 217 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 ) ) ) ) ) ) )
219 209 218 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 ) ) ) ) ) ) )
220 188 198 219 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 ) ) ) ) ) )
221 121 220 eqtrid 
 |-  ( 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 ) ) ) ) ) )
222 49 110 221 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 ) ) ) ) ) )
223 31 222 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 ) ) ) ) ) )
224 13 223 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 ) ) ) ) ) )