Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  binomcxplemnotnn0 Structured version   Unicode version

Theorem binomcxplemnotnn0 36122
Description: Lemma for binomcxp 36123. When  C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36115 —which we will call  P —is a convergent power series: its base  b is always of smaller absolute value than the radius of convergence.

pserdv2 23119 gives the derivative of  P, which by dvradcnv 23110 also converges in that radius. When  A is fixed at one,  ( A  +  b ) times that derivative equals  ( C  x.  P
) and fraction  ( P  / 
( ( A  +  b )  ^c  C ) ) is always defined with derivative zero, so the fraction is a constant—specifically one, because  ( ( 1  +  0 )  ^c  C )  =  1. Thus  ( ( 1  +  b )  ^c  C )  =  ( P `  b ).

Finally, let  b be  ( B  /  A ), and multiply both the binomial  ( ( 1  +  ( B  /  A ) )  ^c  C ) and the sum  ( P `  ( B  /  A
) ) by  ( A  ^c  C ) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.)

Hypotheses
Ref Expression
binomcxp.a  |-  ( ph  ->  A  e.  RR+ )
binomcxp.b  |-  ( ph  ->  B  e.  RR )
binomcxp.lt  |-  ( ph  ->  ( abs `  B
)  <  ( abs `  A ) )
binomcxp.c  |-  ( ph  ->  C  e.  CC )
binomcxplem.f  |-  F  =  ( j  e.  NN0  |->  ( CC𝑐 j ) )
binomcxplem.s  |-  S  =  ( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
binomcxplem.r  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
binomcxplem.e  |-  E  =  ( b  e.  CC  |->  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
binomcxplem.d  |-  D  =  ( `' abs " (
0 [,) R ) )
binomcxplem.p  |-  P  =  ( b  e.  D  |-> 
sum_ k  e.  NN0  ( ( S `  b ) `  k
) )
Assertion
Ref Expression
binomcxplemnotnn0  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( A  +  B
)  ^c  C )  =  sum_ k  e.  NN0  ( ( CC𝑐 k )  x.  ( ( A  ^c  ( C  -  k ) )  x.  ( B ^ k ) ) ) )
Distinct variable groups:    k, b,
r, A    B, b,
k, r    j, b, ph, k    C, b, j, k    F, b, k, r    S, k, r    D, j, k    j, E, k
Allowed substitution hints:    ph( r)    A( j)    B( j)    C( r)    D( r, b)    P( j, k, r, b)    R( j, k, r, b)    S( j, b)    E( r, b)    F( j)

Proof of Theorem binomcxplemnotnn0
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 binomcxplem.p . . . . . . 7  |-  P  =  ( b  e.  D  |-> 
sum_ k  e.  NN0  ( ( S `  b ) `  k
) )
2 binomcxplem.d . . . . . . . . 9  |-  D  =  ( `' abs " (
0 [,) R ) )
3 nfcv 2566 . . . . . . . . . 10  |-  F/_ b `' abs
4 nfcv 2566 . . . . . . . . . . 11  |-  F/_ b
0
5 nfcv 2566 . . . . . . . . . . 11  |-  F/_ b [,)
6 binomcxplem.r . . . . . . . . . . . 12  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
7 nfcv 2566 . . . . . . . . . . . . . . . 16  |-  F/_ b  +
8 binomcxplem.s . . . . . . . . . . . . . . . . . 18  |-  S  =  ( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
9 nfmpt1 4486 . . . . . . . . . . . . . . . . . 18  |-  F/_ b
( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
108, 9nfcxfr 2564 . . . . . . . . . . . . . . . . 17  |-  F/_ b S
11 nfcv 2566 . . . . . . . . . . . . . . . . 17  |-  F/_ b
r
1210, 11nffv 5858 . . . . . . . . . . . . . . . 16  |-  F/_ b
( S `  r
)
134, 7, 12nfseq 12163 . . . . . . . . . . . . . . 15  |-  F/_ b  seq 0 (  +  , 
( S `  r
) )
1413nfel1 2582 . . . . . . . . . . . . . 14  |-  F/ b  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>
15 nfcv 2566 . . . . . . . . . . . . . 14  |-  F/_ b RR
1614, 15nfrab 2991 . . . . . . . . . . . . 13  |-  F/_ b { r  e.  RR  |  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>  }
17 nfcv 2566 . . . . . . . . . . . . 13  |-  F/_ b RR*
18 nfcv 2566 . . . . . . . . . . . . 13  |-  F/_ b  <
1916, 17, 18nfsup 7946 . . . . . . . . . . . 12  |-  F/_ b sup ( { r  e.  RR  |  seq 0
(  +  ,  ( S `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )
206, 19nfcxfr 2564 . . . . . . . . . . 11  |-  F/_ b R
214, 5, 20nfov 6306 . . . . . . . . . 10  |-  F/_ b
( 0 [,) R
)
223, 21nfima 5167 . . . . . . . . 9  |-  F/_ b
( `' abs " (
0 [,) R ) )
232, 22nfcxfr 2564 . . . . . . . 8  |-  F/_ b D
24 nfcv 2566 . . . . . . . 8  |-  F/_ x D
25 nfcv 2566 . . . . . . . 8  |-  F/_ x sum_ k  e.  NN0  (
( S `  b
) `  k )
26 nfcv 2566 . . . . . . . . 9  |-  F/_ b NN0
27 nfcv 2566 . . . . . . . . . . 11  |-  F/_ b
x
2810, 27nffv 5858 . . . . . . . . . 10  |-  F/_ b
( S `  x
)
29 nfcv 2566 . . . . . . . . . 10  |-  F/_ b
k
3028, 29nffv 5858 . . . . . . . . 9  |-  F/_ b
( ( S `  x ) `  k
)
3126, 30nfsum 13664 . . . . . . . 8  |-  F/_ b sum_ k  e.  NN0  (
( S `  x
) `  k )
32 simpl 457 . . . . . . . . . . 11  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
b  =  x )
3332fveq2d 5855 . . . . . . . . . 10  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
( S `  b
)  =  ( S `
 x ) )
