Metamath Proof Explorer

Theorem binomcxplemdvbinom

Description: Lemma for binomcxp . By the power and chain rules, calculate the derivative of ( ( 1 + b ) ^c -u C ) , with respect to b in the disk of convergence D . We later multiply the derivative in the later binomcxplemdvsum by this derivative to show that ( ( 1 + b ) ^c C ) (with a nonnegated C ) and the later sum, since both at b = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses 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 |-> ( C _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 ) )
Assertion binomcxplemdvbinom 
|- ( ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 binomcxp.a 
 |-  ( ph -> A e. RR+ )
2 binomcxp.b 
 |-  ( ph -> B e. RR )
3 binomcxp.lt 
 |-  ( ph -> ( abs ` B ) < ( abs ` A ) )
4 binomcxp.c 
 |-  ( ph -> C e. CC )
5 binomcxplem.f 
 |-  F = ( j e. NN0 |-> ( C _Cc j ) )
6 binomcxplem.s 
 |-  S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
7 binomcxplem.r 
 |-  R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
8 binomcxplem.e 
 |-  E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
9 binomcxplem.d 
 |-  D = ( `' abs " ( 0 [,) R ) )
10 nfcv 
 |-  F/_ b `' abs
11 nfcv 
 |-  F/_ b 0
12 nfcv 
 |-  F/_ b [,)
13 nfcv 
 |-  F/_ b +
14 nfmpt1 
 |-  F/_ b ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
15 6 14 nfcxfr 
 |-  F/_ b S
16 nfcv 
 |-  F/_ b r
17 15 16 nffv 
 |-  F/_ b ( S ` r )
18 11 13 17 nfseq 
 |-  F/_ b seq 0 ( + , ( S ` r ) )
19 18 nfel1 
 |-  F/ b seq 0 ( + , ( S ` r ) ) e. dom ~~>
20 nfcv 
 |-  F/_ b RR
21 19 20 nfrabw 
 |-  F/_ b { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> }
22 nfcv 
 |-  F/_ b RR*
23 nfcv 
 |-  F/_ b <
24 21 22 23 nfsup 
 |-  F/_ b sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
25 7 24 nfcxfr 
 |-  F/_ b R
26 11 12 25 nfov 
 |-  F/_ b ( 0 [,) R )
27 10 26 nfima 
 |-  F/_ b ( `' abs " ( 0 [,) R ) )
28 9 27 nfcxfr 
 |-  F/_ b D
29 nfcv 
 |-  F/_ y D
30 nfcv 
 |-  F/_ y ( ( 1 + b ) ^c -u C )
31 nfcv 
 |-  F/_ b ( ( 1 + y ) ^c -u C )
32 oveq2 
 |-  ( b = y -> ( 1 + b ) = ( 1 + y ) )
33 32 oveq1d 
 |-  ( b = y -> ( ( 1 + b ) ^c -u C ) = ( ( 1 + y ) ^c -u C ) )
34 28 29 30 31 33 cbvmptf 
 |-  ( b e. D |-> ( ( 1 + b ) ^c -u C ) ) = ( y e. D |-> ( ( 1 + y ) ^c -u C ) )
35 34 oveq2i 
 |-  ( CC _D ( b e. D |-> ( ( 1 + b ) ^c -u C ) ) ) = ( CC _D ( y e. D |-> ( ( 1 + y ) ^c -u C ) ) )
36 cnelprrecn 
 |-  CC e. { RR , CC }
37 36 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> CC e. { RR , CC } )
38 1cnd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> 1 e. CC )
39 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
40 9 39 eqsstri 
 |-  D C_ dom abs
41 absf 
 |-  abs : CC --> RR
42 41 fdmi 
 |-  dom abs = CC
43 40 42 sseqtri 
 |-  D C_ CC
44 43 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> D C_ CC )
45 44 sselda 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> y e. CC )
46 38 45 addcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( 1 + y ) e. CC )
47 simpr 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> ( 1 + y ) e. RR )
48 1cnd 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> 1 e. CC )
49 45 adantr 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> y e. CC )
50 48 49 pncan2d 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> ( ( 1 + y ) - 1 ) = y )
51 1red 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> 1 e. RR )
52 47 51 resubcld 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> ( ( 1 + y ) - 1 ) e. RR )
53 50 52 eqeltrrd 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> y e. RR )
54 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
55 1red 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> 1 e. RR )
56 55 renegcld 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> -u 1 e. RR )
57 simpr 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> y e. RR )
58 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
59 elpreima 
 |-  ( abs Fn CC -> ( y e. ( `' abs " ( 0 [,) R ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) R ) ) ) )
60 41 58 59 mp2b 
 |-  ( y e. ( `' abs " ( 0 [,) R ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) R ) ) )
61 60 simprbi 
 |-  ( y e. ( `' abs " ( 0 [,) R ) ) -> ( abs ` y ) e. ( 0 [,) R ) )
62 61 9 eleq2s 
 |-  ( y e. D -> ( abs ` y ) e. ( 0 [,) R ) )
63 0re 
 |-  0 e. RR
64 ssrab2 
 |-  { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR
65 ressxr 
 |-  RR C_ RR*
66 64 65 sstri 
 |-  { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR*
67 supxrcl 
 |-  ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } C_ RR* -> sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
68 66 67 ax-mp 
 |-  sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < ) e. RR*
69 7 68 eqeltri 
 |-  R e. RR*
70 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` y ) e. ( 0 [,) R ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < R ) ) )
71 63 69 70 mp2an 
 |-  ( ( abs ` y ) e. ( 0 [,) R ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < R ) )
72 62 71 sylib 
 |-  ( y e. D -> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < R ) )
73 72 simp3d 
 |-  ( y e. D -> ( abs ` y ) < R )
74 73 adantl 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( abs ` y ) < R )
75 1 2 3 4 5 6 7 binomcxplemradcnv 
 |-  ( ( ph /\ -. C e. NN0 ) -> R = 1 )
76 75 adantr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> R = 1 )
77 74 76 breqtrd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( abs ` y ) < 1 )
78 77 adantr 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> ( abs ` y ) < 1 )
79 57 55 absltd 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> ( ( abs ` y ) < 1 <-> ( -u 1 < y /\ y < 1 ) ) )
80 78 79 mpbid 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> ( -u 1 < y /\ y < 1 ) )
81 80 simpld 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> -u 1 < y )
82 56 57 55 81 ltadd2dd 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> ( 1 + -u 1 ) < ( 1 + y ) )
83 54 82 eqbrtrrid 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ y e. RR ) -> 0 < ( 1 + y ) )
84 53 83 syldan 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> 0 < ( 1 + y ) )
85 47 84 elrpd 
 |-  ( ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) /\ ( 1 + y ) e. RR ) -> ( 1 + y ) e. RR+ )
