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

Theorem logtayl 20504
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 10476 . . . 4  |-  NN0  =  ( ZZ>= `  0 )
2 0z 10249 . . . . 5  |-  0  e.  ZZ
32a1i 11 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
0  e.  ZZ )
4 eqeq1 2410 . . . . . . . 8  |-  ( k  =  n  ->  (
k  =  0  <->  n  =  0 ) )
5 oveq2 6048 . . . . . . . 8  |-  ( k  =  n  ->  (
1  /  k )  =  ( 1  /  n ) )
64, 5ifbieq2d 3719 . . . . . . 7  |-  ( k  =  n  ->  if ( k  =  0 ,  0 ,  ( 1  /  k ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
7 oveq2 6048 . . . . . . 7  |-  ( k  =  n  ->  ( A ^ k )  =  ( A ^ n
) )
86, 7oveq12d 6058 . . . . . 6  |-  ( k  =  n  ->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
9 eqid 2404 . . . . . 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 ) ) )
10 ovex 6065 . . . . . 6  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^ n ) )  e.  _V
118, 9, 10fvmpt 5765 . . . . 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 ) ) )
1211adantl 453 . . . 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 ) ) )
13 0cn 9040 . . . . . . 7  |-  0  e.  CC
1413a1i 11 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  n  =  0 )  ->  0  e.  CC )
15 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  n  e.  NN0 )
16 elnn0 10179 . . . . . . . . . . . 12  |-  ( n  e.  NN0  <->  ( n  e.  NN  \/  n  =  0 ) )
1715, 16sylib 189 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( n  e.  NN  \/  n  =  0 ) )
1817ord 367 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  e.  NN  ->  n  = 
0 ) )
1918con1d 118 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  =  0  ->  n  e.  NN ) )
2019imp 419 . . . . . . . 8  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  ->  n  e.  NN )
2120nnrecred 10001 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  RR )
2221recnd 9070 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  CC )
2314, 22ifclda 3726 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  CC )
24 expcl 11354 . . . . . 6  |-  ( ( A  e.  CC  /\  n  e.  NN0 )  -> 
( A ^ n
)  e.  CC )
2524adantlr 696 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( A ^
n )  e.  CC )
2623, 25mulcld 9064 . . . 4  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) )  e.  CC )
27 logtayllem 20503 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  seq  0 (  +  , 
( k  e.  NN0  |->  ( if ( k  =  0 ,  0 ,  ( 1  /  k
) )  x.  ( A ^ k ) ) ) )  e.  dom  ~~>  )
281, 3, 12, 26, 27isumclim2 12497 . . 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 ) ) )
29 simpl 444 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  CC )
30 eqid 2404 . . . . . . . . 9  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3130cnmetdval 18758 . . . . . . . 8  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  ( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
3229, 13, 31sylancl 644 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
33 subid1 9278 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( A  -  0 )  =  A )
3433adantr 452 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  -  0 )  =  A )
3534fveq2d 5691 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  ( A  -  0 ) )  =  ( abs `  A ) )
3632, 35eqtrd 2436 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  A ) )
37 simpr 448 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  A
)  <  1 )
3836, 37eqbrtrd 4192 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  <  1 )
39 cnxmet 18760 . . . . . . 7  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
40 1rp 10572 . . . . . . . 8  |-  1  e.  RR+
41 rpxr 10575 . . . . . . . 8  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
4240, 41ax-mp 8 . . . . . . 7  |-  1  e.  RR*
43 elbl3 18375 . . . . . . 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
) )
4439, 42, 43mpanl12 664 . . . . . 6  |-  ( ( 0  e.  CC  /\  A  e.  CC )  ->  ( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4513, 29, 44sylancr 645 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4638, 45mpbird 224 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
47 tru 1327 . . . . . 6  |-  T.
48 eqid 2404 . . . . . . . 8  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )
4913a1i 11 . . . . . . . 8  |-  (  T. 
->  0  e.  CC )
5042a1i 11 . . . . . . . 8  |-  (  T. 
->  1  e.  RR* )
51 ax-1cn 9004 . . . . . . . . . . . . 13  |-  1  e.  CC
52 blssm 18401 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
5339, 13, 42, 52mp3an 1279 . . . . . . . . . . . . . 14  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
5453sseli 3304 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  CC )
55 subcl 9261 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  y
)  e.  CC )
5651, 54, 55sylancr 645 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  CC )
5754abscld 12193 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR )
5830cnmetdval 18758 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  /\  0  e.  CC )  ->  ( y ( abs 
o.  -  ) 0 )  =  ( abs `  ( y  -  0 ) ) )
5954, 13, 58sylancl 644 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  ( y  -  0 ) ) )
6054subid1d 9356 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  -  0 )  =  y )
6160fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( y  -  0 ) )  =  ( abs `  y ) )
6259, 61eqtrd 2436 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  y ) )
63 elbl3 18375 . . . . . . . . . . . . . . . . . . 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
) )
6439, 42, 63mpanl12 664 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  CC  /\  y  e.  CC )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( y
( abs  o.  -  )
0 )  <  1
) )
6513, 54, 64sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <-> 
( y ( abs 
o.  -  ) 0 )  <  1 ) )
6665ibi 233 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  <  1
)
6762, 66eqbrtrrd 4194 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  1
)
6857, 67gtned 9164 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  ( abs `  y ) )
69 abs1 12057 . . . . . . . . . . . . . . . 16  |-  ( abs `  1 )  =  1
70 fveq2 5687 . . . . . . . . . . . . . . . 16  |-  ( 1  =  y  ->  ( abs `  1 )  =  ( abs `  y
) )
7169, 70syl5eqr 2450 . . . . . . . . . . . . . . 15  |-  ( 1  =  y  ->  1  =  ( abs `  y
) )
7271necon3i 2606 . . . . . . . . . . . . . 14  |-  ( 1  =/=  ( abs `  y
)  ->  1  =/=  y )
7368, 72syl 16 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  y )
74 subeq0 9283 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =  0  <->  1  =  y ) )
7574necon3bid 2602 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =/=  0  <->  1  =/=  y ) )
7651, 54, 75sylancr 645 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  -  y )  =/=  0  <->  1  =/=  y ) )
7773, 76mpbird 224 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  =/=  0 )
7856, 77logcld 20421 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  ( 1  -  y
) )  e.  CC )
7978negcld 9354 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
8079adantl 453 . . . . . . . . 9  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
81 eqid 2404 . . . . . . . . 9  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u ( log `  (
1  -  y ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) )
8280, 81fmptd 5852 . . . . . . . 8  |-  (  T. 
->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) : ( 0 (
ball `  ( abs  o. 
-  ) ) 1 ) --> CC )
8354absge0d 12201 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( abs `  y ) )
8457rexrd 9090 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR* )
85 peano2re 9195 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  y )  e.  RR  ->  (
( abs `  y
)  +  1 )  e.  RR )
8657, 85syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  +  1 )  e.  RR )
8786rehalfcld 10170 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  RR )
8887rexrd 9090 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e. 
RR* )
89 iccssxr 10949 . . . . . . . . . . . . . . 15  |-  ( 0 [,]  +oo )  C_  RR*
90 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
m  =  0  <->  j  =  0 ) )
91 oveq2 6048 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
1  /  m )  =  ( 1  / 
j ) )
9290, 91ifbieq2d 3719 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  j  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( j  =  0 ,  0 ,  ( 1  /  j ) ) )
93 eqid 2404 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )
94 c0ex 9041 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
95 ovex 6065 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  j )  e. 
_V
9694, 95ifex 3757 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  e.  _V
9792, 93, 96fvmpt 5765 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j )  =  if ( j  =  0 ,  0 ,  ( 1  / 
j ) ) )
9897eqcomd 2409 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j ) )
9998oveq1d 6055 . . . . . . . . . . . . . . . . . 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 ) ) )
10099mpteq2ia 4251 . . . . . . . . . . . . . . . . 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 ) ) )
101100mpteq2i 4252 . . . . . . . . . . . . . . . 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 ) ) ) )
10213a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  m  e.  NN0 )  /\  m  =  0 )  -> 
0  e.  CC )
103 nn0cn 10187 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN0  ->  m  e.  CC )
104103adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  m  e. 
NN0 )  ->  m  e.  CC )
105 df-ne 2569 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =/=  0  <->  -.  m  =  0 )
106105biimpri 198 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  m  =  0  ->  m  =/=  0 )
107 reccl 9641 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  CC  /\  m  =/=  0 )  -> 
( 1  /  m
)  e.  CC )
108104, 106, 107syl2an 464 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  m  e.  NN0 )  /\  -.  m  =  0 )  ->  ( 1  /  m )  e.  CC )
109102, 108ifclda 3726 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  m  e. 
NN0 )  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  e.  CC )
110109, 93fmptd 5852 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
111 recn 9036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  e.  RR  ->  r  e.  CC )
112 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  r  ->  (
x ^ j )  =  ( r ^
j ) )
113112oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  r  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) )
114113mpteq2dv 4256 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
115 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
116 nn0ex 10183 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  e.  _V
117116mptex 5925 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) )  e.  _V
118114, 115, 117fvmpt 5765 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
119111, 118syl 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 ) ) ) )
120119eqcomd 2409 . . . . . . . . . . . . . . . . . . . 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
) )
121120seqeq3d 11286 . . . . . . . . . . . . . . . . . . 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
) ) )
122121eleq1d 2470 . . . . . . . . . . . . . . . . . 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  ~~>  ) )
123122rabbiia 2906 . . . . . . . . . . . . . . . . 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  ~~>  }
124123supeq1i 7410 . . . . . . . . . . . . . . . 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* ,  <  )
125101, 110, 124radcnvcl 20286 . . . . . . . . . . . . . . 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 ) )
12689, 125sseldi 3306 . . . . . . . . . . . . . 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* )
12747, 126mp1i 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* )
128 1re 9046 . . . . . . . . . . . . . . 15  |-  1  e.  RR
129 avglt1 10161 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) ) )
13057, 128, 129sylancl 644 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( abs `  y
)  <  ( (
( abs `  y
)  +  1 )  /  2 ) ) )
13167, 130mpbid 202 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) )
132 0re 9047 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
133132a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  RR )
134133, 57, 87, 83, 131lelttrd 9184 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <  ( ( ( abs `  y
)  +  1 )  /  2 ) )
135133, 87, 134ltled 9177 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13687, 135absidd 12180 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  =  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13747, 110mp1i 12 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
13887recnd 9070 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  CC )
139 oveq1 6047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( ( ( abs `  y )  +  1 )  / 
2 )  ->  (
x ^ j )  =  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) )
140139oveq2d 6056 . . . . . . . . . . . . . . . . . . . 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 ) ) )
141140mpteq2dv 4256 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
142116mptex 5925 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) )  e.  _V
143141, 115, 142fvmpt 5765 . . . . . . . . . . . . . . . . . 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 ) ) ) )
144138, 143syl 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 ) ) ) )
145144seqeq3d 11286 . . . . . . . . . . . . . . . 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 ) ) ) ) )
146 avglt2 10162 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 ) )
14757, 128, 146sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( ( ( abs `  y )  +  1 )  / 
2 )  <  1
) )
14867, 147mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 )
149136, 148eqbrtrd 4192 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  <  1 )
150 logtayllem 20503 . . . . . . . . . . . . . . . . 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  ~~>  )
151138, 149, 150syl2anc 643 . . . . . . . . . . . . . . . 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  ~~>  )
152145, 151eqeltrd 2478 . . . . . . . . . . . . . . 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  ~~>  )
153101, 137, 124, 138, 152radcnvle 20289 . . . . . . . . . . . . . 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* ,  <  ) )
154136, 153eqbrtrrd 4194 . . . . . . . . . . . . 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* ,  <  )
)
15584, 88, 127, 131, 154xrltletrd 10707 . . . . . . . . . . . 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* ,  <  ) )
156 elico2 10930 . . . . . . . . . . . . 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* ,  <  )
) ) )
157132, 127, 156sylancr 645 . . . . . . . . . . . 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* ,  <  ) ) ) )
15857, 83, 155, 157mpbir3and 1137 . . . . . . . . . . 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* ,  <  ) ) )
159 absf 12096 . . . . . . . . . . . 12  |-  abs : CC
--> RR
160 ffn 5550 . . . . . . . . . . . 12  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
161 elpreima 5809 . . . . . . . . . . . 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* ,  <  ) ) ) ) )
162159, 160, 161mp2b 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* ,  <  ) ) ) )
16354, 158, 162sylanbrc 646 . . . . . . . . . 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* ,  <  ) ) ) )
164 cnvimass 5183 . . . . . . . . . . . . . . . . . 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
165159fdmi 5555 . . . . . . . . . . . . . . . . . 18  |-  dom  abs  =  CC
166164, 165sseqtri 3340 . . . . . . . . . . . . . . . . 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
167166sseli 3304 . . . . . . . . . . . . . . . 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 )
168 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x ^ j )  =  ( y ^
j ) )
169168oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^
j ) ) )
170169mpteq2dv 4256 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
171116mptex 5925 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) )  e.  _V
172170, 115, 171fvmpt 5765 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
173172adantr 452 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
174173fveq1d 5689 . . . . . . . . . . . . . . . . . 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 ) )
175 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
j  =  0  <->  n  =  0 ) )
176 oveq2 6048 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
1  /  j )  =  ( 1  /  n ) )
177175, 176ifbieq2d 3719 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
178 oveq2 6048 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  (
y ^ j )  =  ( y ^
n ) )
179177, 178oveq12d 6058 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  n  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
180 eqid 2404 . . . . . . . . . . . . . . . . . . . 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 ) ) )
181 ovex 6065 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^ n ) )  e.  _V
182179, 180, 181fvmpt 5765 . . . . . . . . . . . . . . . . . . 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 ) ) )
183182adantl 453 . . . . . . . . . . . . . . . . . 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
) ) )
184174, 183eqtr2d 2437 . . . . . . . . . . . . . . . . 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 ) )
185184sumeq2dv 12452 . . . . . . . . . . . . . . . 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 )
)
186167, 185syl 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 )
)
187186mpteq2ia 4251 . . . . . . . . . . . . . 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 )
)
188 eqid 2404 . . . . . . . . . . . . . 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* ,  <  ) ) )
189 eqid 2404 . . . . . . . . . . . . . 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 ) )
190101, 187, 110, 124, 188, 189psercn 20295 . . . . . . . . . . . . 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 ) )
191 cncff 18876 . . . . . . . . . . . . 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 )
192190, 191syl 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 )
193 eqid 2404 . . . . . . . . . . . . 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 ) ) )
194193fmpt 5849 . . . . . . . . . . . 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 )
195192, 194sylibr 204 . . . . . . . . . . 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 )
196195r19.21bi 2764 . . . . . . . . . 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 )
197163, 196sylan2 461 . . . . . . . . 9  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  sum_ n  e. 
NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC )
198 eqid 2404 . . . . . . . . 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 ) ) )
199197, 198fmptd 5852 . . . . . . . 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 )
200 cnex 9027 . . . . . . . . . . . . . 14  |-  CC  e.  _V
201200prid2 3873 . . . . . . . . . . . . 13  |-  CC  e.  { RR ,  CC }
202201a1i 11 . . . . . . . . . . . 12  |-  (  T. 
->  CC  e.  { RR ,  CC } )
20378adantl 453 . . . . . . . . . . . 12  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  ( 1  -  y
) )  e.  CC )
204 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V
205204a1i 11 . . . . . . . . . . . 12  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V )
20630cnmetdval 18758 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  ( 1  -  y
)  e.  CC )  ->  ( 1 ( abs  o.  -  )
( 1  -  y
) )  =  ( abs `  ( 1  -  ( 1  -  y ) ) ) )
20751, 56, 206sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  (
1  -  ( 1  -  y ) ) ) )
208 nncan 9286 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  (
1  -  y ) )  =  y )
20951, 54, 208sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  ( 1  -  y ) )  =  y )
210209fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( 1  -  (
1  -  y ) ) )  =  ( abs `  y ) )
211207, 210eqtrd 2436 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  y
) )
212211, 67eqbrtrd 4192 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 )
213 elbl 18371 . . . . . . . . . . . . . . . 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 ) ) )
21439, 51, 42, 213mp3an 1279 . . . . . . . . . . . . . . 15  |-  ( ( 1  -  y )  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  <->  ( ( 1  -  y )  e.  CC  /\  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 ) )
21556, 212, 214sylanbrc 646 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
216215adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
217 neg1cn 10023 . . . . . . . . . . . . . 14  |-  -u 1  e.  CC
218217a1i 11 . . . . . . . . . . . . 13  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u 1  e.  CC )
219 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
220219dvlog2lem 20496 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
221220sseli 3304 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  ( CC  \  (  -oo (,] 0 ) ) )
222221eldifad 3292 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  CC )
223 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
224223logdmn0 20484 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  x  =/=  0 )
225221, 224syl 16 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  =/=  0 )
226222, 225logcld 20421 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  x )  e.  CC )
227226adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  x )  e.  CC )
228 ovex 6065 . . . . . . . . . . . . . 14  |-  ( 1  /  x )  e. 
_V
229228a1i 11 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  /  x )  e. 
_V )
230 simpr 448 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  y  e.  CC )  ->  y  e.  CC )
23151, 230, 55sylancr 645 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  y  e.  CC )  ->  (
1  -  y )  e.  CC )
232217a1i 11 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  y  e.  CC )  ->  -u 1  e.  CC )
23351a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  y  e.  CC )  ->  1  e.  CC )
23413a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  y  e.  CC )  ->  0  e.  CC )
23551a1i 11 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  1  e.  CC )
236202, 235dvmptc 19797 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  1 ) )  =  ( y  e.  CC  |->  0 ) )
237202dvmptid 19796 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  y ) )  =  ( y  e.  CC  |->  1 ) )
238202, 233, 234, 236, 230, 233, 237dvmptsub 19806 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  ( 0  -  1 ) ) )
239 df-neg 9250 . . . . . . . . . . . . . . . 16  |-  -u 1  =  ( 0  -  1 )
240239mpteq2i 4252 . . . . . . . . . . . . . . 15  |-  ( y  e.  CC  |->  -u 1
)  =  ( y  e.  CC  |->  ( 0  -  1 ) )
241238, 240syl6eqr 2454 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  -u
1 ) )
24253a1i 11 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
C_  CC )
243 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
244243cnfldtop 18771 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  e.  Top
245243cnfldtopon 18770 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
246245toponunii 16952 . . . . . . . . . . . . . . . . 17  |-  CC  =  U. ( TopOpen ` fld )
247246restid 13616 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
248244, 247ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
249248eqcomi 2408 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
250243cnfldtopn 18769 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
251250blopn 18483 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld ) )
25239, 13, 42, 251mp3an 1279 . . . . . . . . . . . . . . 15  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld )
253252a1i 11 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  ( TopOpen ` fld ) )
254202, 231, 232, 241, 242, 249, 243, 253dvmptres 19802 . . . . . . . . . . . . 13  |-  (  T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  -  y ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u 1 ) )
255219dvlog2 20497 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) )
256 logf1o 20415 . . . . . . . . . . . . . . . . . . . 20  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
257 f1of 5633 . . . . . . . . . . . . . . . . . . . 20  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
258256, 257ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  log :
( CC  \  {
0 } ) --> ran 
log
259223logdmss 20486 . . . . . . . . . . . . . . . . . . . 20  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
260220, 259sstri 3317 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
261 fssres 5569 . . . . . . . . . . . . . . . . . . 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 )
262258, 260, 261mp2an 654 . . . . . . . . . . . . . . . . . 18  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log
263262a1i 11 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log )
264263feqmptd 5738 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) ) )
265 fvres 5704 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  x
)  =  ( log `  x ) )
266265mpteq2ia 4251 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) )  =  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( log `  x
) )
267264, 266syl6eq 2452 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )
268267oveq2d 6056 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( CC  _D  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) )  =  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) ) )
269255, 268syl5reqr 2451 . . . . . . . . . . . . 13  |-  (  T. 
->  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) ) )
270 fveq2 5687 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  ( log `  x )  =  ( log `  (
1  -  y ) ) )
271 oveq2 6048 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  (
1  /  x )  =  ( 1  / 
( 1  -  y
) ) )
272202, 202, 216, 218, 227, 229, 254, 269, 270, 271dvmptco 19811 . . . . . . . . . . . 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
) ) )
273202, 203, 205, 272dvmptneg 19805 . . . . . . . . . . 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 ) ) )
27456, 77reccld 9739 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e.  CC )
275 mulcom 9032 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  /  (
1  -  y ) )  e.  CC  /\  -u 1  e.  CC )  ->  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
276274, 217, 275sylancl 644 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
277274mulm1d 9441 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( -u 1  x.  ( 1  /  (
1  -  y ) ) )  =  -u ( 1  /  (
1  -  y ) ) )
278276, 277eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u ( 1  / 
( 1  -  y
) ) )
279278negeqd 9256 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u -u ( 1  / 
( 1  -  y
) ) )
280274negnegd 9358 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u -u (
1  /  ( 1  -  y ) )  =  ( 1  / 
( 1  -  y
) ) )
281279, 280eqtrd 2436 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( 1  /  (
1  -  y ) ) )
282281mpteq2ia 4251 . . . . . . . . . . 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 ) ) )
283273, 282syl6eq 2452 . . . . . . . . . 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
) ) ) )
284283dmeqd 5031 . . . . . . . . 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 ) ) ) )
285 dmmptg 5326 . . . . . . . . . 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 ) )
286 ovex 6065 . . . . . . . . . . 11  |-  ( 1  /  ( 1  -  y ) )  e. 
_V
287286a1i 11 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e. 
_V )
288285, 287mprg 2735 . . . . . . . . 9  |-  dom  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  ( 1  -  y ) ) )  =  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )
289284, 288syl6eq 2452 . . . . . . . 8  |-  (  T. 
->  dom  ( CC  _D  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
290 sumex 12436 . . . . . . . . . . . 12  |-  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  e.  _V
291290a1i 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 )
292 fveq2 5687 . . . . . . . . . . . . . . 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 )
)
293292cbvsumv 12445 . . . . . . . . . . . . . 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 )
294186, 293syl6eq 2452 . . . . . . . . . . . . 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 )
)
295294mpteq2ia 4251 . . . . . . . . . . . 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 )
)
296 eqid 2404 . . . . . . . . . . . 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
) )
297101, 295, 110, 124, 188, 189, 296pserdv2 20299 . . . . . . . . . . 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 ) ) ) ) )
298163ssriv 3312 . . . . . . . . . . . 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* ,  <  ) ) )
299298a1i 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* ,  <  ) ) ) )
300202, 196, 291, 297, 299, 249, 243, 253dvmptres 19802 . . . . . . . . . 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 ) ) ) ) )
301 nnnn0 10184 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  NN0 )
302301adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  NN0 )
303 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
m  =  0  <->  n  =  0 ) )
304 oveq2 6048 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
1  /  m )  =  ( 1  /  n ) )
305303, 304ifbieq2d 3719 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
306 ovex 6065 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  n )  e. 
_V
30794, 306ifex 3757 . . . . . . . . . . . . . . . . . . . 20  |-  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  _V
308305, 93, 307fvmpt 5765 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
309302, 308syl 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 ) ) )
310 nnne0 9988 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  n  =/=  0 )
311310adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  =/=  0 )
312311neneqd 2583 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  -.  n  =  0 )
313 iffalse 3706 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  n  =  0  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  =  ( 1  /  n ) )
314312, 313syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  =  ( 1  /  n ) )
315309, 314eqtrd 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
)  =  ( 1  /  n ) )
316315oveq2d 6056 . . . . . . . . . . . . . . . 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 ) ) )
317 nncn 9964 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  n  e.  CC )
318317adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  CC )
319318, 311recidd 9741 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( 1  /  n ) )  =  1 )
320316, 319eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  =  1 )
321320oveq1d 6055 . . . . . . . . . . . . . 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 ) ) ) )
322 nnm1nn0 10217 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  (
n  -  1 )  e.  NN0 )
323 expcl 11354 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  CC  /\  ( n  -  1
)  e.  NN0 )  ->  ( y ^ (
n  -  1 ) )  e.  CC )
32454, 322, 323syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
y ^ ( n  -  1 ) )  e.  CC )
325324mulid2d 9062 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
1  x.  ( y ^ ( n  - 
1 ) ) )  =  ( y ^
( n  -  1 ) ) )
326321, 325eqtrd 2436 . . . . . . . . . . . . 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 ) ) )
327326sumeq2dv 12452 . . . . . . . . . . . 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 ) ) )
328 nnuz 10477 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
329 1e0p1 10366 . . . . . . . . . . . . . . . 16  |-  1  =  ( 0  +  1 )
330329fveq2i 5690 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
331328, 330eqtri 2424 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
332 oveq1 6047 . . . . . . . . . . . . . . 15  |-  ( n  =  ( 1  +  m )  ->  (
n  -  1 )  =  ( ( 1  +  m )  - 
1 ) )
333332oveq2d 6056 . . . . . . . . . . . . . 14  |-  ( n  =  ( 1  +  m )  ->  (
y ^ ( n  -  1 ) )  =  ( y ^
( ( 1  +  m )  -  1 ) ) )
334 1z 10267 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
335334a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  e.  ZZ )
3362a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  ZZ )
3371, 331, 333, 335, 336, 324isumshft 12574 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ ( ( 1  +  m )  - 
1 ) ) )
338 pncan2 9268 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  m  e.  CC )  ->  ( ( 1  +  m )  -  1 )  =  m )
33951, 103, 338sylancr 645 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( 1  +  m )  -  1 )  =  m )
340339oveq2d 6056 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( y ^ ( ( 1  +  m )  - 
1 ) )  =  ( y ^ m
) )
341340sumeq2i 12448 . . . . . . . . . . . . 13  |-  sum_ m  e.  NN0  ( y ^
( ( 1  +  m )  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m )
342337, 341syl6eq 2452 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m ) )
343 geoisum 12609 . . . . . . . . . . . . 13  |-  ( ( y  e.  CC  /\  ( abs `  y )  <  1 )  ->  sum_ m  e.  NN0  (
y ^ m )  =  ( 1  / 
( 1  -  y
) ) )
34454, 67, 343syl2anc 643 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ m  e. 
NN0  ( y ^
m )  =  ( 1  /  ( 1  -  y ) ) )
345327, 342, 3443eqtrd 2440 . . . . . . . . . . 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
) ) )
346345mpteq2ia 4251 . . . . . . . . . 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 ) ) )
347300, 346syl6eq 2452 . . . . . . . . 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
) ) ) )
348283, 347eqtr4d 2439 . . . . . . . 8  |-  (  T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y )