3433fveq1d 5853 . . . . . . . . 9  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
( ( S `  b ) `  k
)  =  ( ( S `  x ) `
 k ) )
3534sumeq2dv 13676 . . . . . . . 8  |-  ( b  =  x  ->  sum_ k  e.  NN0  ( ( S `
 b ) `  k )  =  sum_ k  e.  NN0  ( ( S `  x ) `
 k ) )
3623, 24, 25, 31, 35cbvmptf 4487 . . . . . . 7  |-  ( b  e.  D  |->  sum_ k  e.  NN0  ( ( S `
 b ) `  k ) )  =  ( x  e.  D  |-> 
sum_ k  e.  NN0  ( ( S `  x ) `  k
) )
371, 36eqtri 2433 . . . . . 6  |-  P  =  ( x  e.  D  |-> 
sum_ k  e.  NN0  ( ( S `  x ) `  k
) )
3837a1i 11 . . . . 5  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  P  =  ( x  e.  D  |->  sum_ k  e.  NN0  ( ( S `  x ) `  k
) ) )
39 simplr 756 . . . . . . . 8  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  x  =  ( B  /  A ) )
4039fveq2d 5855 . . . . . . 7  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  ( S `  x )  =  ( S `  ( B  /  A
) ) )
4140fveq1d 5853 . . . . . 6  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  (
( S `  x
) `  k )  =  ( ( S `
 ( B  /  A ) ) `  k ) )
4241sumeq2dv 13676 . . . . 5  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  ->  sum_ k  e.  NN0  (
( S `  x
) `  k )  =  sum_ k  e.  NN0  ( ( S `  ( B  /  A
) ) `  k
) )
43 binomcxp.b . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
4443recnd 9654 . . . . . . . 8  |-  ( ph  ->  B  e.  CC )
4544adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  B  e.  CC )
46 binomcxp.a . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
4746rpcnd 11308 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
4847adantr 465 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  A  e.  CC )
49 0red 9629 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  e.  RR )
5045abscld 13418 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  e.  RR )
5148abscld 13418 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  RR )
5245absge0d 13426 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <_  ( abs `  B
) )
53 binomcxp.lt . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  B
)  <  ( abs `  A ) )
5453adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  < 
( abs `  A
) )
5549, 50, 51, 52, 54lelttrd 9776 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <  ( abs `  A
) )
5655gt0ne0d 10159 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  =/=  0 )
5748abs00ad 13274 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  =  0  <->  A  =  0 ) )
5857necon3bid 2663 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  =/=  0  <->  A  =/=  0 ) )
5956, 58mpbid 212 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  A  =/=  0 )
6045, 48, 59divcld 10363 . . . . . 6  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( B  /  A )  e.  CC )
6160abscld 13418 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  e.  RR )
6260absge0d 13426 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <_  ( abs `  ( B  /  A ) ) )
6351recnd 9654 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  CC )
6463mulid1d 9645 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  x.  1 )  =  ( abs `  A
) )
6554, 64breqtrrd 4423 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  < 
( ( abs `  A
)  x.  1 ) )
66 1red 9643 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  1  e.  RR )
6751, 55elrpd 11303 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  RR+ )
6850, 66, 67ltdivmuld 11353 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( ( abs `  B
)  /  ( abs `  A ) )  <  1  <->  ( abs `  B
)  <  ( ( abs `  A )  x.  1 ) ) )
6965, 68mpbird 234 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  B
)  /  ( abs `  A ) )  <  1 )
7045, 48, 59absdivd 13437 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  =  ( ( abs `  B
)  /  ( abs `  A ) ) )
71 binomcxp.c . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
72 binomcxplem.f . . . . . . . . 9  |-  F  =  ( j  e.  NN0  |->  ( CC𝑐 j ) )
7346, 43, 53, 71, 72, 8, 6binomcxplemradcnv 36118 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  R  =  1 )
7469, 70, 733brtr4d 4427 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  < 
R )
75 0re 9628 . . . . . . . 8  |-  0  e.  RR
76 ssrab2 3526 . . . . . . . . . . 11  |-  { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } 
C_  RR
77 ressxr 9669 . . . . . . . . . . 11  |-  RR  C_  RR*
7876, 77sstri 3453 . . . . . . . . . 10  |-  { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } 
C_  RR*
79 supxrcl 11561 . . . . . . . . . 10  |-  ( { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } 
C_  RR*  ->  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR* )
8078, 79ax-mp 5 . . . . . . . . 9  |-  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR*
816, 80eqeltri 2488 . . . . . . . 8  |-  R  e. 
RR*
82 elico2 11644 . . . . . . . 8  |-  ( ( 0  e.  RR  /\  R  e.  RR* )  -> 
( ( abs `  ( B  /  A ) )  e.  ( 0 [,) R )  <->  ( ( abs `  ( B  /  A ) )  e.  RR  /\  0  <_ 
( abs `  ( B  /  A ) )  /\  ( abs `  ( B  /  A ) )  <  R ) ) )
8375, 81, 82mp2an 672 . . . . . . 7  |-  ( ( abs `  ( B  /  A ) )  e.  ( 0 [,) R )  <->  ( ( abs `  ( B  /  A ) )  e.  RR  /\  0  <_ 
( abs `  ( B  /  A ) )  /\  ( abs `  ( B  /  A ) )  <  R ) )
8461, 62, 74, 83syl3anbrc 1183 . . . . . 6  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  e.  ( 0 [,) R
) )
852eleq2i 2482 . . . . . . 7  |-  ( ( B  /  A )  e.  D  <->  ( B  /  A )  e.  ( `' abs " ( 0 [,) R ) ) )
86 absf 13321 . . . . . . . 8  |-  abs : CC
--> RR
87 ffn 5716 . . . . . . . 8  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
88 elpreima 5987 . . . . . . . 8  |-  ( abs 
Fn  CC  ->  ( ( B  /  A )  e.  ( `' abs " ( 0 [,) R
) )  <->  ( ( B  /  A )  e.  CC  /\  ( abs `  ( B  /  A
) )  e.  ( 0 [,) R ) ) ) )
8986, 87, 88mp2b 10 . . . . . . 7  |-  ( ( B  /  A )  e.  ( `' abs " ( 0 [,) R
) )  <->  ( ( B  /  A )  e.  CC  /\  ( abs `  ( B  /  A
) )  e.  ( 0 [,) R ) ) )
9085, 89bitri 251 . . . . . 6  |-  ( ( B  /  A )  e.  D  <->  ( ( B  /  A )  e.  CC  /\  ( abs `  ( B  /  A
) )  e.  ( 0 [,) R ) ) )
9160, 84, 90sylanbrc 664 . . . . 5  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( B  /  A )  e.  D )
92 sumex 13661 . . . . . 6  |-  sum_ k  e.  NN0  ( ( S `
 ( B  /  A ) ) `  k )  e.  _V
9392a1i 11 . . . . 5  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  sum_ k  e.  NN0  ( ( S `
 ( B  /  A ) ) `  k )  e.  _V )
9438, 42, 91, 93fvmptd 5940 . . . 4  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( P `  ( B  /  A ) )  = 
sum_ k  e.  NN0  ( ( S `  ( B  /  A
) ) `  k
) )
95 eqid 2404 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
9695cnbl0 21575 . . . . . . . . . . . 12  |-  ( R  e.  RR*  ->  ( `' abs " ( 0 [,) R ) )  =  ( 0 (
ball `  ( abs  o. 
-  ) ) R ) )
9781, 96ax-mp 5 . . . . . . . . . . 11  |-  ( `' abs " ( 0 [,) R ) )  =  ( 0 (
ball `  ( abs  o. 
-  ) ) R )
982, 97eqtri 2433 . . . . . . . . . 10  |-  D  =  ( 0 ( ball `  ( abs  o.  -  ) ) R )
99 0cnd 9621 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  e.  CC )
10081a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  R  e.  RR* )
101 mulcl 9608 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
102101adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  ( x  e.  CC  /\  y  e.  CC ) )  ->  ( x  x.  y )  e.  CC )
103 nfv 1730 . . . . . . . . . . . . . . 15  |-  F/ b ( ph  /\  -.  C  e.  NN0 )
10423nfcri 2559 . . . . . . . . . . . . . . 15  |-  F/ b  x  e.  D
105103, 104nfan 1958 . . . . . . . . . . . . . 14  |-  F/ b ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D
)
10631nfel1 2582 . . . . . . . . . . . . . 14  |-  F/ b
sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC
107105, 106nfim 1950 . . . . . . . . . . . . 13  |-  F/ b ( ( ( ph  /\ 
-.  C  e.  NN0 )  /\  x  e.  D
)  ->  sum_ k  e. 
NN0  ( ( S `
 x ) `  k )  e.  CC )
108 eleq1 2476 . . . . . . . . . . . . . . 15  |-  ( b  =  x  ->  (
b  e.  D  <->  x  e.  D ) )
109108anbi2d 704 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  <->  ( ( ph  /\ 
-.  C  e.  NN0 )  /\  x  e.  D
) ) )
11035eleq1d 2473 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  ( sum_ k  e.  NN0  (
( S `  b
) `  k )  e.  CC  <->  sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC ) )
111109, 110imbi12d 320 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
( ( ( ph  /\ 
-.  C  e.  NN0 )  /\  b  e.  D
)  ->  sum_ k  e. 
NN0  ( ( S `
 b ) `  k )  e.  CC ) 
<->  ( ( ( ph  /\ 
-.  C  e.  NN0 )  /\  x  e.  D
)  ->  sum_ k  e. 
NN0  ( ( S `
 x ) `  k )  e.  CC ) ) )
