Metamath Proof Explorer

Theorem binomcxplemdvsum

Description: Lemma for binomcxp . The derivative of the generalized sum in binomcxplemnn0 . Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (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 ) )
binomcxplem.p 
|- P = ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) )
Assertion binomcxplemdvsum 
|- ( ph -> ( CC _D P ) = ( b e. D |-> sum_ k e. NN ( ( E ` b ) ` k ) ) )

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 binomcxplem.p 
 |-  P = ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) )
11 nfcv 
 |-  F/_ b `' abs
12 nfcv 
 |-  F/_ b 0
13 nfcv 
 |-  F/_ b [,)
14 nfcv 
 |-  F/_ b +
15 nfmpt1 
 |-  F/_ b ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
16 6 15 nfcxfr 
 |-  F/_ b S
17 nfcv 
 |-  F/_ b r
18 16 17 nffv 
 |-  F/_ b ( S ` r )
19 12 14 18 nfseq 
 |-  F/_ b seq 0 ( + , ( S ` r ) )
20 19 nfel1 
 |-  F/ b seq 0 ( + , ( S ` r ) ) e. dom ~~>
21 nfcv 
 |-  F/_ b RR
22 20 21 nfrabw 
 |-  F/_ b { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> }
23 nfcv 
 |-  F/_ b RR*
24 nfcv 
 |-  F/_ b <
25 22 23 24 nfsup 
 |-  F/_ b sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
26 7 25 nfcxfr 
 |-  F/_ b R
27 12 13 26 nfov 
 |-  F/_ b ( 0 [,) R )
28 11 27 nfima 
 |-  F/_ b ( `' abs " ( 0 [,) R ) )
29 9 28 nfcxfr 
 |-  F/_ b D
30 nfcv 
 |-  F/_ y D
31 nfcv 
 |-  F/_ y sum_ k e. NN0 ( ( S ` b ) ` k )
32 nfcv 
 |-  F/_ b NN0
33 nfcv 
 |-  F/_ b y
34 16 33 nffv 
 |-  F/_ b ( S ` y )
35 nfcv 
 |-  F/_ b m
36 34 35 nffv 
 |-  F/_ b ( ( S ` y ) ` m )
37 32 36 nfsum 
 |-  F/_ b sum_ m e. NN0 ( ( S ` y ) ` m )
38 simpl 
 |-  ( ( b = y /\ k e. NN0 ) -> b = y )
39 38 fveq2d 
 |-  ( ( b = y /\ k e. NN0 ) -> ( S ` b ) = ( S ` y ) )
40 39 fveq1d 
 |-  ( ( b = y /\ k e. NN0 ) -> ( ( S ` b ) ` k ) = ( ( S ` y ) ` k ) )
41 40 sumeq2dv 
 |-  ( b = y -> sum_ k e. NN0 ( ( S ` b ) ` k ) = sum_ k e. NN0 ( ( S ` y ) ` k ) )
42 nfcv 
 |-  F/_ m ( ( S ` y ) ` k )
43 nfcv 
 |-  F/_ k CC
44 nfmpt1 
 |-  F/_ k ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) )
45 43 44 nfmpt 
 |-  F/_ k ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
46 6 45 nfcxfr 
 |-  F/_ k S
47 nfcv 
 |-  F/_ k y
48 46 47 nffv 
 |-  F/_ k ( S ` y )
49 nfcv 
 |-  F/_ k m
50 48 49 nffv 
 |-  F/_ k ( ( S ` y ) ` m )
51 fveq2 
 |-  ( k = m -> ( ( S ` y ) ` k ) = ( ( S ` y ) ` m ) )
52 42 50 51 cbvsumi 
 |-  sum_ k e. NN0 ( ( S ` y ) ` k ) = sum_ m e. NN0 ( ( S ` y ) ` m )
53 41 52 eqtrdi 
 |-  ( b = y -> sum_ k e. NN0 ( ( S ` b ) ` k ) = sum_ m e. NN0 ( ( S ` y ) ` m ) )
54 29 30 31 37 53 cbvmptf 
 |-  ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) ) = ( y e. D |-> sum_ m e. NN0 ( ( S ` y ) ` m ) )
55 10 54 eqtri 
 |-  P = ( y e. D |-> sum_ m e. NN0 ( ( S ` y ) ` m ) )
56 ovexd 
 |-  ( ( ph /\ j e. NN0 ) -> ( C _Cc j ) e. _V )
57 5 a1i 
 |-  ( ph -> F = ( j e. NN0 |-> ( C _Cc j ) ) )
58 5 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> F = ( j e. NN0 |-> ( C _Cc j ) ) )
59 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> j = k )
60 59 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( C _Cc j ) = ( C _Cc k ) )
61 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
62 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> C e. CC )
63 62 61 bcccl 
 |-  ( ( ph /\ k e. NN0 ) -> ( C _Cc k ) e. CC )
64 58 60 61 63 fvmptd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( C _Cc k ) )
65 64 63 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
66 56 57 65 fmpt2d 
 |-  ( ph -> F : NN0 --> CC )
67 nfcv 
 |-  F/_ r RR
68 nfcv 
 |-  F/_ z RR
69 nfv 
 |-  F/ z seq 0 ( + , ( S ` r ) ) e. dom ~~>
