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

Theorem binomcxplemnotnn0 36569
Description: Lemma for binomcxp 36570. When  C is not a nonnegative integer, the generalized sum in binomcxplemnn0 36562 —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 23377 gives the derivative of  P, which by dvradcnv 23368 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 2585 . . . . . . . . . 10  |-  F/_ b `' abs
4 nfcv 2585 . . . . . . . . . . 11  |-  F/_ b
0
5 nfcv 2585 . . . . . . . . . . 11  |-  F/_ b [,)
6 binomcxplem.r . . . . . . . . . . . 12  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
7 nfcv 2585 . . . . . . . . . . . . . . . 16  |-  F/_ b  +
8 binomcxplem.s . . . . . . . . . . . . . . . . . 18  |-  S  =  ( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
9 nfmpt1 4511 . . . . . . . . . . . . . . . . . 18  |-  F/_ b
( b  e.  CC  |->  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
108, 9nfcxfr 2583 . . . . . . . . . . . . . . . . 17  |-  F/_ b S
11 nfcv 2585 . . . . . . . . . . . . . . . . 17  |-  F/_ b
r
1210, 11nffv 5886 . . . . . . . . . . . . . . . 16  |-  F/_ b
( S `  r
)
134, 7, 12nfseq 12224 . . . . . . . . . . . . . . 15  |-  F/_ b  seq 0 (  +  , 
( S `  r
) )
1413nfel1 2601 . . . . . . . . . . . . . 14  |-  F/ b  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>
15 nfcv 2585 . . . . . . . . . . . . . 14  |-  F/_ b RR
1614, 15nfrab 3011 . . . . . . . . . . . . 13  |-  F/_ b { r  e.  RR  |  seq 0 (  +  ,  ( S `  r ) )  e. 
dom 
~~>  }
17 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ b RR*
18 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ b  <
1916, 17, 18nfsup 7969 . . . . . . . . . . . 12  |-  F/_ b sup ( { r  e.  RR  |  seq 0
(  +  ,  ( S `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )
206, 19nfcxfr 2583 . . . . . . . . . . 11  |-  F/_ b R
214, 5, 20nfov 6329 . . . . . . . . . 10  |-  F/_ b
( 0 [,) R
)
223, 21nfima 5193 . . . . . . . . 9  |-  F/_ b
( `' abs " (
0 [,) R ) )
232, 22nfcxfr 2583 . . . . . . . 8  |-  F/_ b D
24 nfcv 2585 . . . . . . . 8  |-  F/_ x D
25 nfcv 2585 . . . . . . . 8  |-  F/_ x sum_ k  e.  NN0  (
( S `  b
) `  k )
26 nfcv 2585 . . . . . . . . 9  |-  F/_ b NN0
27 nfcv 2585 . . . . . . . . . . 11  |-  F/_ b
x
2810, 27nffv 5886 . . . . . . . . . 10  |-  F/_ b
( S `  x
)
29 nfcv 2585 . . . . . . . . . 10  |-  F/_ b
k
3028, 29nffv 5886 . . . . . . . . 9  |-  F/_ b
( ( S `  x ) `  k
)
3126, 30nfsum 13750 . . . . . . . 8  |-  F/_ b sum_ k  e.  NN0  (
( S `  x
) `  k )
32 simpl 459 . . . . . . . . . . 11  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
b  =  x )
3332fveq2d 5883 . . . . . . . . . 10  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
( S `  b
)  =  ( S `
 x ) )
3433fveq1d 5881 . . . . . . . . 9  |-  ( ( b  =  x  /\  k  e.  NN0 )  -> 
( ( S `  b ) `  k
)  =  ( ( S `  x ) `
 k ) )
3534sumeq2dv 13762 . . . . . . . 8  |-  ( b  =  x  ->  sum_ k  e.  NN0  ( ( S `
 b ) `  k )  =  sum_ k  e.  NN0  ( ( S `  x ) `
 k ) )
3623, 24, 25, 31, 35cbvmptf 4512 . . . . . . 7  |-  ( b  e.  D  |->  sum_ k  e.  NN0  ( ( S `
 b ) `  k ) )  =  ( x  e.  D  |-> 
sum_ k  e.  NN0  ( ( S `  x ) `  k
) )
371, 36eqtri 2452 . . . . . 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 761 . . . . . . . 8  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  x  =  ( B  /  A ) )
4039fveq2d 5883 . . . . . . 7  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  ( S `  x )  =  ( S `  ( B  /  A
) ) )
4140fveq1d 5881 . . . . . 6  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  =  ( B  /  A ) )  /\  k  e. 
NN0 )  ->  (
( S `  x
) `  k )  =  ( ( S `
 ( B  /  A ) ) `  k ) )
4241sumeq2dv 13762 . . . . 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 9671 . . . . . . . 8  |-  ( ph  ->  B  e.  CC )
4544adantr 467 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  B  e.  CC )
46 binomcxp.a . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
4746rpcnd 11345 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
4847adantr 467 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  A  e.  CC )
49 0red 9646 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  e.  RR )
5045abscld 13491 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  e.  RR )
5148abscld 13491 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  RR )
5245absge0d 13499 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <_  ( abs `  B
) )
53 binomcxp.lt . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  B
)  <  ( abs `  A ) )
5453adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  < 
( abs `  A
) )
5549, 50, 51, 52, 54lelttrd 9795 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <  ( abs `  A
) )
5655gt0ne0d 10180 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  =/=  0 )
5748abs00ad 13347 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  =  0  <->  A  =  0 ) )
5857necon3bid 2683 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  =/=  0  <->  A  =/=  0 ) )
5956, 58mpbid 214 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  A  =/=  0 )
6045, 48, 59divcld 10385 . . . . . 6  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( B  /  A )  e.  CC )
6160abscld 13491 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  e.  RR )
6260absge0d 13499 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  <_  ( abs `  ( B  /  A ) ) )
6351recnd 9671 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  CC )
6463mulid1d 9662 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  A
)  x.  1 )  =  ( abs `  A
) )
6554, 64breqtrrd 4448 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  B )  < 
( ( abs `  A
)  x.  1 ) )
66 1red 9660 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  1  e.  RR )
6751, 55elrpd 11340 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  A )  e.  RR+ )
6850, 66, 67ltdivmuld 11391 . . . . . . . . 9  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( ( abs `  B
)  /  ( abs `  A ) )  <  1  <->  ( abs `  B
)  <  ( ( abs `  A )  x.  1 ) ) )
6965, 68mpbird 236 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
( abs `  B
)  /  ( abs `  A ) )  <  1 )
7045, 48, 59absdivd 13510 . . . . . . . 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 36565 . . . . . . . 8  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  R  =  1 )
7469, 70, 733brtr4d 4452 . . . . . . 7  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  < 
R )
75 0re 9645 . . . . . . . 8  |-  0  e.  RR
76 ssrab2 3547 . . . . . . . . . . 11  |-  { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } 
C_  RR
77 ressxr 9686 . . . . . . . . . . 11  |-  RR  C_  RR*
7876, 77sstri 3474 . . . . . . . . . 10  |-  { r  e.  RR  |  seq 0 (  +  , 
( S `  r
) )  e.  dom  ~~>  } 
C_  RR*
79 supxrcl 11602 . . . . . . . . . 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 2507 . . . . . . . 8  |-  R  e. 
RR*
82 elico2 11700 . . . . . . . 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 677 . . . . . . 7  |-  ( ( abs `  ( B  /  A ) )  e.  ( 0 [,) R )  <->  ( ( abs `  ( B  /  A ) )  e.  RR  /\  0  <_ 
( abs `  ( B  /  A ) )  /\  ( abs `  ( B  /  A ) )  <  R ) )
8461, 62, 74, 83syl3anbrc 1190 . . . . . 6  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( abs `  ( B  /  A ) )  e.  ( 0 [,) R
) )
852eleq2i 2501 . . . . . . 7  |-  ( ( B  /  A )  e.  D  <->  ( B  /  A )  e.  ( `' abs " ( 0 [,) R ) ) )
86 absf 13394 . . . . . . . 8  |-  abs : CC
--> RR
87 ffn 5744 . . . . . . . 8  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
88 elpreima 6015 . . . . . . . 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 253 . . . . . 6  |-  ( ( B  /  A )  e.  D  <->  ( ( B  /  A )  e.  CC  /\  ( abs `  ( B  /  A
) )  e.  ( 0 [,) R ) ) )
9160, 84, 90sylanbrc 669 . . . . 5  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( B  /  A )  e.  D )
92 sumex 13747 . . . . . 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 5968 . . . 4  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( P `  ( B  /  A ) )  = 
sum_ k  e.  NN0  ( ( S `  ( B  /  A
) ) `  k
) )
95 eqid 2423 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
9695cnbl0 21786 . . . . . . . . . . . 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 2452 . . . . . . . . . 10  |-  D  =  ( 0 ( ball `  ( abs  o.  -  ) ) R )
99 0cnd 9638 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  0  e.  CC )
10081a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  R  e.  RR* )
101 mulcl 9625 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
102101adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  ( x  e.  CC  /\  y  e.  CC ) )  ->  ( x  x.  y )  e.  CC )
103 nfv 1752 . . . . . . . . . . . . . . 15  |-  F/ b ( ph  /\  -.  C  e.  NN0 )
10423nfcri 2578 . . . . . . . . . . . . . . 15  |-  F/ b  x  e.  D
105103, 104nfan 1985 . . . . . . . . . . . . . 14  |-  F/ b ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D
)
10631nfel1 2601 . . . . . . . . . . . . . 14  |-  F/ b
sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC
107105, 106nfim 1977 . . . . . . . . . . . . 13  |-  F/ b ( ( ( ph  /\ 
-.  C  e.  NN0 )  /\  x  e.  D
)  ->  sum_ k  e. 
NN0  ( ( S `
 x ) `  k )  e.  CC )
108 eleq1 2495 . . . . . . . . . . . . . . 15  |-  ( b  =  x  ->  (
b  e.  D  <->  x  e.  D ) )
109108anbi2d 709 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  <->  ( ( ph  /\ 
-.  C  e.  NN0 )  /\  x  e.  D
) ) )
11035eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  ( sum_ k  e.  NN0  (
( S `  b
) `  k )  e.  CC  <->  sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC ) )
111109, 110imbi12d 322 . . . . . . . . . . . . 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 11195 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
113 0zd 10951 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  0  e.  ZZ )
114 eqidd 2424 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( S `  b ) `  k )  =  ( ( S `  b
) `  k )
)
115 cnvimass 5205 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' abs " ( 0 [,) R ) ) 
C_  dom  abs
1162, 115eqsstri 3495 . . . . . . . . . . . . . . . . . . 19  |-  D  C_  dom  abs
11786fdmi 5749 . . . . . . . . . . . . . . . . . . 19  |-  dom  abs  =  CC
118116, 117sseqtri 3497 . . . . . . . . . . . . . . . . . 18  |-  D  C_  CC
119118sseli 3461 . . . . . . . . . . . . . . . . 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 10877 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  e.  _V
122121mptex 6149 . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  b  e.  CC )  ->  ( S `
 b )  =  ( k  e.  NN0  |->  ( ( F `  k )  x.  (
b ^ k ) ) ) )
125 ovex 6331 . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
j  =  k )
130129oveq2d 6319 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  j  =  k )  -> 
( CC𝑐 j )  =  ( CC𝑐 k ) )
131 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  NN0 )
132 ovex 6331 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( CC𝑐 k )  e.  _V
133132a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( CC𝑐 k
)  e.  _V )
134128, 130, 131, 133fvmptd 5968 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  =  ( CC𝑐 k ) )
135134oveq1d 6318 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( F `  k )  x.  ( b ^ k
) )  =  ( ( CC𝑐 k )  x.  (
b ^ k ) ) )
136135adantlr 720 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( F `  k
)  x.  ( b ^ k ) )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
137127, 136eqtrd 2464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
138119, 137sylanl2 656 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
13971ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  C  e.  CC )
140 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  k  e.  NN0 )
141139, 140bcccl 36552 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  ( CC𝑐 k )  e.  CC )
142119ad2antlr 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  b  e.  CC )
143142, 140expcld 12417 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
b ^ k )  e.  CC )
144141, 143mulcld 9665 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( CC𝑐 k )  x.  (
b ^ k ) )  e.  CC )
145138, 144eqeltrd 2511 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN0 )  ->  (
( S `  b
) `  k )  e.  CC )
146145adantllr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( S `  b ) `  k )  e.  CC )
147 eleq1 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (
x  e.  D  <->  b  e.  D ) )
148147anbi2d 709 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  b  ->  (
( ph  /\  x  e.  D )  <->  ( ph  /\  b  e.  D ) ) )
149 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  b  ->  ( S `  x )  =  ( S `  b ) )
150149seqeq3d 12222 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  b  ->  seq 0 (  +  , 
( S `  x
) )  =  seq 0 (  +  , 
( S `  b
) ) )
151150eleq1d 2492 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (  seq 0 (  +  , 
( S `  x
) )  e.  dom  ~~>  <->  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  ) )
152 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  b  ->  ( E `  x )  =  ( E `  b ) )
153152seqeq3d 12222 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  b  ->  seq 1 (  +  , 
( E `  x
) )  =  seq 1 (  +  , 
( E `  b
) ) )
154153eleq1d 2492 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  b  ->  (  seq 1 (  +  , 
( E `  x
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  ) )
155151, 154anbi12d 716 . . . . . . . . . . . . . . . . . 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 322 . . . . . . . . . . . . . . . . 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 36567 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  D )  ->  (  seq 0 (  +  , 
( S `  x
) )  e.  dom  ~~>  /\ 
seq 1 (  +  ,  ( E `  x ) )  e. 
dom 
~~>  ) )
159156, 158chvarv 2069 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  D )  ->  (  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  /\ 
seq 1 (  +  ,  ( E `  b ) )  e. 
dom 
~~>  ) )
160159simpld 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  D )  ->  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  )
161160adantlr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 0 (  +  ,  ( S `  b ) )  e. 
dom 
~~>  )
162112, 113, 114, 146, 161isumcl 13815 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN0  ( ( S `  b ) `  k
)  e.  CC )
163107, 111, 162chvar 2068 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  -> 
sum_ k  e.  NN0  ( ( S `  x ) `  k
)  e.  CC )
164163, 37fmptd 6059 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  P : D --> CC )
165 1cnd 9661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  1  e.  CC )
166118sseli 3461 . . . . . . . . . . . . . . 15  |-  ( x  e.  D  ->  x  e.  CC )
167166adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  x  e.  CC )
168165, 167addcld 9664 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( 1  +  x
)  e.  CC )
16971ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  C  e.  CC )
170169negcld 9975 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  -> 
-u C  e.  CC )
171168, 170cxpcld 23645 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( ( 1  +  x )  ^c  -u C )  e.  CC )
172 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ x
( ( 1  +  b )  ^c  -u C )
173 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ b
( ( 1  +  x )  ^c  -u C )
174 oveq2 6311 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
1  +  b )  =  ( 1  +  x ) )
175174oveq1d 6318 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
( 1  +  b )  ^c  -u C )  =  ( ( 1  +  x
)  ^c  -u C ) )
17623, 24, 172, 173, 175cbvmptf 4512 . . . . . . . . . . . 12  |-  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C
) )  =  ( x  e.  D  |->  ( ( 1  +  x
)  ^c  -u C ) )
177171, 176fmptd 6059 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) : D --> CC )
178 cnex 9622 . . . . . . . . . . . . . . . 16  |-  CC  e.  _V
179 fex 6151 . . . . . . . . . . . . . . . 16  |-  ( ( abs : CC --> RR  /\  CC  e.  _V )  ->  abs  e.  _V )
18086, 178, 179mp2an 677 . . . . . . . . . . . . . . 15  |-  abs  e.  _V
181180cnvex 6752 . . . . . . . . . . . . . 14  |-  `' abs  e.  _V
182 imaexg 6742 . . . . . . . . . . . . . 14  |-  ( `' abs  e.  _V  ->  ( `' abs " ( 0 [,) R ) )  e.  _V )
183181, 182ax-mp 5 . . . . . . . . . . . . 13  |-  ( `' abs " ( 0 [,) R ) )  e.  _V
1842, 183eqeltri 2507 . . . . . . . . . . . 12  |-  D  e. 
_V
185184a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  D  e.  _V )
186 inidm 3672 . . . . . . . . . . 11  |-  ( D  i^i  D )  =  D
187102, 164, 177, 185, 185, 186off 6558 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( P  oF  x.  (
b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) ) : D --> CC )
188 1ex 9640 . . . . . . . . . . . . . 14  |-  1  e.  _V
189188fconst 5784 . . . . . . . . . . . . 13  |-  ( D  X.  { 1 } ) : D --> { 1 }
190 fconstmpt 4895 . . . . . . . . . . . . . . 15  |-  ( D  X.  { 1 } )  =  ( x  e.  D  |->  1 )
191 nfcv 2585 . . . . . . . . . . . . . . . 16  |-  F/_ b
1
192 nfcv 2585 . . . . . . . . . . . . . . . 16  |-  F/_ x
1
193 eqidd 2424 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  1  =  1 )
19424, 23, 191, 192, 193cbvmptf 4512 . . . . . . . . . . . . . . 15  |-  ( x  e.  D  |->  1 )  =  ( b  e.  D  |->  1 )
195190, 194eqtri 2452 . . . . . . . . . . . . . 14  |-  ( D  X.  { 1 } )  =  ( b  e.  D  |->  1 )
196195feq1i 5736 . . . . . . . . . . . . 13  |-  ( ( D  X.  { 1 } ) : D --> { 1 }  <->  ( b  e.  D  |->  1 ) : D --> { 1 } )
197189, 196mpbi 212 . . . . . . . . . . . 12  |-  ( b  e.  D  |->  1 ) : D --> { 1 }
198 ax-1cn 9599 . . . . . . . . . . . . 13  |-  1  e.  CC
199 snssi 4142 . . . . . . . . . . . . 13  |-  ( 1  e.  CC  ->  { 1 }  C_  CC )
200198, 199ax-mp 5 . . . . . . . . . . . 12  |-  { 1 }  C_  CC
201 fss 5752 . . . . . . . . . . . 12  |-  ( ( ( b  e.  D  |->  1 ) : D --> { 1 }  /\  { 1 }  C_  CC )  ->  ( b  e.  D  |->  1 ) : D --> CC )
202197, 200, 201mp2an 677 . . . . . . . . . . 11  |-  ( b  e.  D  |->  1 ) : D --> CC
203202a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  (
b  e.  D  |->  1 ) : D --> CC )
204 cnelprrecn 9634 . . . . . . . . . . . . . . . . 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 36568 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( CC  _D  P
)  =  ( b  e.  D  |->  sum_ k  e.  NN  ( ( E `
 b ) `  k ) ) )
207206adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P )  =  ( b  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  b ) `  k
) ) )
208 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x sum_ k  e.  NN  (
( E `  b
) `  k )
209 nfcv 2585 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ b NN
210 nfmpt1 4511 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ b
( b  e.  CC  |->  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
211157, 210nfcxfr 2583 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ b E
212211, 27nffv 5886 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ b
( E `  x
)
213212, 29nffv 5886 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ b
( ( E `  x ) `  k
)
214209, 213nfsum 13750 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ b sum_ k  e.  NN  (
( E `  x
) `  k )
215 simpl 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  =  x  /\  k  e.  NN )  ->  b  =  x )
216215fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  =  x  /\  k  e.  NN )  ->  ( E `  b
)  =  ( E `
 x ) )
217216fveq1d 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( b  =  x  /\  k  e.  NN )  ->  ( ( E `  b ) `  k
)  =  ( ( E `  x ) `
 k ) )
218217sumeq2dv 13762 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  x  ->  sum_ k  e.  NN  ( ( E `
 b ) `  k )  =  sum_ k  e.  NN  (
( E `  x
) `  k )
)
21923, 24, 208, 214, 218cbvmptf 4512 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  D  |->  sum_ k  e.  NN  ( ( E `
 b ) `  k ) )  =  ( x  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  x ) `  k
) )
220207, 219syl6eq 2480 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P )  =  ( x  e.  D  |-> 
sum_ k  e.  NN  ( ( E `  x ) `  k
) ) )
221 sumex 13747 . . . . . . . . . . . . . . . . . . 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 6060 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  P ) : D --> _V )
224 fdm 5748 . . . . . . . . . . . . . . . . 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 36566 . . . . . . . . . . . . . . . . . . 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 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( -u C  x.  (
( 1  +  b )  ^c  (
-u C  -  1 ) ) )
228 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ b
( -u C  x.  (
( 1  +  x
)  ^c  (
-u C  -  1 ) ) )
229174oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  x  ->  (
( 1  +  b )  ^c  (
-u C  -  1 ) )  =  ( ( 1  +  x
)  ^c  (
-u C  -  1 ) ) )
230229oveq2d 6319 . . . . . . . . . . . . . . . . . . . 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 4512 . . . . . . . . . . . . . . . . . . 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 2480 . . . . . . . . . . . . . . . . . 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 9988 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( -u C  - 
1 )  e.  CC )
234168, 233cxpcld 23645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( ( 1  +  x )  ^c 
( -u C  -  1 ) )  e.  CC )
235170, 234mulcld 9665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  x  e.  D )  ->  ( -u C  x.  ( ( 1  +  x )  ^c 
( -u C  -  1 ) ) )  e.  CC )
236232, 235fmpt3d 6060 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  C  e.  NN0 )  ->  ( CC  _D  ( b  e.  D  |->  ( ( 1  +  b )  ^c  -u C ) ) ) : D --> CC )
237 fdm 5748 . . . . . . . . . . . . . . . . 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 22889 . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  C  e.  CC )
241240mulid1d 9662 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( C  x.  1 )  =  C )
242241oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . 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 9661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  1  e.  CC )
244 nnuz 11196 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  NN  =  ( ZZ>= `  1 )
245 1zzd 10970 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  1  e.  ZZ )
246 nnnn0 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  NN  ->  k  e.  NN0 )
247246, 138sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN )  ->  (
( S `  b
) `  k )  =  ( ( CC𝑐 k )  x.  ( b ^ k ) ) )
248247adantllr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( S `  b ) `
 k )  =  ( ( CC𝑐 k )  x.  ( b ^
k ) ) )
24971ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  C  e.  CC )
250 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
251249, 250bcccl 36552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( CC𝑐 k
)  e.  CC )
252246, 251sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( CC𝑐 k )  e.  CC )
253119adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  b  e.  CC )
254253adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  b  e.  CC )
255254, 250expcld 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( b ^ k )  e.  CC )
256246, 255sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ k )  e.  CC )
257252, 256mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( CC𝑐 k )  x.  (
b ^ k ) )  e.  CC )
258 1nn0 10887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  1  e.  NN0
259258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  b  e.  D )  ->  1  e.  NN0 )
260112, 259, 145iserex 13713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  b  e.  D )  ->  (  seq 0 (  +  , 
( S `  b
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( S `  b
) )  e.  dom  ~~>  ) )
261160, 260mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  b  e.  D )  ->  seq 1 (  +  , 
( S `  b
) )  e.  dom  ~~>  )
262261adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( S `  b ) )  e. 
dom 
~~>  )
263244, 245, 248, 257, 262isumcl 13815 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
sum_ k  e.  NN  ( ( CC𝑐 k )  x.  ( b ^
k ) )  e.  CC )
264240, 243, 263adddid 9669 . . . . . . . . . . . . . . . . . . . . . . 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 10617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  NN  e.  _V
267266mptex 6149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  b  e.  CC )  ->  ( E `
 b )  =  ( k  e.  NN  |->  ( ( k  x.  ( F `  k
) )  x.  (
b ^ ( k  -  1 ) ) ) ) )
270119, 269sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  b  e.  D )  ->  ( E `  b )  =  ( k  e.  NN  |->  ( ( k  x.  ( F `  k ) )  x.  ( b ^ (
k  -  1 ) ) ) ) )
271270adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
)  =  ( k  e.  NN  |->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) ) ) )
272 ovex 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  ( E `  b
) : NN --> _V )
275274feqmptd 5932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( k  x.  ( F `  k ) )  x.  ( b ^ (
k  -  1 ) ) ) )
278246, 134sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  =  ( CC𝑐 k ) )
279278oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( F `  k ) )  =  ( k  x.  ( CC𝑐 k ) ) )
280279oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  x.  ( F `
 k ) )  x.  ( b ^
( k  -  1 ) ) )  =  ( ( k  x.  ( CC𝑐 k ) )  x.  ( b ^ (
k  -  1 ) ) ) )
281280adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( k  x.  ( CC𝑐 k ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
28371adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  C  e.  CC )
284 nnm1nn0 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( k  e.  NN  ->  (
k  -  1 )  e.  NN0 )
285284adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  -  1 )  e. 
NN0 )
286283, 285bccp1k 36554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( ( k  -  1 )  +  1 ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  ( ( k  -  1 )  +  1 ) ) ) )
287246adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  k  e.  NN )  ->  k  e. 
NN0 )
288287nn0cnd 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
289 1cnd 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  CC )
290288, 289npcand 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  -  1 )  +  1 )  =  k )
291290oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( ( k  -  1 )  +  1 ) )  =  ( CC𝑐 k ) )
292290oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( C  -  ( k  -  1 ) )  /  ( ( k  -  1 )  +  1 ) )  =  ( ( C  -  ( k  -  1 ) )  /  k
) )
293292oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 k )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  (
( C  -  (
k  -  1 ) )  /  k ) ) )
295294oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( CC𝑐 k ) )  =  ( k  x.  ( ( CC𝑐 ( k  -  1 ) )  x.  ( ( C  -  ( k  -  1 ) )  /  k ) ) ) )
296283, 285bcccl 36552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
297288, 289subcld 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  -  1 )  e.  CC )
298283, 297subcld 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  ( C  -  ( k  - 
1 ) )  e.  CC )
299 nnne0 10644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  NN  ->  k  =/=  0 )
300299adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
301296, 298, 288, 300divassd 10420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  /  k )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  ( ( C  -  ( k  -  1 ) )  /  k ) ) )
302301oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  e.  CC )
304303, 288, 300divcan2d 10387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  x.  ( CC𝑐 k ) )  =  ( ( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) ) )
306305oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
309298adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  ( C  -  ( k  -  1 ) )  e.  CC )
310308, 309mulcomd 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( CC𝑐 ( k  -  1 ) )  x.  ( C  -  ( k  -  1 ) ) )  =  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) ) )
311310oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  b  e.  CC )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
313119, 312sylanl2 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  b  e.  D )  /\  k  e.  NN )  ->  (
( E `  b
) `  k )  =  ( ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  ( b ^ ( k  - 
1 ) ) ) )
314313adantllr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  x.  (
b ^ ( k  -  1 ) ) )  e.  _V
320 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  =  ( j  -  -u 1 )  ->  (
k  -  1 )  =  ( ( j  -  -u 1 )  - 
1 ) )
321320oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  ( j  -  -u 1 )  ->  ( C  -  ( k  -  1 ) )  =  ( C  -  ( ( j  -  -u 1 )  -  1 ) ) )
322320oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  ( j  -  -u 1 )  ->  ( CC𝑐 ( k  -  1 ) )  =  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) ) )
323321, 322oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  ( j  -  -u 1 )  ->  (
( C  -  (
k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  =  ( ( C  -  (
( j  -  -u 1
)  -  1 ) )  x.  ( CC𝑐 ( ( j  -  -u 1
)  -  1 ) ) ) )
324320oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  ( j  -  -u 1 )  ->  (
b ^ ( k  -  1 ) )  =  ( b ^
( ( j  -  -u 1 )  -  1 ) ) )
325323, 324oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1  +  -u 1 )  =  0
327326fveq2i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ZZ>= `  ( 1  +  -u
1 ) )  =  ( ZZ>= `  0 )
328112, 327eqtr4i 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  NN0  =  ( ZZ>= `  ( 1  +  -u 1 ) )
329245znegcld 11044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  -> 
-u 1  e.  ZZ )
330318, 319, 325, 244, 328, 245, 329uzmptshftfval 36559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  =  k  ->  (
j  -  -u 1
)  =  ( k  -  -u 1 ) )
332331oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  =  k  ->  (
( j  -  -u 1
)  -  1 )  =  ( ( k  -  -u 1 )  - 
1 ) )
333332oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  k  ->  ( C  -  ( (
j  -  -u 1
)  -  1 ) )  =  ( C  -  ( ( k  -  -u 1 )  - 
1 ) ) )
334332oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  k  ->  ( CC𝑐 ( ( j  -  -u 1 )  -  1 ) )  =  ( CC𝑐 ( ( k  -  -u 1 )  -  1 ) ) )
335333, 334oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  k  ->  (
b ^ ( ( j  -  -u 1
)  -  1 ) )  =  ( b ^ ( ( k  -  -u 1 )  - 
1 ) ) )
337335, 336oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN0  ->  k  e.  CC )
342 1cnd 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN0  ->  1  e.  CC )
343341, 342subnegd 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN0  ->  ( k  -  -u 1 )  =  ( k  +  1 ) )
344343oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN0  ->  ( ( k  -  -u 1
)  -  1 )  =  ( ( k  +  1 )  - 
1 ) )
345341, 342pncand 9989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN0  ->  ( ( k  +  1 )  -  1 )  =  k )
346344, 345eqtrd 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN0  ->  ( ( k  -  -u 1
)  -  1 )  =  k )
347346adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
k  -  -u 1
)  -  1 )  =  k )
348347oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( C  -  ( ( k  -  -u 1 )  - 
1 ) )  =  ( C  -  k
) )
349347oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( CC𝑐 (
( k  -  -u 1
)  -  1 ) )  =  ( CC𝑐 k ) )
350348, 349oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( b ^ ( ( k  -  -u 1 )  - 
1 ) )  =  ( b ^ k
) )
352350, 351oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  k  e.  CC )
360249, 359subcld 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( C  -  k )  e.  CC )
361360, 251mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( ( C  -  k )  x.  ( CC𝑐 k ) )  e.  CC )
362361, 255mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  CC )
363246, 362sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( ( C  -  k
)  x.  ( CC𝑐 k ) )  x.  (
b ^ k ) )  e.  CC )
364 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  j  ->  (
( E `  b
) `  k )  =  ( ( E `
 b ) `  j ) )
365364oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  j  ->  (
b  x.  ( ( E `  b ) `
 k ) )  =  ( b  x.  ( ( E `  b ) `  j
) ) )
366365cbvmptv 4514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  NN  |->  ( b  x.  ( ( E `
 b ) `  k ) ) )  =  ( j  e.  NN  |->  ( b  x.  ( ( E `  b ) `  j
) ) )
367314oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  b  e.  CC )
36971ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  C  e.  CC )
370 nncn 10619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  k  e.  CC )
371370adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  k  e.  CC )
372 1cnd 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  1  e.  CC )
373371, 372subcld 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( k  -  1 )  e.  CC )
374369, 373subcld 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( C  -  ( k  - 
1 ) )  e.  CC )
375284adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( k  -  1 )  e. 
NN0 )
376369, 375bcccl 36552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( CC𝑐 ( k  -  1 ) )  e.  CC )
377374, 376mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( C  -  ( k  -  1 ) )  x.  ( CC𝑐 ( k  -  1 ) ) )  e.  CC )
378368, 375expcld 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( k  - 
1 ) )  e.  CC )
379368, 377, 378mul12d 9844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( b ^
( k  -  1 ) ) )  =  ( ( b ^
( k  -  1 ) )  x.  b
) )
381368, 375expp1d 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( ( k  -  1 )  +  1 ) )  =  ( ( b ^
( k  -  1 ) )  x.  b
) )
382290adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  k  e.  NN )  ->  ( ( k  - 
1 )  +  1 )  =  k )
383382adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( k  -  1 )  +  1 )  =  k )
384383oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b ^ ( ( k  -  1 )  +  1 ) )  =  ( b ^ k
) )
385380, 381, 3843eqtr2d 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( b  x.  ( b ^
( k  -  1 ) ) )  =  ( b ^ k
) )
386385oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Rel  ~~>
396159simprd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  b  e.  D )  ->  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  )
397396adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( E `  b ) )  e. 
dom 
~~>  )
398 climdm 13611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (  seq 1 (  +  , 
( E `  b
) )  e.  dom  ~~>  <->  seq 1 (  +  , 
( E `  b
) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
399397, 398sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
400 0z 10950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  0  e.  ZZ
401 neg1z 10975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -u 1  e.  ZZ
402 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E `
 b )  e. 
_V
403402seqshft 13142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  seq 0
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  =  (  seq (
0  -  -u 1
) (  +  , 
( E `  b
) )  shift  -u 1
)
405 0cn 9637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  CC
406405, 198subnegi 9955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  -  -u 1 )  =  ( 0  +  1 )
407 0p1e1 10723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 0  +  1 )  =  1
408406, 407eqtri 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 0  -  -u 1 )  =  1
409 seqeq1 12217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  (  seq ( 0  -  -u 1
) (  +  , 
( E `  b
) )  shift  -u 1
)  =  (  seq 1 (  +  , 
( E `  b
) )  shift  -u 1
)
412404, 411eqtri 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  seq 0
(  +  ,  ( ( E `  b
)  shift  -u 1 ) )  =  (  seq 1
(  +  ,  ( E `  b ) )  shift  -u 1 )
413412breq1i 4428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  seq 1
(  +  ,  ( E `  b ) )  e.  _V
415 climshft 13633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (  seq 1 (  +  ,  ( E `  b ) )  shift  -u
1 )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  seq 1
(  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
417413, 416bitri 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (  seq 0 (  +  , 
( ( E `  b )  shift  -u 1
) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) )  <->  seq 1
(  +  ,  ( E `  b ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
418399, 417sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 0 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  ~~>  (  ~~>  `  seq 1 (  +  , 
( E `  b
) ) ) )
419 releldm 5084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN0 )  ->  ( (
( E `  b
)  shift  -u 1 ) `  k )  e.  CC )
423112, 421, 422iserex 13713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D )  ->  seq 1 (  +  ,  ( ( E `
 b )  shift  -u
1 ) )  e. 
dom 
~~>  )
425377, 378mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( E `  b ) `
 k )  e.  CC )
427393, 388eqtr4d 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13821 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . 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 9988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( C  -  k )  e.  CC )
434433, 252mulcld 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  C  e.  NN0 )  /\  b  e.  D
)  /\  k  e.  NN )  ->  ( ( C  -  k )  x.  ( CC𝑐 k ) )  e.  CC )
435434, 377, 256adddird 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13762 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . 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 13762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
446387