112 nn0uz 11163 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
113 0zd 10919 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  0  e.  ZZ )
114 eqidd 2405 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( S `  b ) `  k )  =  ( ( S `  b
) `  k )
)
115 cnvimass 5179 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' abs " ( 0 [,) R ) ) 
C_  dom  abs
1162, 115eqsstri 3474 . . . . . . . . . . . . . . . . . . 19  |-  D  C_  dom  abs
11786fdmi 5721 . . . . . . . . . . . . . . . . . . 19  |-  dom  abs  =  CC
118116, 117sseqtri 3476 . . . . . . . . . . . . . . . . . 18  |-  D  C_  CC
119118sseli 3440 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  D  ->  b  e.  CC )
1208a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S  =  ( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  ( b ^
k ) ) ) ) )
121 nn0ex 10844 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  e.  _V
122121mptex 6126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN0  |->  ( ( F `  k )  x.  ( b ^
k ) ) )  e.  _V
123122a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  b  e.  CC )  ->  ( k  e.  NN0  |->  ( ( F `  k )  x.  ( b ^
k ) ) )  e.  _V )
124120, 123fvmpt2d 5945 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  b  e.  CC )  ->  ( S `
 b )  =  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
125 ovex 6308 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  k )  x.  ( b ^
k ) )  e. 
_V
126125a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( F `  k
)  x.  ( b ^ k ) )  e.  _V )
127124, 126fvmpt2d 5945 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  =  ( ( F `
 k )  x.  ( b ^ k
) ) )
12872a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN0 )  ->  F  =  ( j  e.  NN0  |->  ( CC𝑐 j ) ) )
129 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
j  =  k )
130129oveq2d 6296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( CC𝑐 j )  =  ( CC𝑐 k ) )
131 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  NN0 )
132 ovex 6308 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( CC𝑐 k )  e.  _V
133132a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( CC𝑐 k
)  e.  _V )
134128, 130, 131, 133fvmptd 5940 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  =  ( CC𝑐 k ) )
135134oveq1d 6295 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( F `  k )  x.  ( b ^ k
) )  =  ( ( CC𝑐 k )  x.  (
b ^ k ) ) )
136135adantlr 715 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( F `  k
)  x.  ( b ^ k ) )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
137127, 136eqtrd 2445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
138119, 137sylanl2 651 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
13971ad2antrr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  C  e.  CC )
140 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
141139, 140bcccl 36105 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  ( CC𝑐 k )  e.  CC )
142119ad2antlr 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  b  e.  CC )
143142, 140expcld 12356 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
b ^ k )  e.  CC )
144141, 143mulcld 9648 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( CC𝑐 k )  x.  (
b ^ k ) )  e.  CC )
145138, 144eqeltrd 2492 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  e.  CC )
146145adantllr 719 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( S `  b ) `  k )  e.  CC )
147 eleq1 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (
x  e.  D  <->  b  e.  D ) )
148147anbi2d 704 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  b  ->  (
( ph  /\  x  e.  D )  <->  ( ph  /\  b  e.  D ) ) )
149 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  b  ->  ( S `  x )  =  ( S `  b ) )
150149seqeq3d 12161 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  b  ->  seq 0 (  +  , 
( S `  x
) )  =  seq 0 (  +  , 
( S `  b
) ) )
151150eleq1d 2473 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (  seq 0 (  +  , 
( S `  x
) )  e.  dom  ~~>  <->  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  ) )
152 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  b  ->  ( E `  x )  =  ( E `  b ) )
153152seqeq3d 12161 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  b  ->  seq 1 (  +  , 
( E `  x
) )  =  seq 1 (  +  , 
( E `  b
) ) )
154153eleq1d 2473 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (  seq 1 (  +  , 
( E `  x
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  ) )
155151, 154anbi12d 711 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  b  ->  (
(  seq 0 (  +  ,  ( S `  x ) )  e. 
dom 
~~>  /\  seq 1 (  +  ,  ( E `
 x ) )  e.  dom  ~~>  )  <->  (  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  /\ 
seq 1 (  +  ,  ( E `  b ) )  e. 
dom 
~~>  ) ) )
156148, 155imbi12d 320 . . . . . . . . . . . . . . . . 17  |-  ( x  =  b  ->  (
( ( ph  /\  x  e.  D )  ->  (  seq 0 (  +  ,  ( S `
 x ) )  e.  dom  ~~>  /\  seq 1 (  +  , 
( E `  x
) )  e.  dom  ~~>  ) )  <->  ( ( ph  /\  b  e.  D )  ->  (  seq 0
(  +  ,  ( S `  b ) )  e.  dom  ~~>  /\  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  ) ) ) )
157 binomcxplem.e . . . . . . . . . . . . . . . . . 18  |-  E  =  ( b  e.  CC  |->  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
15846, 43, 53, 71, 72, 8, 6, 157, 2binomcxplemcvg 36120 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  D )  ->  (  seq 0 (  +  , 
( S `  x
) )  e.  dom  ~~>  /\ 
seq 1 (  +  ,  ( E `  x ) )  e. 
dom 
~~>  ) )
159156, 158chvarv 2043 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  D )  ->  (  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  /\ 
seq 1 (  +  ,  ( E `  b ) )  e. 
dom 
~~>  ) )
160159simpld 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  D )  ->  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  )
161160adantlr 715 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 0 (  +  ,  ( S `  b ) )  e. 
dom 
~~>  )
162112, 113, 114, 146, 161isumcl 13729 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN0  ( ( S `  b ) `  k
)  e.  CC )
163107, 111, 162chvar 2042 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  -> 
sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC )
164163, 37fmptd 6035 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  P : D --> CC )
165 1cnd 9644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  1  e.  CC )
166118sseli 3440 . . . . . . . . . . . . . . 15  |-  ( x  e.  D  ->  x  e.  CC )
167166adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  x  e.  CC )
168165, 167addcld 9647 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( 1  +  x
)  e.  CC )
16971ad2antrr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  C  e.  CC )
170169negcld 9956 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  -> 
-u C  e.  CC )
171168, 170cxpcld 23385 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( ( 1  +  x )  ^c  -u C )  e.  CC )
172 nfcv 2566 . . . . . . . . . . . . 13  |-  F/_ x
( ( 1  +  b )  ^c  -u C )
173 nfcv 2566 . . . . . . . . . . . . 13  |-  F/_ b
( ( 1  +  x )  ^c  -u C )
174 oveq2 6288 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
1  +  b )  =  ( 1  +  x ) )
175174oveq1d 6295 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
( 1  +  b )  ^c  -u C )  =  ( ( 1  +  x
)  ^c  -u C ) )
17623, 24, 172, 173, 175cbvmptf 4487 . . . . . . . . . . . 12  |-  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C
) )  =  ( x  e.  D  |->  ( ( 1  +  x
)  ^c  -u C ) )
177171, 176fmptd 6035 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) : D --> CC )
178 cnex 9605 . . . . . . . . . . . . . . . 16  |-  CC  e.  _V
179 fex 6128 . . . . . . . . . . . . . . . 16  |-  ( ( abs : CC --> RR  /\  CC  e.  _V )  ->  abs  e.  _V )
18086, 178, 179mp2an 672 . . . . . . . . . . . . . . 15  |-  abs  e.  _V
181180cnvex 6733 . . . . . . . . . . . . . 14  |-  `' abs  e.  _V
182 imaexg 6723 . . . . . . . . . . . . . 14  |-  ( `' abs  e.  _V  ->  ( `' abs " ( 0 [,) R ) )  e.  _V )
183181, 182ax-mp 5 . . . . . . . . . . . . 13  |-  ( `' abs " ( 0 [,) R ) )  e.  _V
1842, 183eqeltri 2488 . . . . . . . . . . . 12  |-  D  e. 
_V
185184a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  D  e.  _V )
186 inidm 3650 . . . . . . . . . . 11  |-  ( D  i^i  D )  =  D
187102, 164, 177, 185, 185, 186off 6538 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( P  oF  x.  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) ) : D --> CC )
188 1ex 9623 . . . . . . . . . . . . . 14  |-  1  e.  _V
189188fconst 5756 . . . . . . . . . . . . 13  |-  ( D  X.  { 1 } ) : D --> { 1 }
190 fconstmpt 4869 . . . . . . . . . . . . . . 15  |-  ( D  X.  { 1 } )  =  ( x  e.  D  |->  1 )
191 nfcv 2566 . . . . . . . . . . . . . . . 16  |-  F/_ b
1
192 nfcv 2566 . . . . . . . . . . . . . . . 16  |-  F/_ x
1
193 eqidd 2405 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  1  =  1 )
19424, 23, 191, 192, 193cbvmptf 4487 . . . . . . . . . . . . . . 15  |-  ( x  e.  D  |->  1 )  =  ( b  e.  D  |->  1 )
195190, 194eqtri 2433 . . . . . . . . . . . . . 14  |-  ( D  X.  { 1 } )  =  ( b  e.  D  |->  1 )
196195feq1i 5708 . . . . . . . . . . . . 13  |-  ( ( D  X.  { 1 } ) : D --> { 1 }  <->  ( b  e.  D  |->  1 ) : D --> { 1 } )
197189, 196mpbi 210 . . . . . . . . . . . 12  |-  ( b  e.  D  |->  1 ) : D --> { 1 }
198 ax-1cn 9582 . . . . . . . . . . . . 13  |-  1  e.  CC
199 snssi 4118 . . . . . . . . . . . . 13  |-  ( 1  e.  CC  ->  { 1 }  C_  CC )
200198, 199ax-mp 5 . . . . . . . . . . . 12  |-  { 1 }  C_  CC
201 fss 5724 . . . . . . . . . . . 12  |-  ( ( ( b  e.  D  |->  1 ) : D --> { 1 }  /\  { 1 }  C_  CC )  ->  ( b  e.  D  |->  1 ) : D --> CC )
202197, 200, 201mp2an 672 . . . . . . . . . . 11  |-  ( b  e.  D  |->  1 ) : D --> CC
203202a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
b  e.  D  |->  1 ) : D --> CC )
204 cnelprrecn 9617 . . . . . . . . . . . . . . . . 17  |-  CC  e.  { RR ,  CC }
205204a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  CC  e.  { RR ,  CC } )
20646, 43, 53, 71, 72, 8, 6, 157, 2, 1binomcxplemdvsum 36121 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( CC  _D  P
)  =  ( b  e.  D  |->  sum_ k  e.  NN  ( ( E `
 b ) `  k ) ) )
207206adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P )  =  ( b  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  b ) `  k
) ) )
208 nfcv 2566 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x sum_ k  e.  NN  (
( E `  b
) `  k )
209 nfcv 2566 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ b NN
210 nfmpt1 4486 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ b
( b  e.  CC  |->  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
211157, 210nfcxfr 2564 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ b E
212211, 27nffv 5858 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ b
( E `  x
)
213212, 29nffv 5858 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ b
( ( E `  x ) `  k
)
214209, 213nfsum 13664 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ b sum_ k  e.  NN  (
( E `  x
) `  k )
215 simpl 457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  =  x  /\  k  e.  NN )  ->  b  =  x )
216215fveq2d 5855 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  =  x  /\  k  e.  NN )  ->  ( E `  b
)  =  ( E `
 x ) )
217216fveq1d 5853 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b  =  x  /\  k  e.  NN )  ->  ( ( E `  b ) `  k
)  =  ( ( E `  x ) `
 k ) )
218217sumeq2dv 13676 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  x  ->  sum_ k  e.  NN  ( ( E `
 b ) `  k )  =  sum_ k  e.  NN  (
( E `  x
) `  k )
)
21923, 24, 208, 214, 218cbvmptf 4487 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  D  |->  sum_ k  e.  NN  ( ( E `
 b ) `  k ) )  =  ( x  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  x ) `  k
) )
220207, 219syl6eq 2461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P )  =  ( x  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  x ) `  k
) ) )
221 sumex 13661 . . . . . . . . . . . . . . . . . . 19  |-  sum_ k  e.  NN  ( ( E `
 x ) `  k )  e.  _V
222221a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  -> 
sum_ k  e.  NN  ( ( E `  x ) `  k
)  e.  _V )
223220, 222fmpt3d 6036 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P ) : D --> _V )
224 fdm 5720 . . . . . . . . . . . . . . . . 17  |-  ( ( CC  _D  P ) : D --> _V  ->  dom  ( CC  _D  P
)  =  D )
225223, 224syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  dom  ( CC  _D  P
)  =  D )
22646, 43, 53, 71, 72, 8, 6, 157, 2binomcxplemdvbinom 36119 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  =  ( b  e.  D  |->  ( -u C  x.  ( (
1  +  b )  ^c  ( -u C  -  1 ) ) ) ) )
227 nfcv 2566 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( -u C  x.  (
( 1  +  b )  ^c  (
-u C  -  1 ) ) )
228 nfcv 2566 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ b
( -u C  x.  (
( 1  +  x
)  ^c  (
-u C  -  1 ) ) )
229174oveq1d 6295 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  x  ->  (
( 1  +  b )  ^c  (
-u C  -  1 ) )  =  ( ( 1  +  x
)  ^c  (
-u C  -  1 ) ) )
230229oveq2d 6296 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  x  ->  ( -u C  x.  ( ( 1  +  b )  ^c  ( -u C  -  1 ) ) )  =  (
-u C  x.  (
( 1  +  x
)  ^c  (
-u C  -  1 ) ) ) )
23123, 24, 227, 228, 230cbvmptf 4487 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  D  |->  ( -u C  x.  ( (
1  +  b )  ^c  ( -u C  -  1 ) ) ) )  =  ( x  e.  D  |->  ( -u C  x.  ( ( 1  +  x )  ^c 
( -u C  -  1 ) ) ) )
232226, 231syl6eq 2461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  =  ( x  e.  D  |->  ( -u C  x.  ( (
1  +  x )  ^c  ( -u C  -  1 ) ) ) ) )
233170, 165subcld 9969 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( -u C  - 
1 )  e.  CC )
234168, 233cxpcld 23385 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( ( 1  +  x )  ^c 
( -u C  -  1 ) )  e.  CC )
235170, 234mulcld 9648 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( -u C  x.  ( ( 1  +  x )  ^c 
( -u C  -  1 ) ) )  e.  CC )
236232, 235fmpt3d 6036 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) ) : D --> CC )
237 fdm 5720 . . . . . . . . . . . . . . . . 17  |-  ( ( CC  _D  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C
) ) ) : D --> CC  ->  dom  ( CC  _D  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  =  D )
238236, 237syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  dom  ( CC  _D  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  =  D )
239205, 164, 177, 225, 238dvmulf 22640 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  ( P  oF  x.  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C
) ) ) )  =  ( ( ( CC  _D  P )  oF  x.  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  oF  +  ( ( CC  _D  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) )  oF  x.  P
) ) )
24071ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  C  e.  CC )
241240mulid1d 9645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( C  x.  1 )  =  C )
242241oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( C  x.  1 )  +  ( C  x.  sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^ k ) ) ) )  =  ( C  +  ( C  x.  sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^
k ) ) ) ) )
243 1cnd 9644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  1  e.  CC )
244 nnuz 11164 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  NN  =  ( ZZ>= `  1 )
245 1zzd 10938 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  1  e.  ZZ )
246 nnnn0 10845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  NN  ->  k  e.  NN0 )
247246, 138sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
248247adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( S `  b ) `
 k )  =  ( ( CC𝑐 k )  x.  ( b ^
k ) ) )
24971ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  C  e.  CC )
250 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
251249, 250bcccl 36105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( CC𝑐 k
)  e.  CC )
252246, 251sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( CC𝑐 k )  e.  CC )
253119adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  b  e.  CC )
254253adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  b  e.  CC )
255254, 250expcld 12356 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( b ^ k )  e.  CC )
256246, 255sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ k )  e.  CC )
257252, 256mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( CC𝑐 k )  x.  (
b ^ k ) )  e.  CC )
258 1nn0 10854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  1  e.  NN0
259258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  b  e.  D )  ->  1  e.  NN0 )
260112, 259, 145iserex 13630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  b  e.  D )  ->  (  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( S `  b
) )  e.  dom  ~~>  ) )
261160, 260mpbid 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  b  e.  D )  ->  seq 1 (  +  , 
( S `  b
) )  e.  dom  ~~>  )
262261adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( S `  b ) )  e. 
dom 
~~>  )
263244, 245, 248, 257, 262isumcl 13729 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^
k ) )  e.  CC )
264240, 243, 263adddid 9652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( C  x.  (
1  +  sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^ k ) ) ) )  =  ( ( C  x.  1 )  +  ( C  x.  sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^
k ) ) ) ) )
265157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  E  =  ( b  e.  CC  |->  ( k  e.  NN  |->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) ) ) ) )
266 nnex 10584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  NN  e.  _V
267266mptex 6126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( k  e.  NN  |->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) ) )  e.  _V
268267a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  b  e.  CC )  ->  ( k  e.  NN  |->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) ) )  e.  _V )
269265, 268fvmpt2d 5945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  b  e.  CC )  ->  ( E `
 b )  =  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