70 nfcv 
 |-  F/_ r 0
71 nfcv 
 |-  F/_ r +
72 nfcv 
 |-  F/_ r ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
73 6 72 nfcxfr 
 |-  F/_ r S
74 nfcv 
 |-  F/_ r z
75 73 74 nffv 
 |-  F/_ r ( S ` z )
76 70 71 75 nfseq 
 |-  F/_ r seq 0 ( + , ( S ` z ) )
77 76 nfel1 
 |-  F/ r seq 0 ( + , ( S ` z ) ) e. dom ~~>
78 fveq2 
 |-  ( r = z -> ( S ` r ) = ( S ` z ) )
79 78 seqeq3d 
 |-  ( r = z -> seq 0 ( + , ( S ` r ) ) = seq 0 ( + , ( S ` z ) ) )
80 79 eleq1d 
 |-  ( r = z -> ( seq 0 ( + , ( S ` r ) ) e. dom ~~> <-> seq 0 ( + , ( S ` z ) ) e. dom ~~> ) )
81 67 68 69 77 80 cbvrabw 
 |-  { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } = { z e. RR | seq 0 ( + , ( S ` z ) ) e. dom ~~> }
82 81 supeq1i 
 |-  sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { z e. RR | seq 0 ( + , ( S ` z ) ) e. dom ~~> } , RR* , < )
83 7 82 eqtri 
 |-  R = sup ( { z e. RR | seq 0 ( + , ( S ` z ) ) e. dom ~~> } , RR* , < )
84 6 fveq1i 
 |-  ( S ` z ) = ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z )
85 seqeq3 
 |-  ( ( S ` z ) = ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) -> seq 0 ( + , ( S ` z ) ) = seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) )
86 84 85 ax-mp 
 |-  seq 0 ( + , ( S ` z ) ) = seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) )
87 86 eleq1i 
 |-  ( seq 0 ( + , ( S ` z ) ) e. dom ~~> <-> seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> )
88 87 rabbii 
 |-  { z e. RR | seq 0 ( + , ( S ` z ) ) e. dom ~~> } = { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> }
