MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  logtayl Structured version   Unicode version

Theorem logtayl 22910
Description: The Taylor series for  -u log (
1  -  A ). (Contributed by Mario Carneiro, 1-Apr-2015.)
Assertion
Ref Expression
logtayl  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  seq 1 (  +  , 
( k  e.  NN  |->  ( ( A ^
k )  /  k
) ) )  ~~>  -u ( log `  ( 1  -  A ) ) )
Distinct variable group:    A, k

Proof of Theorem logtayl
Dummy variables  j  m  n  r  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 11121 . . . 4  |-  NN0  =  ( ZZ>= `  0 )
2 0zd 10879 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
0  e.  ZZ )
3 eqeq1 2445 . . . . . . . 8  |-  ( k  =  n  ->  (
k  =  0  <->  n  =  0 ) )
4 oveq2 6286 . . . . . . . 8  |-  ( k  =  n  ->  (
1  /  k )  =  ( 1  /  n ) )
53, 4ifbieq2d 3948 . . . . . . 7  |-  ( k  =  n  ->  if ( k  =  0 ,  0 ,  ( 1  /  k ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
6 oveq2 6286 . . . . . . 7  |-  ( k  =  n  ->  ( A ^ k )  =  ( A ^ n
) )
75, 6oveq12d 6296 . . . . . 6  |-  ( k  =  n  ->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
8 eqid 2441 . . . . . 6  |-  ( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) ) )  =  ( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) ) )
9 ovex 6306 . . . . . 6  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^ n ) )  e.  _V
107, 8, 9fvmpt 5938 . . . . 5  |-  ( n  e.  NN0  ->  ( ( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) ) ) `  n )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
1110adantl 466 . . . 4  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( ( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) ) ) `  n )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
12 0cnd 9589 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  n  =  0 )  ->  0  e.  CC )
13 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  n  e.  NN0 )
14 elnn0 10800 . . . . . . . . . . . 12  |-  ( n  e.  NN0  <->  ( n  e.  NN  \/  n  =  0 ) )
1513, 14sylib 196 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( n  e.  NN  \/  n  =  0 ) )
1615ord 377 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  e.  NN  ->  n  = 
0 ) )
1716con1d 124 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  =  0  ->  n  e.  NN ) )
1817imp 429 . . . . . . . 8  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  ->  n  e.  NN )
1918nnrecred 10584 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  RR )
2019recnd 9622 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  CC )
2112, 20ifclda 3955 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  CC )
22 expcl 12160 . . . . . 6  |-  ( ( A  e.  CC  /\  n  e.  NN0 )  -> 
( A ^ n
)  e.  CC )
2322adantlr 714 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( A ^
n )  e.  CC )
2421, 23mulcld 9616 . . . 4  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) )  e.  CC )
25 logtayllem 22909 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  seq 0 (  +  , 
( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k
) )  x.  ( A ^ k ) ) ) )  e.  dom  ~~>  )
261, 2, 11, 24, 25isumclim2 13549 . . 3  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  seq 0 (  +  , 
( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k
) )  x.  ( A ^ k ) ) ) )  ~~>  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
27 simpl 457 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  CC )
28 0cn 9588 . . . . . . . 8  |-  0  e.  CC
29 eqid 2441 . . . . . . . . 9  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3029cnmetdval 21148 . . . . . . . 8  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  ( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
3127, 28, 30sylancl 662 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
32 subid1 9841 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( A  -  0 )  =  A )
3332adantr 465 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  -  0 )  =  A )
3433fveq2d 5857 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  ( A  -  0 ) )  =  ( abs `  A ) )
3531, 34eqtrd 2482 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  A ) )
36 simpr 461 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  A
)  <  1 )
3735, 36eqbrtrd 4454 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  <  1 )
38 cnxmet 21150 . . . . . . 7  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
39 1rp 11230 . . . . . . . 8  |-  1  e.  RR+
40 rpxr 11233 . . . . . . . 8  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
4139, 40ax-mp 5 . . . . . . 7  |-  1  e.  RR*
42 elbl3 20765 . . . . . . 7  |-  ( ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  1  e.  RR* )  /\  ( 0  e.  CC  /\  A  e.  CC ) )  -> 
( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4338, 41, 42mpanl12 682 . . . . . 6  |-  ( ( 0  e.  CC  /\  A  e.  CC )  ->  ( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4428, 27, 43sylancr 663 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4537, 44mpbird 232 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
46 tru 1385 . . . . . 6  |- T.
47 eqid 2441 . . . . . . . 8  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )
48 0cnd 9589 . . . . . . . 8  |-  ( T. 
->  0  e.  CC )
4941a1i 11 . . . . . . . 8  |-  ( T. 
->  1  e.  RR* )
50 ax-1cn 9550 . . . . . . . . . . . . 13  |-  1  e.  CC
51 blssm 20791 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
5238, 28, 41, 51mp3an 1323 . . . . . . . . . . . . . 14  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
5352sseli 3483 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  CC )
54 subcl 9821 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  y
)  e.  CC )
5550, 53, 54sylancr 663 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  CC )
5653abscld 13243 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR )
5729cnmetdval 21148 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  /\  0  e.  CC )  ->  ( y ( abs 
o.  -  ) 0 )  =  ( abs `  ( y  -  0 ) ) )
5853, 28, 57sylancl 662 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  ( y  -  0 ) ) )
5953subid1d 9922 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  -  0 )  =  y )
6059fveq2d 5857 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( y  -  0 ) )  =  ( abs `  y ) )
6158, 60eqtrd 2482 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  y ) )
62 elbl3 20765 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  1  e.  RR* )  /\  ( 0  e.  CC  /\  y  e.  CC ) )  -> 
( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( y
( abs  o.  -  )
0 )  <  1
) )
6338, 41, 62mpanl12 682 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  CC  /\  y  e.  CC )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( y
( abs  o.  -  )
0 )  <  1
) )
6428, 53, 63sylancr 663 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <-> 
( y ( abs 
o.  -  ) 0 )  <  1 ) )
6564ibi 241 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  <  1
)
6661, 65eqbrtrrd 4456 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  1
)
6756, 66gtned 9720 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  ( abs `  y ) )
68 abs1 13106 . . . . . . . . . . . . . . . 16  |-  ( abs `  1 )  =  1
69 fveq2 5853 . . . . . . . . . . . . . . . 16  |-  ( 1  =  y  ->  ( abs `  1 )  =  ( abs `  y
) )
7068, 69syl5eqr 2496 . . . . . . . . . . . . . . 15  |-  ( 1  =  y  ->  1  =  ( abs `  y
) )
7170necon3i 2681 . . . . . . . . . . . . . 14  |-  ( 1  =/=  ( abs `  y
)  ->  1  =/=  y )
7267, 71syl 16 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  y )
73 subeq0 9847 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =  0  <->  1  =  y ) )
7473necon3bid 2699 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =/=  0  <->  1  =/=  y ) )
7550, 53, 74sylancr 663 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  -  y )  =/=  0  <->  1  =/=  y ) )
7672, 75mpbird 232 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  =/=  0 )
7755, 76logcld 22827 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  ( 1  -  y
) )  e.  CC )
7877negcld 9920 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
7978adantl 466 . . . . . . . . 9  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
80 eqid 2441 . . . . . . . . 9  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u ( log `  (
1  -  y ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) )
8179, 80fmptd 6037 . . . . . . . 8  |-  ( T. 
->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) : ( 0 (
ball `  ( abs  o. 
-  ) ) 1 ) --> CC )
8253absge0d 13251 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( abs `  y ) )
8356rexrd 9643 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR* )
84 peano2re 9753 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  y )  e.  RR  ->  (
( abs `  y
)  +  1 )  e.  RR )
8556, 84syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  +  1 )  e.  RR )
8685rehalfcld 10788 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  RR )
8786rexrd 9643 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e. 
RR* )
88 iccssxr 11613 . . . . . . . . . . . . . . 15  |-  ( 0 [,] +oo )  C_  RR*
89 eqeq1 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
m  =  0  <->  j  =  0 ) )
90 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
1  /  m )  =  ( 1  / 
j ) )
9189, 90ifbieq2d 3948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  j  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( j  =  0 ,  0 ,  ( 1  /  j ) ) )
92 eqid 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )
93 c0ex 9590 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
94 ovex 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  j )  e. 
_V
9593, 94ifex 3992 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  e.  _V
9691, 92, 95fvmpt 5938 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j )  =  if ( j  =  0 ,  0 ,  ( 1  / 
j ) ) )
9796eqcomd 2449 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j ) )
9897oveq1d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  NN0  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j )  x.  ( x ^
j ) ) )
9998mpteq2ia 4516 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) )  =  ( j  e.  NN0  |->  ( ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j
)  x.  ( x ^ j ) ) )
10099mpteq2i 4517 . . . . . . . . . . . . . . . 16  |-  ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) )  =  ( x  e.  CC  |->  ( j  e.  NN0  |->  ( ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j
)  x.  ( x ^ j ) ) ) )
101 0cnd 9589 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  m  e.  NN0 )  /\  m  =  0 )  -> 
0  e.  CC )
102 nn0cn 10808 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN0  ->  m  e.  CC )
103102adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  m  e. 
NN0 )  ->  m  e.  CC )
104 df-ne 2638 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =/=  0  <->  -.  m  =  0 )
105104biimpri 206 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  m  =  0  ->  m  =/=  0 )
106 reccl 10217 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  CC  /\  m  =/=  0 )  -> 
( 1  /  m
)  e.  CC )
107103, 105, 106syl2an 477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  m  e.  NN0 )  /\  -.  m  =  0 )  ->  ( 1  /  m )  e.  CC )
108101, 107ifclda 3955 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  m  e. 
NN0 )  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  e.  CC )
109108, 92fmptd 6037 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
110 recn 9582 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  e.  RR  ->  r  e.  CC )
111 oveq1 6285 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  r  ->  (
x ^ j )  =  ( r ^
j ) )
112111oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  r  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) )
113112mpteq2dv 4521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  r  ->  (
j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )
114 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) )  =  ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) )
115 nn0ex 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  e.  _V
116115mptex 6125 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) )  e.  _V
117113, 114, 116fvmpt 5938 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  e.  CC  ->  (
( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
x ^ j ) ) ) ) `  r )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )
118110, 117syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  RR  ->  (
( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
x ^ j ) ) ) ) `  r )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )
119118eqcomd 2449 . . . . . . . . . . . . . . . . . . . 20  |-  ( r  e.  RR  ->  (
j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) )  =  ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  r
) )
120119seqeq3d 12091 . . . . . . . . . . . . . . . . . . 19  |-  ( r  e.  RR  ->  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  =  seq 0 (  +  ,  ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  r
) ) )
121120eleq1d 2510 . . . . . . . . . . . . . . . . . 18  |-  ( r  e.  RR  ->  (  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~> 
<->  seq 0 (  +  ,  ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  r
) )  e.  dom  ~~>  ) )
122121rabbiia 3082 . . . . . . . . . . . . . . . . 17  |-  { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  }  =  { r  e.  RR  |  seq 0 (  +  , 
( ( x  e.  CC  |->  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^
j ) ) ) ) `  r ) )  e.  dom  ~~>  }
123122supeq1i 7906 . . . . . . . . . . . . . . . 16  |-  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  )  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( ( x  e.  CC  |->  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^
j ) ) ) ) `  r ) )  e.  dom  ~~>  } ,  RR* ,  <  )
124100, 109, 123radcnvcl 22681 . . . . . . . . . . . . . . 15  |-  ( T. 
->  sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  ( 0 [,] +oo ) )
12588, 124sseldi 3485 . . . . . . . . . . . . . 14  |-  ( T. 
->  sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR* )
12646, 125mp1i 12 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  )  e. 
RR* )
127 1re 9595 . . . . . . . . . . . . . . 15  |-  1  e.  RR
128 avglt1 10779 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) ) )
12956, 127, 128sylancl 662 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( abs `  y
)  <  ( (
( abs `  y
)  +  1 )  /  2 ) ) )
13066, 129mpbid 210 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) )
131 0red 9597 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  RR )
132131, 56, 86, 82, 130lelttrd 9740 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <  ( ( ( abs `  y
)  +  1 )  /  2 ) )
133131, 86, 132ltled 9733 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13486, 133absidd 13230 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  =  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13546, 109mp1i 12 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
13686recnd 9622 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  CC )
137 oveq1 6285 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( ( ( abs `  y )  +  1 )  / 
2 )  ->  (
x ^ j )  =  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) )
138137oveq2d 6294 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( ( ( abs `  y )  +  1 )  / 
2 )  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) )
139138mpteq2dv 4521 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( ( ( abs `  y )  +  1 )  / 
2 )  ->  (
j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) ) )
140115mptex 6125 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) )  e.  _V
141139, 114, 140fvmpt 5938 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( abs `  y
)  +  1 )  /  2 )  e.  CC  ->  ( (
x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  (
( ( abs `  y
)  +  1 )  /  2 ) )  =  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) ) )
142136, 141syl 16 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  (
( ( abs `  y
)  +  1 )  /  2 ) )  =  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) ) )
143142seqeq3d 12091 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  seq 0
(  +  ,  ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
x ^ j ) ) ) ) `  ( ( ( abs `  y )  +  1 )  /  2 ) ) )  =  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
( ( ( abs `  y )  +  1 )  /  2 ) ^ j ) ) ) ) )
144 avglt2 10780 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 ) )
14556, 127, 144sylancl 662 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( ( ( abs `  y )  +  1 )  / 
2 )  <  1
) )
14666, 145mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 )
147134, 146eqbrtrd 4454 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  <  1 )
148 logtayllem 22909 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( abs `  y )  +  1 )  /  2 )  e.  CC  /\  ( abs `  ( ( ( abs `  y )  +  1 )  / 
2 ) )  <  1 )  ->  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
( ( ( abs `  y )  +  1 )  /  2 ) ^ j ) ) ) )  e.  dom  ~~>  )
149136, 147, 148syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  seq 0
(  +  ,  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) ) )  e.  dom  ~~>  )
150143, 149eqeltrd 2529 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  seq 0
(  +  ,  ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
x ^ j ) ) ) ) `  ( ( ( abs `  y )  +  1 )  /  2 ) ) )  e.  dom  ~~>  )
151100, 135, 123, 136, 150radcnvle 22684 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  <_  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )
152134, 151eqbrtrrd 4456 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  <_  sup ( { r  e.  RR  |  seq 0
(  +  ,  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  )
)
15383, 87, 126, 130, 152xrltletrd 11370 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )
154 0re 9596 . . . . . . . . . . . . 13  |-  0  e.  RR
155 elico2 11594 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR  /\  sup ( { r  e.  RR  |  seq 0
(  +  ,  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  )  e.  RR* )  ->  (
( abs `  y
)  e.  ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) )  <->  ( ( abs `  y )  e.  RR  /\  0  <_  ( abs `  y )  /\  ( abs `  y )  <  sup ( { r  e.  RR  |  seq 0
(  +  ,  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  )
) ) )
156154, 126, 155sylancr 663 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  e.  ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )  <-> 
( ( abs `  y
)  e.  RR  /\  0  <_  ( abs `  y
)  /\  ( abs `  y )  <  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) )
15756, 82, 153, 156mpbir3and 1178 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )
158 absf 13146 . . . . . . . . . . . 12  |-  abs : CC
--> RR
159 ffn 5718 . . . . . . . . . . . 12  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
160 elpreima 5989 . . . . . . . . . . . 12  |-  ( abs 
Fn  CC  ->  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  <->  ( y  e.  CC  /\  ( abs `  y )  e.  ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) ) )
161158, 159, 160mp2b 10 . . . . . . . . . . 11  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  <->  ( y  e.  CC  /\  ( abs `  y )  e.  ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) )
16253, 157, 161sylanbrc 664 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) )
163 cnvimass 5344 . . . . . . . . . . . . . . . . . 18  |-  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  C_  dom  abs
164158fdmi 5723 . . . . . . . . . . . . . . . . . 18  |-  dom  abs  =  CC
165163, 164sseqtri 3519 . . . . . . . . . . . . . . . . 17  |-  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  C_  CC
166165sseli 3483 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  ->  y  e.  CC )
167 oveq1 6285 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x ^ j )  =  ( y ^
j ) )
168167oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^
j ) ) )
169168mpteq2dv 4521 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) ) )
170115mptex 6125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) )  e.  _V
171169, 114, 170fvmpt 5938 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
x ^ j ) ) ) ) `  y )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) ) )
172171adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  CC  /\  n  e.  NN0 )  -> 
( ( x  e.  CC  |->  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^
j ) ) ) ) `  y )  =  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^
j ) ) ) )
173172fveq1d 5855 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  /\  n  e.  NN0 )  -> 
( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  n )  =  ( ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) ) `  n ) )
174 eqeq1 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
j  =  0  <->  n  =  0 ) )
175 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
1  /  j )  =  ( 1  /  n ) )
176174, 175ifbieq2d 3948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
177 oveq2 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  (
y ^ j )  =  ( y ^
n ) )
178176, 177oveq12d 6296 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  n  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
179 eqid 2441 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) )  =  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) )
180 ovex 6306 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^ n ) )  e.  _V
181178, 179, 180fvmpt 5938 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  ( ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) ) `  n )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
182181adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  /\  n  e.  NN0 )  -> 
( ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^
j ) ) ) `
 n )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^ n
) ) )
183173, 182eqtr2d 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  CC  /\  n  e.  NN0 )  -> 
( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^ n
) )  =  ( ( ( x  e.  CC  |->  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^
j ) ) ) ) `  y ) `
 n ) )