270119, 269sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  b  e.  D )  ->  ( E `  b )  =  ( k  e.  NN  |->  ( ( k  x.  ( F `  k ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
271270adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
)  =  ( k  e.  NN  |->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) ) ) )
272 ovex 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) )  e. 
_V
273272a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) )  e. 
_V )
274271, 273fmpt3d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
) : NN --> _V )
275274feqmptd 5904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
)  =  ( k  e.  NN  |->  ( ( E `  b ) `
 k ) ) )
276272a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( k  x.  ( F `  k )
)  x.  ( b ^ ( k  - 
1 ) ) )  e.  _V )
277269, 276fvmpt2d 5945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( k  x.  ( F `  k ) )  x.  ( b ^ (
k  -  1 ) ) ) )
278246, 134sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  =  ( CC𝑐 k ) )
279278oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( F `  k ) )  =  ( k  x.  ( CC𝑐 k ) ) )
280279oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) )  =  ( ( k  x.  ( CC𝑐 k ) )  x.  ( b ^ (
k  -  1 ) ) ) )
281280adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( k  x.  ( F `  k )
)  x.  ( b ^ ( k  - 
1 ) ) )  =  ( ( k  x.  ( CC𝑐 k ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
282277, 281eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( k  x.  ( CC𝑐 k ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
28371adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  C  e.  CC )
284 nnm1nn0 10880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( k  e.  NN  ->  (
k  -  1 )  e.  NN0 )
285284adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  -  1 )  e. 
NN0 )
286283, 285bccp1k 36107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( ( k  -  1 )  +  1 ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  ( ( k  -  1 )  +  1 ) ) ) )
287246adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  k  e.  NN )  ->  k  e. 
NN0 )
288287nn0cnd 10897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
289 1cnd 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  CC )
290288, 289npcand 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  -  1 )  +  1 )  =  k )
291290oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( ( k  -  1 )  +  1 ) )  =  ( CC𝑐 k ) )
292290oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( C  -  ( k  -  1 ) )  /  ( ( k  -  1 )  +  1 ) )  =  ( ( C  -  ( k  -  1 ) )  /  k
) )
293292oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  ( ( k  -  1 )  +  1 ) ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  k ) ) )
294286, 291, 2933eqtr3d 2453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 k )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  k ) ) )
295294oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( CC𝑐 k ) )  =  ( k  x.  ( ( CC𝑐 ( k  -  1 ) )  x.  ( ( C  -  ( k  -  1 ) )  /  k ) ) ) )
296283, 285bcccl 36105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
297288, 289subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  -  1 )  e.  CC )
298283, 297subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( C  -  ( k  - 
1 ) )  e.  CC )
299 nnne0 10611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  NN  ->  k  =/=  0 )
300299adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
301296, 298, 288, 300divassd 10398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  /  k )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  ( ( C  -  ( k  -  1 ) )  /  k ) ) )
302301oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  /  k ) )  =  ( k  x.  ( ( CC𝑐 ( k  -  1 ) )  x.  ( ( C  -  ( k  -  1 ) )  /  k ) ) ) )
303296, 298mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  e.  CC )
304303, 288, 300divcan2d 10365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  /  k ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) ) )
305295, 302, 3043eqtr2d 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( CC𝑐 k ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) ) )
306305oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  x.  ( CC𝑐 k ) )  x.  (
b ^ ( k  -  1 ) ) )  =  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
307306adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( k  x.  ( CC𝑐 k ) )  x.  ( b ^ (
k  -  1 ) ) )  =  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
308296adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
309298adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  ( C  -  ( k  -  1 ) )  e.  CC )
310308, 309mulcomd 9649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  =  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) ) )
311310oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
312282, 307, 3113eqtrd 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
313119, 312sylanl2 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
314313adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( E `  b ) `
 k )  =  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