89 88 supeq1i 
 |-  sup ( { z e. RR | seq 0 ( + , ( S ` z ) ) e. dom ~~> } , RR* , < ) = sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < )
90 7 82 89 3eqtrri 
 |-  sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) = R
91 90 eleq1i 
 |-  ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR <-> R e. RR )
92 90 oveq2i 
 |-  ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) = ( ( abs ` x ) + R )
93 92 oveq1i 
 |-  ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) = ( ( ( abs ` x ) + R ) / 2 )
94 eqid 
 |-  ( ( abs ` x ) + 1 ) = ( ( abs ` x ) + 1 )
95 91 93 94 ifbieq12i 
 |-  if ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) = if ( R e. RR , ( ( ( abs ` x ) + R ) / 2 ) , ( ( abs ` x ) + 1 ) )
96 oveq1 
 |-  ( w = b -> ( w ^ k ) = ( b ^ k ) )
97 96 oveq2d 
 |-  ( w = b -> ( ( F ` k ) x. ( w ^ k ) ) = ( ( F ` k ) x. ( b ^ k ) ) )
98 97 mpteq2dv 
 |-  ( w = b -> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) = ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
99 98 cbvmptv 
 |-  ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
100 99 fveq1i 
 |-  ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) = ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z )
101 seqeq3 
 |-  ( ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) = ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) -> seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) = seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) )
102 100 101 ax-mp 
 |-  seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) = seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) )
103 102 eleq1i 
 |-  ( seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> <-> seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> )
104 103 rabbii 
 |-  { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } = { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> }
105 104 supeq1i 
 |-  sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) = sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < )
106 105 eleq1i 
 |-  ( sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR <-> sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR )
107 105 oveq2i 
 |-  ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) = ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) )
108 107 oveq1i 
 |-  ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) = ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 )
109 106 108 94 ifbieq12i 
 |-  if ( sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) = if ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) )
110 109 oveq2i 
 |-  ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) ) = ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) )
111 110 oveq1i 
 |-  ( ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) ) / 2 ) = ( ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) ) / 2 )
112 111 oveq2i 
 |-  ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( w e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( w ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` x ) + if ( sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` x ) + sup ( { z e. RR | seq 0 ( + , ( ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) ) ` z ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` x ) + 1 ) ) ) / 2 ) )
113 6 55 66 83 9 95 112 pserdv2 
 |-  ( ph -> ( CC _D P ) = ( y e. D |-> sum_ n e. NN ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
114 cnvimass 
 |-  ( `' abs " ( 0 [,) R ) ) C_ dom abs
115 9 114 eqsstri 
 |-  D C_ dom abs
116 absf 
 |-  abs : CC --> RR
117 116 fdmi 
 |-  dom abs = CC
118 115 117 sseqtri 
 |-  D C_ CC
119 118 sseli 
 |-  ( y e. D -> y e. CC )
120 8 a1i 
 |-  ( ( ph /\ y e. CC ) -> E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) ) )
121 simplr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ b = y ) /\ k e. NN ) -> b = y )
122 121 oveq1d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ b = y ) /\ k e. NN ) -> ( b ^ ( k - 1 ) ) = ( y ^ ( k - 1 ) ) )
123 122 oveq2d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ b = y ) /\ k e. NN ) -> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) = ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) )
124 123 mpteq2dva 
 |-  ( ( ( ph /\ y e. CC ) /\ b = y ) -> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )
125 simpr 
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
126 nnex 
 |-  NN e. _V
127 126 mptex 
 |-  ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) e. _V
128 127 a1i 
 |-  ( ( ph /\ y e. CC ) -> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) e. _V )
129 120 124 125 128 fvmptd 
 |-  ( ( ph /\ y e. CC ) -> ( E ` y ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )
130 129 adantr 
 |-  ( ( ( ph /\ y e. CC ) /\ n e. NN ) -> ( E ` y ) = ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) ) )