184183sumeq2dv 13501 . . . . . . . . . . . . . . . 16  |-  ( y  e.  CC  ->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  = 
sum_ n  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  n )
)
185166, 184syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  ->  sum_ n  e. 
NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  = 
sum_ n  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  n )
)
186185mpteq2ia 4516 . . . . . . . . . . . . . 14  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) )  =  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  n )
)
187 eqid 2441 . . . . . . . . . . . . . 14  |-  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  =  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )
188 eqid 2441 . . . . . . . . . . . . . 14  |-  if ( sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR ,  ( ( ( abs `  z
)  +  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )  /  2 ) ,  ( ( abs `  z
)  +  1 ) )  =  if ( sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR ,  ( ( ( abs `  z
)  +  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )  /  2 ) ,  ( ( abs `  z
)  +  1 ) )
189100, 186, 109, 123, 187, 188psercn 22690 . . . . . . . . . . . . 13  |-  ( T. 
->  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )  e.  ( ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) -cn-> CC ) )
190 cncff 21267 . . . . . . . . . . . . 13  |-  ( ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )  e.  ( ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) -cn-> CC )  ->  ( y  e.  ( `' abs " (
0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) --> CC )
191189, 190syl 16 . . . . . . . . . . . 12  |-  ( T. 
->  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) ) : ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) --> CC )
192 eqid 2441 . . . . . . . . . . . . 13  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) )  =  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
193192fmpt 6034 . . . . . . . . . . . 12  |-  ( A. y  e.  ( `' abs " ( 0 [,)
sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC  <->  ( y  e.  ( `' abs " (
0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) --> CC )
194191, 193sylibr 212 . . . . . . . . . . 11  |-  ( T. 
->  A. y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) ) sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC )
195194r19.21bi 2810 . . . . . . . . . 10  |-  ( ( T.  /\  y  e.  ( `' abs " (
0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) )  ->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC )
196162, 195sylan2 474 . . . . . . . . 9  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  sum_ n  e. 
NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC )
197 eqid 2441 . . . . . . . . 9  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
198196, 197fmptd 6037 . . . . . . . 8  |-  ( T. 
->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) ) : ( 0 (
ball `  ( abs  o. 
-  ) ) 1 ) --> CC )
199 cnelprrecn 9585 . . . . . . . . . . . . 13  |-  CC  e.  { RR ,  CC }
200199a1i 11 . . . . . . . . . . . 12  |-  ( T. 
->  CC  e.  { RR ,  CC } )
20177adantl 466 . . . . . . . . . . . 12  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  ( 1  -  y
) )  e.  CC )
202 ovex 6306 . . . . . . . . . . . . 13  |-  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V
203202a1i 11 . . . . . . . . . . . 12  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V )
20429cnmetdval 21148 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  ( 1  -  y
)  e.  CC )  ->  ( 1 ( abs  o.  -  )
( 1  -  y
) )  =  ( abs `  ( 1  -  ( 1  -  y ) ) ) )
20550, 55, 204sylancr 663 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  (
1  -  ( 1  -  y ) ) ) )
206 nncan 9850 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  (
1  -  y ) )  =  y )
20750, 53, 206sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  ( 1  -  y ) )  =  y )
208207fveq2d 5857 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( 1  -  (
1  -  y ) ) )  =  ( abs `  y ) )
209205, 208eqtrd 2482 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  y
) )
210209, 66eqbrtrd 4454 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 )
211 elbl 20761 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  1  e.  CC  /\  1  e.  RR* )  ->  (
( 1  -  y
)  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( (
1  -  y )  e.  CC  /\  (
1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 ) ) )
21238, 50, 41, 211mp3an 1323 . . . . . . . . . . . . . . 15  |-  ( ( 1  -  y )  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  <->  ( ( 1  -  y )  e.  CC  /\  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 ) )
21355, 210, 212sylanbrc 664 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
214213adantl 466 . . . . . . . . . . . . 13  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
215 neg1cn 10642 . . . . . . . . . . . . . 14  |-  -u 1  e.  CC
216215a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u 1  e.  CC )
217 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
218217dvlog2lem 22902 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  ( -oo (,] 0 ) )
219218sseli 3483 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  ( CC  \  ( -oo (,] 0 ) ) )
220219eldifad 3471 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  CC )
221 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( CC 
\  ( -oo (,] 0 ) )  =  ( CC  \  ( -oo (,] 0 ) )
222221logdmn0 22890 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( CC  \ 
( -oo (,] 0 ) )  ->  x  =/=  0 )
223219, 222syl 16 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  =/=  0 )
224220, 223logcld 22827 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  x )  e.  CC )
225224adantl 466 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  x )  e.  CC )
226 ovex 6306 . . . . . . . . . . . . . 14  |-  ( 1  /  x )  e. 
_V
227226a1i 11 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  /  x )  e. 
_V )
228 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  y  e.  CC )  ->  y  e.  CC )
22950, 228, 54sylancr 663 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  y  e.  CC )  ->  (
1  -  y )  e.  CC )
230215a1i 11 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  y  e.  CC )  ->  -u 1  e.  CC )
231 1cnd 9612 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  y  e.  CC )  ->  1  e.  CC )
232 0cnd 9589 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  y  e.  CC )  ->  0  e.  CC )
233 1cnd 9612 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  1  e.  CC )
234200, 233dvmptc 22231 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( CC  _D  (
y  e.  CC  |->  1 ) )  =  ( y  e.  CC  |->  0 ) )
235200dvmptid 22230 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( CC  _D  (
y  e.  CC  |->  y ) )  =  ( y  e.  CC  |->  1 ) )
236200, 231, 232, 234, 228, 231, 235dvmptsub 22240 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  ( 0  -  1 ) ) )
237 df-neg 9810 . . . . . . . . . . . . . . . 16  |-  -u 1  =  ( 0  -  1 )
238237mpteq2i 4517 . . . . . . . . . . . . . . 15  |-  ( y  e.  CC  |->  -u 1
)  =  ( y  e.  CC  |->  ( 0  -  1 ) )
239236, 238syl6eqr 2500 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  -u
1 ) )
24052a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
C_  CC )
241 eqid 2441 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
242241cnfldtop 21161 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  e.  Top
243241cnfldtopon 21160 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
244243toponunii 19303 . . . . . . . . . . . . . . . . 17  |-  CC  =  U. ( TopOpen ` fld )
245244restid 14705 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
246242, 245ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
247246eqcomi 2454 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
248241cnfldtopn 21159 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
249248blopn 20873 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld ) )
25038, 28, 41, 249mp3an 1323 . . . . . . . . . . . . . . 15  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld )
251250a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  ( TopOpen ` fld ) )
252200, 229, 230, 239, 240, 247, 241, 251dvmptres 22236 . . . . . . . . . . . . 13  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  -  y ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u 1 ) )
253217dvlog2 22903 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) )
254 logf1o 22821 . . . . . . . . . . . . . . . . . . . 20  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
255 f1of 5803 . . . . . . . . . . . . . . . . . . . 20  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
256254, 255ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  log :
( CC  \  {
0 } ) --> ran 
log
257221logdmss 22892 . . . . . . . . . . . . . . . . . . . 20  |-  ( CC 
\  ( -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
258218, 257sstri 3496 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
259 fssres 5738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( log : ( CC 
\  { 0 } ) --> ran  log  /\  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } ) )  ->  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log )
260256, 258, 259mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log
261260a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log )
262261feqmptd 5908 . . . . . . . . . . . . . . . 16  |-  ( T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) ) )
263 fvres 5867 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  x
)  =  ( log `  x ) )
264263mpteq2ia 4516 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) )  =  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( log `  x
) )
265262, 264syl6eq 2498 . . . . . . . . . . . . . . 15  |-  ( T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )
266265oveq2d 6294 . . . . . . . . . . . . . 14  |-  ( T. 
->  ( CC  _D  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) )  =  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) ) )
267253, 266syl5reqr 2497 . . . . . . . . . . . . 13  |-  ( T. 
->  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) ) )
268 fveq2 5853 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  ( log `  x )  =  ( log `  (
1  -  y ) ) )
269 oveq2 6286 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  (
1  /  x )  =  ( 1  / 
( 1  -  y
) ) )
270200, 200, 214, 216, 225, 227, 252, 267, 268, 269dvmptco 22245 . . . . . . . . . . . 12  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  ( 1  -  y
) ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( ( 1  / 
( 1  -  y
) )  x.  -u 1
) ) )
271200, 201, 203, 270dvmptneg 22239 . . . . . . . . . . 11  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 ) ) )
27255, 76reccld 10316 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e.  CC )
273 mulcom 9578 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  /  (
1  -  y ) )  e.  CC  /\  -u 1  e.  CC )  ->  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
274272, 215, 273sylancl 662 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
275272mulm1d 10011 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( -u 1  x.  ( 1  /  (
1  -  y ) ) )  =  -u ( 1  /  (
1  -  y ) ) )
276274, 275eqtrd 2482 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u ( 1  / 
( 1  -  y
) ) )
277276negeqd 9816 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u -u ( 1  / 
( 1  -  y
) ) )
278272negnegd 9924 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u -u (
1  /  ( 1  -  y ) )  =  ( 1  / 
( 1  -  y
) ) )
279277, 278eqtrd 2482 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( 1  /  (
1  -  y ) ) )
280279mpteq2ia 4516 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  (
1  -  y ) ) )
281271, 280syl6eq 2498 . . . . . . . . . 10  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( 1  / 
( 1  -  y
) ) ) )
282281dmeqd 5192 . . . . . . . . 9  |-  ( T. 
->  dom  ( CC  _D  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  dom  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  ( 1  -  y ) ) ) )
283 dmmptg 5491 . . . . . . . . . 10  |-  ( A. y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) ( 1  /  ( 1  -  y ) )  e. 
_V  ->  dom  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  (
1  -  y ) ) )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
284 ovex 6306 . . . . . . . . . . 11  |-  ( 1  /  ( 1  -  y ) )  e. 
_V
285284a1i 11 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e. 
_V )
286283, 285mprg 2804 . . . . . . . . 9  |-  dom  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  ( 1  -  y ) ) )  =  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )
287282, 286syl6eq 2498 . . . . . . . 8  |-  ( T. 
->  dom  ( CC  _D  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
288 sumex 13486 . . . . . . . . . . . 12  |-  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  e.  _V
289288a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  y  e.  ( `' abs " (
0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) )  ->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  e.  _V )
290 fveq2 5853 . . . . . . . . . . . . . . 15  |-  ( n  =  k  ->  (
( ( x  e.  CC  |->  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^
j ) ) ) ) `  y ) `
 n )  =  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  k )
)
291290cbvsumv 13494 . . . . . . . . . . . . . 14  |-  sum_ n  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  n )  =  sum_ k  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  k )
292185, 291syl6eq 2498 . . . . . . . . . . . . 13  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  ->  sum_ n  e. 
NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  = 
sum_ k  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  k )
)
293292mpteq2ia 4516 . . . . . . . . . . . 12  |-  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) )  =  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ k  e.  NN0  ( ( ( x  e.  CC  |->  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) ) ) ) `  y
) `  k )
)
294 eqid 2441 . . . . . . . . . . . 12  |-  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  z )  +  if ( sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR ,  ( ( ( abs `  z
)  +  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )  /  2 ) ,  ( ( abs `  z
)  +  1 ) ) )  /  2
) )  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( ( ( abs `  z )  +  if ( sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  )  e.  RR ,  ( ( ( abs `  z
)  +  sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) )  /  2 ) ,  ( ( abs `  z
)  +  1 ) ) )  /  2
) )
295100, 293, 109, 123, 187, 188, 294pserdv2 22694 . . . . . . . . . . 11  |-  ( T. 
->  ( CC  _D  (
y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) ) )  =  ( y  e.  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) )  |->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e. 
NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `
 n ) )  x.  ( y ^
( n  -  1 ) ) ) ) )
296162ssriv 3491 . . . . . . . . . . . 12  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  , 
( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j
) )  x.  (
r ^ j ) ) ) )  e. 
dom 
~~>  } ,  RR* ,  <  ) ) )
297296a1i 11 . . . . . . . . . . 11  |-  ( T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
C_  ( `' abs " ( 0 [,) sup ( { r  e.  RR  |  seq 0 (  +  ,  ( j  e. 
NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) ) )  e.  dom  ~~>  } ,  RR* ,  <  ) ) ) )
298200, 195, 289, 295, 297, 247, 241, 251dvmptres 22236 . . . . . . . . . 10  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e. 
NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `
 n ) )  x.  ( y ^
( n  -  1 ) ) ) ) )
299 nnnn0 10805 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  NN0 )
300299adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  NN0 )
301 eqeq1 2445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
m  =  0  <->  n  =  0 ) )
302 oveq2 6286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
1  /  m )  =  ( 1  /  n ) )
303301, 302ifbieq2d 3948 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
304 ovex 6306 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  n )  e. 
_V
30593, 304ifex 3992 . . . . . . . . . . . . . . . . . . . 20  |-  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  _V
306303, 92, 305fvmpt 5938 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
307300, 306syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
)  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
308 nnne0 10571 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  n  =/=  0 )
309308adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  =/=  0 )
310309neneqd 2643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  -.  n  =  0 )
311310iffalsed 3934 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  =  ( 1  /  n ) )
312307, 311eqtrd 2482 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
)  =  ( 1  /  n ) )
313312oveq2d 6294 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  =  ( n  x.  ( 1  /  n ) ) )
314 nncn 10547 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  n  e.  CC )
315314adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  CC )
316315, 309recidd 10318 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( 1  /  n ) )  =  1 )
317313, 316eqtrd 2482 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  =  1 )
318317oveq1d 6293 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( n  x.  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
) )  x.  (
y ^ ( n  -  1 ) ) )  =  ( 1  x.  ( y ^
( n  -  1 ) ) ) )
319 nnm1nn0 10840 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  (
n  -  1 )  e.  NN0 )
320 expcl 12160 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  CC  /\  ( n  -  1
)  e.  NN0 )  ->  ( y ^ (
n  -  1 ) )  e.  CC )
32153, 319, 320syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
y ^ ( n  -  1 ) )  e.  CC )
322321mulid2d 9614 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
1  x.  ( y ^ ( n  - 
1 ) ) )  =  ( y ^
( n  -  1 ) ) )
323318, 322eqtrd 2482 . . . . . . . . . . . . 13  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( n  x.  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
) )  x.  (
y ^ ( n  -  1 ) ) )  =  ( y ^ ( n  - 
1 ) ) )
324323sumeq2dv 13501 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  =  sum_ n  e.  NN  ( y ^ (
n  -  1 ) ) )
325 nnuz 11122 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
326 1e0p1 11009 . . . . . . . . . . . . . . . 16  |-  1  =  ( 0  +  1 )
327326fveq2i 5856 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
328325, 327eqtri 2470 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
329 oveq1 6285 . . . . . . . . . . . . . . 15  |-  ( n  =  ( 1  +  m )  ->  (
n  -  1 )  =  ( ( 1  +  m )  - 
1 ) )
330329oveq2d 6294 . . . . . . . . . . . . . 14  |-  ( n  =  ( 1  +  m )  ->  (
y ^ ( n  -  1 ) )  =  ( y ^
( ( 1  +  m )  -  1 ) ) )
331 1zzd 10898 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  e.  ZZ )
332 0zd 10879 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  ZZ )
3331, 328, 330, 331, 332, 321isumshft 13627 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ ( ( 1  +  m )  - 
1 ) ) )
334 pncan2 9829 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  m  e.  CC )  ->  ( ( 1  +  m )  -  1 )  =  m )
33550, 102, 334sylancr 663 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( 1  +  m )  -  1 )  =  m )
336335oveq2d 6294 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( y ^ ( ( 1  +  m )  - 
1 ) )  =  ( y ^ m
) )
337336sumeq2i 13497 . . . . . . . . . . . . 13  |-  sum_ m  e.  NN0  ( y ^
( ( 1  +  m )  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m )
338333, 337syl6eq 2498 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m ) )
339 geoisum 13662 . . . . . . . . . . . . 13  |-  ( ( y  e.  CC  /\  ( abs `  y )  <  1 )  ->  sum_ m  e.  NN0  (
y ^ m )  =  ( 1  / 
( 1  -  y
) ) )
34053, 66, 339syl2anc 661 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ m  e. 
NN0  ( y ^
m )  =  ( 1  /  ( 1  -  y ) ) )
341324, 338, 3403eqtrd 2486 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  =  ( 1  / 
( 1  -  y
) ) )
342341mpteq2ia 4516 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e. 
NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `
 n ) )  x.  ( y ^
( n  -  1 ) ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  (
1  -  y ) ) )
343298, 342syl6eq 2498 . . . . . . . . 9  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( 1  / 
( 1  -  y
) ) ) )
344281, 343eqtr4d 2485 . . . . . . . 8  |-  ( T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( CC 
_D  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  sum_ n  e.  NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n
) )  x.  (
y ^ n ) ) ) ) )
345 blcntr 20786 . . . . . . . . . 10  |-  ( ( (