315314mpteq2dva 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( k  e.  NN  |->  ( ( E `  b ) `  k
) )  =  ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
316275, 315eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
)  =  ( k  e.  NN  |->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
317316oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( E `  b )  shift  -u 1
)  =  ( ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )  shift  -u
1 ) )
318 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  NN  |->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ ( k  -  1 ) ) ) )  =  ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
319 ovex 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ ( k  -  1 ) ) )  e.  _V
320 oveq1 6287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  ( j  -  -u 1 )  ->  (
k  -  1 )  =  ( ( j  -  -u 1 )  - 
1 ) )
321320oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  ( j  -  -u 1 )  ->  ( C  -  ( k  -  1 ) )  =  ( C  -  ( ( j  -  -u 1 )  -  1 ) ) )
322320oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  ( j  -  -u 1 )  ->  ( CC𝑐 ( k  -  1 ) )  =  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) ) )
323321, 322oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  ( j  -  -u 1 )  ->  (
( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  =  ( ( C  -  (
( j  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1
)  -  1 ) ) ) )
324320oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  ( j  -  -u 1 )  ->  (
b ^ ( k  -  1 ) )  =  ( b ^
( ( j  -  -u 1 )  -  1 ) ) )
325323, 324oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  ( j  -  -u 1 )  ->  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) )  =  ( ( ( C  -  ( ( j  -  -u 1 )  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( j  -  -u 1
)  -  1 ) ) ) )
326 1pneg1e0 10687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1  +  -u 1 )  =  0
327326fveq2i 5854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ZZ>= `  ( 1  +  -u
1 ) )  =  ( ZZ>= `  0 )
328112, 327eqtr4i 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  NN0  =  ( ZZ>= `  ( 1  +  -u 1 ) )
329245znegcld 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
-u 1  e.  ZZ )
330318, 319, 325, 244, 328, 245, 329uzmptshftfval 36112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )  shift  -u 1 )  =  ( j  e. 
NN0  |->  ( ( ( C  -  ( ( j  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1
)  -  1 ) ) )  x.  (
b ^ ( ( j  -  -u 1
)  -  1 ) ) ) ) )
331 oveq1 6287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  =  k  ->  (
j  -  -u 1
)  =  ( k  -  -u 1 ) )
332331oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  =  k  ->  (
( j  -  -u 1
)  -  1 )  =  ( ( k  -  -u 1 )  - 
1 ) )
333332oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  k  ->  ( C  -  ( (
j  -  -u 1
)  -  1 ) )  =  ( C  -  ( ( k  -  -u 1 )  - 
1 ) ) )
334332oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  k  ->  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) )  =  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )
335333, 334oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  k  ->  (
( C  -  (
( j  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1
)  -  1 ) ) )  =  ( ( C  -  (
( k  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1
)  -  1 ) ) ) )
336332oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  k  ->  (
b ^ ( ( j  -  -u 1
)  -  1 ) )  =  ( b ^ ( ( k  -  -u 1 )  - 
1 ) ) )
337335, 336oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  =  k  ->  (
( ( C  -  ( ( j  -  -u 1 )  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( j  -  -u 1
)  -  1 ) ) )  =  ( ( ( C  -  ( ( k  -  -u 1 )  -  1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( k  -  -u 1
)  -  1 ) ) ) )
338337cbvmptv 4489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  NN0  |->  ( ( ( C  -  (
( j  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1
)  -  1 ) ) )  x.  (
b ^ ( ( j  -  -u 1
)  -  1 ) ) ) )  =  ( k  e.  NN0  |->  ( ( ( C  -  ( ( k  -  -u 1 )  - 
1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( k  -  -u 1
)  -  1 ) ) ) )
339338a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( j  e.  NN0  |->  ( ( ( C  -  ( ( j  -  -u 1 )  - 
1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( j  -  -u 1
)  -  1 ) ) ) )  =  ( k  e.  NN0  |->  ( ( ( C  -  ( ( k  -  -u 1 )  - 
1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( k  -  -u 1
)  -  1 ) ) ) ) )
340317, 330, 3393eqtrd 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( E `  b )  shift  -u 1
)  =  ( k  e.  NN0  |->  ( ( ( C  -  (
( k  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1
)  -  1 ) ) )  x.  (
b ^ ( ( k  -  -u 1
)  -  1 ) ) ) ) )
341 nn0cn 10848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN0  ->  k  e.  CC )
342 1cnd 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN0  ->  1  e.  CC )
343341, 342subnegd 9976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN0  ->  ( k  -  -u 1 )  =  ( k  +  1 ) )
344343oveq1d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN0  ->  ( ( k  -  -u 1
)  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
345341, 342pncand 9970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN0  ->  ( ( k  +  1 )  -  1 )  =  k )
346344, 345eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN0  ->  ( ( k  -  -u 1
)  -  1 )  =  k )
347346adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
k  -  -u 1
)  -  1 )  =  k )
348347oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( C  -  ( ( k  -  -u 1 )  - 
1 ) )  =  ( C  -  k
) )
349347oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( CC𝑐 (
( k  -  -u 1
)  -  1 ) )  =  ( CC𝑐 k ) )
350348, 349oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( C  -  ( (
k  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1
)  -  1 ) ) )  =  ( ( C  -  k
)  x.  ( CC𝑐 k ) ) )
351347oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( b ^ ( ( k  -  -u 1 )  - 
1 ) )  =  ( b ^ k
) )
352350, 351oveq12d 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( C  -  (
( k  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1
)  -  1 ) ) )  x.  (
b ^ ( ( k  -  -u 1
)  -  1 ) ) )  =  ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) ) )
353352mpteq2dva 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( k  e.  NN0  |->  ( ( ( C  -  ( ( k  -  -u 1 )  - 
1 ) )  x.  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )  x.  ( b ^ (
( k  -  -u 1
)  -  1 ) ) ) )  =  ( k  e.  NN0  |->  ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) ) ) )
354340, 353eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( E `  b )  shift  -u 1
)  =  ( k  e.  NN0  |->  ( ( ( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) ) ) )
355 ovex 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  _V
356355a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  _V )
357354, 356fvmpt2d 5945 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( E `  b
)  shift  -u 1 ) `  k )  =  ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) ) )
358246, 357sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( E `  b
)  shift  -u 1 ) `  k )  =  ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) ) )
359341adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  k  e.  CC )
360249, 359subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( C  -  k )  e.  CC )
361360, 251mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( C  -  k )  x.  ( CC𝑐 k ) )  e.  CC )
362361, 255mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  CC )
363246, 362sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  CC )
364 fveq2 5851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  j  ->  (
( E `  b
) `  k )  =  ( ( E `
 b ) `  j ) )
365364oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  j  ->  (
b  x.  ( ( E `  b ) `
 k ) )  =  ( b  x.  ( ( E `  b ) `  j
) ) )
366365cbvmptv 4489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  NN  |->  ( b  x.  ( ( E `
 b ) `  k ) ) )  =  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `  j
) ) )
367314oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( ( E `
 b ) `  k ) )  =  ( b  x.  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
368253adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  b  e.  CC )
36971ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  C  e.  CC )
370 nncn 10586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  k  e.  CC )
371370adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  k  e.  CC )
372 1cnd 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  1  e.  CC )
373371, 372subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( k  -  1 )  e.  CC )
374369, 373subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( C  -  ( k  - 
1 ) )  e.  CC )
375284adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( k  -  1 )  e. 
NN0 )
376369, 375bcccl 36105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
377374, 376mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  e.  CC )
378368, 375expcld 12356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( k  - 
1 ) )  e.  CC )
379368, 377, 378mul12d 9825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )  =  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b  x.  ( b ^ ( k  - 
1 ) ) ) ) )
380368, 378mulcomd 9649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( b ^
( k  -  1 ) ) )  =  ( ( b ^
( k  -  1 ) )  x.  b
) )
381368, 375expp1d 12357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( ( k  -  1 )  +  1 ) )  =  ( ( b ^
( k  -  1 ) )  x.  b
) )
382290adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  k  e.  NN )  ->  ( ( k  - 
1 )  +  1 )  =  k )
383382adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( k  -  1 )  +  1 )  =  k )
384383oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( ( k  -  1 )  +  1 ) )  =  ( b ^ k
) )
385380, 381, 3843eqtr2d 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( b ^
( k  -  1 ) ) )  =  ( b ^ k
) )
386385oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b  x.  ( b ^ ( k  - 
1 ) ) ) )  =  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) ) )
387379, 386eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )  =  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) ) )
388367, 387eqtrd 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( ( E `
 b ) `  k ) )  =  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) )
389388mpteq2dva 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( k  e.  NN  |->  ( b  x.  (
( E `  b
) `  k )
) )  =  ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) )
390366, 389syl5eqr 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( j  e.  NN  |->  ( b  x.  (
( E `  b
) `  j )
) )  =  ( k  e.  NN  |->  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) )
391 ovex 6308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) )  e.  _V
392391a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) )  e.  _V )
393390, 392fvmpt2d 5945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `
 j ) ) ) `  k )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k ) ) )
394377, 256mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) )  e.  CC )
395 climrel 13466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Rel  ~~>
396159simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  b  e.  D )  ->  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  )
397396adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( E `  b ) )  e. 
dom 
~~>  )
398 climdm 13528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( E `  b
) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
399397, 398sylib 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
400 0z 10918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  0  e.  ZZ
401 neg1z 10943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u 1  e.  ZZ
402 fvex 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E `
 b )  e. 