131 simpr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> k = n )
132 131 fveq2d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> ( F ` k ) = ( F ` n ) )
133 131 132 oveq12d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> ( k x. ( F ` k ) ) = ( n x. ( F ` n ) ) )
134 131 oveq1d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> ( k - 1 ) = ( n - 1 ) )
135 134 oveq2d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> ( y ^ ( k - 1 ) ) = ( y ^ ( n - 1 ) ) )
136 133 135 oveq12d 
 |-  ( ( ( ( ph /\ y e. CC ) /\ n e. NN ) /\ k = n ) -> ( ( k x. ( F ` k ) ) x. ( y ^ ( k - 1 ) ) ) = ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) )
137 simpr 
 |-  ( ( ( ph /\ y e. CC ) /\ n e. NN ) -> n e. NN )
138 ovexd 
 |-  ( ( ( ph /\ y e. CC ) /\ n e. NN ) -> ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V )
139 130 136 137 138 fvmptd 
 |-  ( ( ( ph /\ y e. CC ) /\ n e. NN ) -> ( ( E ` y ) ` n ) = ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) )
140 139 sumeq2dv 
 |-  ( ( ph /\ y e. CC ) -> sum_ n e. NN ( ( E ` y ) ` n ) = sum_ n e. NN ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) )
141 119 140 sylan2 
 |-  ( ( ph /\ y e. D ) -> sum_ n e. NN ( ( E ` y ) ` n ) = sum_ n e. NN ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) )
142 141 mpteq2dva 
 |-  ( ph -> ( y e. D |-> sum_ n e. NN ( ( E ` y ) ` n ) ) = ( y e. D |-> sum_ n e. NN ( ( n x. ( F ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
143 113 142 eqtr4d 
 |-  ( ph -> ( CC _D P ) = ( y e. D |-> sum_ n e. NN ( ( E ` y ) ` n ) ) )
144 nfcv 
 |-  F/_ b NN
145 nfmpt1 
 |-  F/_ b ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
146 8 145 nfcxfr 
 |-  F/_ b E
147 146 33 nffv 
 |-  F/_ b ( E ` y )
148 nfcv 
 |-  F/_ b n
149 147 148 nffv 
 |-  F/_ b ( ( E ` y ) ` n )
150 144 149 nfsum 
 |-  F/_ b sum_ n e. NN ( ( E ` y ) ` n )
151 nfcv 
 |-  F/_ y sum_ k e. NN ( ( E ` b ) ` k )
152 simpl 
 |-  ( ( y = b /\ n e. NN ) -> y = b )
153 152 fveq2d 
 |-  ( ( y = b /\ n e. NN ) -> ( E ` y ) = ( E ` b ) )
154 153 fveq1d 
 |-  ( ( y = b /\ n e. NN ) -> ( ( E ` y ) ` n ) = ( ( E ` b ) ` n ) )
155 154 sumeq2dv 
 |-  ( y = b -> sum_ n e. NN ( ( E ` y ) ` n ) = sum_ n e. NN ( ( E ` b ) ` n ) )
156 nfmpt1 
 |-  F/_ k ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) )
157 43 156 nfmpt 
 |-  F/_ k ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
158 8 157 nfcxfr 
 |-  F/_ k E
159 nfcv 
 |-  F/_ k b
160 158 159 nffv 
 |-  F/_ k ( E ` b )
161 nfcv 
 |-  F/_ k n
162 160 161 nffv 
 |-  F/_ k ( ( E ` b ) ` n )
163 nfcv 
 |-  F/_ n ( ( E ` b ) ` k )
164 fveq2 
 |-  ( n = k -> ( ( E ` b ) ` n ) = ( ( E ` b ) ` k ) )
165 162 163 164 cbvsumi 
 |-  sum_ n e. NN ( ( E ` b ) ` n ) = sum_ k e. NN ( ( E ` b ) ` k )
166 155 165 eqtrdi 
 |-  ( y = b -> sum_ n e. NN ( ( E ` y ) ` n ) = sum_ k e. NN ( ( E ` b ) ` k ) )
167 30 29 150 151 166 cbvmptf 
 |-  ( y e. D |-> sum_ n e. NN ( ( E ` y ) ` n ) ) = ( b e. D |-> sum_ k e. NN ( ( E ` b ) ` k ) )
168 143 167 eqtrdi 
 |-  ( ph -> ( CC _D P ) = ( b e. D |-> sum_ k e. NN ( ( E ` b ) ` k ) ) )