86 85 ex 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( ( 1 + y ) e. RR -> ( 1 + y ) e. RR+ ) )
87 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
88 87 ellogdm 
 |-  ( ( 1 + y ) e. ( CC \ ( -oo (,] 0 ) ) <-> ( ( 1 + y ) e. CC /\ ( ( 1 + y ) e. RR -> ( 1 + y ) e. RR+ ) ) )
89 46 86 88 sylanbrc 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( 1 + y ) e. ( CC \ ( -oo (,] 0 ) ) )
90 eldifi 
 |-  ( x e. ( CC \ ( -oo (,] 0 ) ) -> x e. CC )
91 90 adantl 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. ( CC \ ( -oo (,] 0 ) ) ) -> x e. CC )
92 4 adantr 
 |-  ( ( ph /\ -. C e. NN0 ) -> C e. CC )
93 92 negcld 
 |-  ( ( ph /\ -. C e. NN0 ) -> -u C e. CC )
94 93 adantr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. ( CC \ ( -oo (,] 0 ) ) ) -> -u C e. CC )
95 91 94 cxpcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. ( CC \ ( -oo (,] 0 ) ) ) -> ( x ^c -u C ) e. CC )
96 ovexd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. ( CC \ ( -oo (,] 0 ) ) ) -> ( -u C x. ( x ^c ( -u C - 1 ) ) ) e. _V )
97 1cnd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. CC ) -> 1 e. CC )
98 simpr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. CC ) -> x e. CC )
99 97 98 addcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. CC ) -> ( 1 + x ) e. CC )
100 c0ex 
 |-  0 e. _V
101 100 a1i 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ x e. CC ) -> 0 e. _V )
102 1cnd 
 |-  ( ( ph /\ -. C e. NN0 ) -> 1 e. CC )
103 37 102 dvmptc 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
104 37 dvmptid 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
105 37 97 101 103 98 97 104 dvmptadd 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. CC |-> ( 1 + x ) ) ) = ( x e. CC |-> ( 0 + 1 ) ) )
106 0p1e1 
 |-  ( 0 + 1 ) = 1
107 106 mpteq2i 
 |-  ( x e. CC |-> ( 0 + 1 ) ) = ( x e. CC |-> 1 )
108 105 107 eqtrdi 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. CC |-> ( 1 + x ) ) ) = ( x e. CC |-> 1 ) )
109 fvex 
 |-  ( TopOpen ` CCfld ) e. _V
110 cnfldtps 
 |-  CCfld e. TopSp
111 cnfldbas 
 |-  CC = ( Base ` CCfld )