_V
403402seqshft 13069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 0  e.  ZZ  /\  -u 1  e.  ZZ )  ->  seq 0 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  =  (  seq ( 0  -  -u 1 ) (  +  ,  ( E `
 b ) ) 
shift  -u 1 ) )
404400, 401, 403mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  seq 0
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  =  (  seq (
0  -  -u 1
) (  +  , 
( E `  b
) )  shift  -u 1
)
405 0cn 9620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  CC
406405, 198subnegi 9936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  -  -u 1 )  =  ( 0  +  1 )
407 0p1e1 10690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  +  1 )  =  1
408406, 407eqtri 2433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0  -  -u 1 )  =  1
409 seqeq1 12156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 0  -  -u 1
)  =  1  ->  seq ( 0  -  -u 1
) (  +  , 
( E `  b
) )  =  seq 1 (  +  , 
( E `  b
) ) )
410408, 409ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  seq (
0  -  -u 1
) (  +  , 
( E `  b
) )  =  seq 1 (  +  , 
( E `  b
) )
411410oveq1i 6290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  (  seq ( 0  -  -u 1
) (  +  , 
( E `  b
) )  shift  -u 1
)  =  (  seq 1 (  +  , 
( E `  b
) )  shift  -u 1
)
412404, 411eqtri 2433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  seq 0
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  =  (  seq 1
(  +  ,  ( E `  b ) )  shift  -u 1 )
413412breq1i 4404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (  seq 0 (  +  , 
( ( E `  b )  shift  -u 1
) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  (  seq 1 (  +  , 
( E `  b
) )  shift  -u 1
)  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
414 seqex 12155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  seq 1
(  +  ,  ( E `  b ) )  e.  _V
415 climshft 13550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
-u 1  e.  ZZ  /\ 
seq 1 (  +  ,  ( E `  b ) )  e. 
_V )  ->  (
(  seq 1 (  +  ,  ( E `  b ) )  shift  -u
1 )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  seq 1
(  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) ) )
416401, 414, 415mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (  seq 1 (  +  ,  ( E `  b ) )  shift  -u
1 )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  seq 1
(  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
417413, 416bitri 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (  seq 0 (  +  , 
( ( E `  b )  shift  -u 1
) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  seq 1
(  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
418399, 417sylibr 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 0 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
419 releldm 5058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( Rel  ~~>  /\  seq 0
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  ~~>  (  ~~>  `  seq 1
(  +  ,  ( E `  b ) ) ) )  ->  seq 0 (  +  , 
( ( E `  b )  shift  -u 1
) )  e.  dom  ~~>  )
420395, 418, 419sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 0 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  e. 
dom 
~~>  )
421258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  1  e.  NN0 )
422357, 362eqeltrd 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( E `  b
)  shift  -u 1 ) `  k )  e.  CC )
423112, 421, 422iserex 13630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  (  seq 0 (  +  ,  ( ( E `  b ) 
shift  -u 1 ) )  e.  dom  ~~>  <->  seq 1
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  e.  dom  ~~>  ) )
424420, 423mpbid 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  e. 
dom 
~~>  )
425377, 378mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ ( k  -  1 ) ) )  e.  CC )
426314, 425eqeltrd 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( E `  b ) `
 k )  e.  CC )
427393, 388eqtr4d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `
 j ) ) ) `  k )  =  ( b  x.  ( ( E `  b ) `  k
) ) )
428244, 245, 253, 399, 426, 427isermulc2 13631 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `  j
) ) ) )  ~~>  ( b  x.  (  ~~>  ` 
seq 1 (  +  ,  ( E `  b ) ) ) ) )
429 releldm 5058 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Rel  ~~>  /\  seq 1
(  +  ,  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `
 j ) ) ) )  ~~>  ( b  x.  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) ) )  ->  seq 1
(  +  ,  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `
 j ) ) ) )  e.  dom  ~~>  )
430395, 428, 429sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `  j
) ) ) )  e.  dom  ~~>  )
431244, 245, 358, 363, 393, 394, 424, 430isumadd 13735 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN  ( ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k ) )  +  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k ) ) )  =  ( sum_ k  e.  NN  (
( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) )  +  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) )
432431oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( C  +  sum_ k  e.  NN  (
( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) )  +  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) )  =  ( C  +  ( sum_ k  e.  NN  ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) )  +  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) ) )
433369, 371subcld 9969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( C  -  k )  e.  CC )
434433, 252mulcld 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( C  -  k )  x.  ( CC𝑐 k ) )  e.  CC )
435434, 377, 256adddird 9653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  +  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) ) )  x.  ( b ^
k ) )  =  ( ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k ) )  +  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k ) ) ) )
436435sumeq2dv 13676 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN  ( ( ( ( C  -  k )  x.  ( CC𝑐 k ) )  +  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) ) )  x.  (
b ^ k ) )  =  sum_ k  e.  NN  ( ( ( ( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  +  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ k ) ) ) )
437436oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( C  +  sum_ k  e.  NN  (
( ( ( C  -  k )  x.  ( CC𝑐 k ) )  +  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) ) )  x.  ( b ^
k ) ) )  =  ( C  +  sum_ k  e.  NN  (
( ( ( C  -  k )  x.  ( CC𝑐 k ) )  x.  ( b ^ k
) )  +  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ k
) ) ) ) )
438312sumeq2dv 13676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  b  e.  CC )  ->  sum_ k  e.  NN  ( ( E `
 b ) `  k )  =  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
439438oveq2d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  b  e.  CC )  ->  ( ( 1  +  b )  x.  sum_ k  e.  NN  ( ( E `  b ) `  k
) )  =  ( ( 1  +  b )  x.  sum_ k  e.  NN  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) ) )
440119, 439sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  b  e.  D )  ->  (
( 1  +  b )  x.  sum_ k  e.  NN  ( ( E `
 b ) `  k ) )  =  ( ( 1  +  b )  x.  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
441440adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( 1  +  b )  x.  sum_ k  e.  NN  (
( E `  b
) `  k )
)  =  ( ( 1  +  b )  x.  sum_ k  e.  NN  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
442244, 245, 314, 425, 397isumcl 13729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) )  e.  CC )
443243, 253, 442adddird 9653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( ( 1  +  b )  x.  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )  =  ( ( 1  x. 
sum_ k  e.  NN  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )  +  ( b  x.  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) ) ) )
444442mulid2d 9646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( 1  x.  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )  = 
sum_ k  e.  NN  ( ( ( C  -  ( k  - 
1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )
445244, 245, 314, 425, 397, 253isummulc2 13730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( b  x.  sum_ k  e.  NN  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) ) ) )  = 
sum_ k  e.  NN  ( b  x.  (
( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ (
k  -  1 ) )