112 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
113 111 112 tpsuni 
 |-  ( CCfld e. TopSp -> CC = U. ( TopOpen ` CCfld ) )
114 110 113 ax-mp 
 |-  CC = U. ( TopOpen ` CCfld )
115 114 restid 
 |-  ( ( TopOpen ` CCfld ) e. _V -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
116 109 115 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
117 116 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
118 112 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
119 eqid 
 |-  ( abs o. - ) = ( abs o. - )
120 119 cnbl0 
 |-  ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` ( abs o. - ) ) R ) )
121 69 120 ax-mp 
 |-  ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` ( abs o. - ) ) R )
122 9 121 eqtri 
 |-  D = ( 0 ( ball ` ( abs o. - ) ) R )
123 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
124 0cn 
 |-  0 e. CC
125 112 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
126 125 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` CCfld ) )
127 123 124 69 126 mp3an 
 |-  ( 0 ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` CCfld )
128 122 127 eqeltri 
 |-  D e. ( TopOpen ` CCfld )
129 isopn3i 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ D e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` D ) = D )
130 118 128 129 mp2an 
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` D ) = D
131 130 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` D ) = D )
132 37 99 97 108 44 117 112 131 dvmptres2 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. D |-> ( 1 + x ) ) ) = ( x e. D |-> 1 ) )
133 oveq2 
 |-  ( x = y -> ( 1 + x ) = ( 1 + y ) )
134 133 cbvmptv 
 |-  ( x e. D |-> ( 1 + x ) ) = ( y e. D |-> ( 1 + y ) )
135 134 oveq2i 
 |-  ( CC _D ( x e. D |-> ( 1 + x ) ) ) = ( CC _D ( y e. D |-> ( 1 + y ) ) )
136 eqidd 
 |-  ( x = y -> 1 = 1 )
137 136 cbvmptv 
 |-  ( x e. D |-> 1 ) = ( y e. D |-> 1 )
138 132 135 137 3eqtr3g 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( y e. D |-> ( 1 + y ) ) ) = ( y e. D |-> 1 ) )
139 87 dvcncxp1 
 |-  ( -u C e. CC -> ( CC _D ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c -u C ) ) ) = ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( -u C x. ( x ^c ( -u C - 1 ) ) ) ) )
140 93 139 syl 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c -u C ) ) ) = ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( -u C x. ( x ^c ( -u C - 1 ) ) ) ) )
141 oveq1 
 |-  ( x = ( 1 + y ) -> ( x ^c -u C ) = ( ( 1 + y ) ^c -u C ) )
142 oveq1 
 |-  ( x = ( 1 + y ) -> ( x ^c ( -u C - 1 ) ) = ( ( 1 + y ) ^c ( -u C - 1 ) ) )
143 142 oveq2d 
 |-  ( x = ( 1 + y ) -> ( -u C x. ( x ^c ( -u C - 1 ) ) ) = ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) )
144 37 37 89 38 95 96 138 140 141 143 dvmptco 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( y e. D |-> ( ( 1 + y ) ^c -u C ) ) ) = ( y e. D |-> ( ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) x. 1 ) ) )
145 92 adantr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> C e. CC )
146 145 negcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> -u C e. CC )
147 146 38 subcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( -u C - 1 ) e. CC )
148 46 147 cxpcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( ( 1 + y ) ^c ( -u C - 1 ) ) e. CC )
149 146 148 mulcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) e. CC )
150 149 mulridd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ y e. D ) -> ( ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) x. 1 ) = ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) )
151 150 mpteq2dva 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( y e. D |-> ( ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) x. 1 ) ) = ( y e. D |-> ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) ) )
152 nfcv 
 |-  F/_ b ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) )
153 nfcv 
 |-  F/_ y ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) )
154 oveq2 
 |-  ( y = b -> ( 1 + y ) = ( 1 + b ) )
155 154 oveq1d 
 |-  ( y = b -> ( ( 1 + y ) ^c ( -u C - 1 ) ) = ( ( 1 + b ) ^c ( -u C - 1 ) ) )
156 155 oveq2d 
 |-  ( y = b -> ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) = ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) ) )
157 29 28 152 153 156 cbvmptf 
 |-  ( y e. D |-> ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) ) = ( b e. D |-> ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) ) )
158 157 a1i 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( y e. D |-> ( -u C x. ( ( 1 + y ) ^c ( -u C - 1 ) ) ) ) = ( b e. D |-> ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) ) ) )
159 144 151 158 3eqtrd 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( CC _D ( y e. D |-> ( ( 1 + y ) ^c -u C ) ) ) = ( b e. D |-> ( -u C x. ( ( 1 + b ) ^c ( -u C - 1 ) ) ) ) )
160 35 159 eqtrid 
 |-  ( ( 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 ) ) ) ) )