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

Theorem logtayl 20023
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 10278 . . . 4  |-  NN0  =  ( ZZ>= `  0 )
2 0z 10051 . . . . 5  |-  0  e.  ZZ
32a1i 10 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
0  e.  ZZ )
4 eqeq1 2302 . . . . . . . 8  |-  ( k  =  n  ->  (
k  =  0  <->  n  =  0 ) )
5 oveq2 5882 . . . . . . . 8  |-  ( k  =  n  ->  (
1  /  k )  =  ( 1  /  n ) )
64, 5ifbieq2d 3598 . . . . . . 7  |-  ( k  =  n  ->  if ( k  =  0 ,  0 ,  ( 1  /  k ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
7 oveq2 5882 . . . . . . 7  |-  ( k  =  n  ->  ( A ^ k )  =  ( A ^ n
) )
86, 7oveq12d 5892 . . . . . 6  |-  ( k  =  n  ->  ( if ( k  =  0 ,  0 ,  ( 1  /  k ) )  x.  ( A ^ k ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) ) )
9 eqid 2296 . . . . . 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 5899 . . . . . 6  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^ n ) )  e.  _V
118, 9, 10fvmpt 5618 . . . . 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 452 . . . 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 8847 . . . . . . 7  |-  0  e.  CC
1413a1i 10 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  n  =  0 )  ->  0  e.  CC )
15 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  n  e.  NN0 )
16 elnn0 9983 . . . . . . . . . . . 12  |-  ( n  e.  NN0  <->  ( n  e.  NN  \/  n  =  0 ) )
1715, 16sylib 188 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( n  e.  NN  \/  n  =  0 ) )
1817ord 366 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  e.  NN  ->  n  = 
0 ) )
1918con1d 116 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( -.  n  =  0  ->  n  e.  NN ) )
2019imp 418 . . . . . . . 8  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  ->  n  e.  NN )
2120nnrecred 9807 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  RR )
2221recnd 8877 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  ( abs `  A )  <  1
)  /\  n  e.  NN0 )  /\  -.  n  =  0 )  -> 
( 1  /  n
)  e.  CC )
2314, 22ifclda 3605 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  CC )
24 expcl 11137 . . . . . 6  |-  ( ( A  e.  CC  /\  n  e.  NN0 )  -> 
( A ^ n
)  e.  CC )
2524adantlr 695 . . . . 5  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( A ^
n )  e.  CC )
2623, 25mulcld 8871 . . . 4  |-  ( ( ( A  e.  CC  /\  ( abs `  A
)  <  1 )  /\  n  e.  NN0 )  ->  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( A ^
n ) )  e.  CC )
27 logtayllem 20022 . . . 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 12237 . . 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 443 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  CC )
30 eqid 2296 . . . . . . . . 9  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3130cnmetdval 18296 . . . . . . . 8  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  ( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
3229, 13, 31sylancl 643 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  ( A  -  0 ) ) )
33 subid1 9084 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( A  -  0 )  =  A )
3433adantr 451 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  -  0 )  =  A )
3534fveq2d 5545 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  ( A  -  0 ) )  =  ( abs `  A ) )
3632, 35eqtrd 2328 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  =  ( abs `  A ) )
37 simpr 447 . . . . . 6  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( abs `  A
)  <  1 )
3836, 37eqbrtrd 4059 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A ( abs 
o.  -  ) 0 )  <  1 )
39 cnxmet 18298 . . . . . . 7  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
40 1rp 10374 . . . . . . . 8  |-  1  e.  RR+
41 rpxr 10377 . . . . . . . 8  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
4240, 41ax-mp 8 . . . . . . 7  |-  1  e.  RR*
43 elbl3 17967 . . . . . . 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 663 . . . . . 6  |-  ( ( 0  e.  CC  /\  A  e.  CC )  ->  ( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4513, 29, 44sylancr 644 . . . . 5  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  -> 
( A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( A
( abs  o.  -  )
0 )  <  1
) )
4638, 45mpbird 223 . . . 4  |-  ( ( A  e.  CC  /\  ( abs `  A )  <  1 )  ->  A  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
47 tru 1312 . . . . . 6  |-  T.
48 eqid 2296 . . . . . . . 8  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )
4913a1i 10 . . . . . . . 8  |-  (  T. 
->  0  e.  CC )
5042a1i 10 . . . . . . . 8  |-  (  T. 
->  1  e.  RR* )
51 ax-1cn 8811 . . . . . . . . . . . . 13  |-  1  e.  CC
52 blssm 17984 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
5339, 13, 42, 52mp3an 1277 . . . . . . . . . . . . . 14  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
5453sseli 3189 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  CC )
55 subcl 9067 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  y
)  e.  CC )
5651, 54, 55sylancr 644 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  CC )
5754abscld 11934 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR )
5830cnmetdval 18296 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  CC  /\  0  e.  CC )  ->  ( y ( abs 
o.  -  ) 0 )  =  ( abs `  ( y  -  0 ) ) )
5954, 13, 58sylancl 643 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  ( y  -  0 ) ) )
6054subid1d 9162 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  -  0 )  =  y )
6160fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( y  -  0 ) )  =  ( abs `  y ) )
6259, 61eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  =  ( abs `  y ) )
63 elbl3 17967 . . . . . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  CC  /\  y  e.  CC )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( y
( abs  o.  -  )
0 )  <  1
) )
6513, 54, 64sylancr 644 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  <-> 
( y ( abs 
o.  -  ) 0 )  <  1 ) )
6665ibi 232 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y
( abs  o.  -  )
0 )  <  1
)
6762, 66eqbrtrrd 4061 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  1
)
6857, 67gtned 8970 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  ( abs `  y ) )
69 abs1 11798 . . . . . . . . . . . . . . . 16  |-  ( abs `  1 )  =  1
70 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( 1  =  y  ->  ( abs `  1 )  =  ( abs `  y
) )
7169, 70syl5eqr 2342 . . . . . . . . . . . . . . 15  |-  ( 1  =  y  ->  1  =  ( abs `  y
) )
7271necon3i 2498 . . . . . . . . . . . . . 14  |-  ( 1  =/=  ( abs `  y
)  ->  1  =/=  y )
7368, 72syl 15 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =/=  y )
74 subeq0 9089 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =  0  <->  1  =  y ) )
7574necon3bid 2494 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( ( 1  -  y )  =/=  0  <->  1  =/=  y ) )
7651, 54, 75sylancr 644 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  -  y )  =/=  0  <->  1  =/=  y ) )
7773, 76mpbird 223 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  =/=  0 )
78 logcl 19942 . . . . . . . . . . . 12  |-  ( ( ( 1  -  y
)  e.  CC  /\  ( 1  -  y
)  =/=  0 )  ->  ( log `  (
1  -  y ) )  e.  CC )
7956, 77, 78syl2anc 642 . . . . . . . . . . 11  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  ( 1  -  y
) )  e.  CC )
8079negcld 9160 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
8180adantl 452 . . . . . . . . 9  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u ( log `  ( 1  -  y
) )  e.  CC )
82 eqid 2296 . . . . . . . . 9  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u ( log `  (
1  -  y ) ) )  =  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) )
8381, 82fmptd 5700 . . . . . . . 8  |-  (  T. 
->  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) : ( 0 (
ball `  ( abs  o. 
-  ) ) 1 ) --> CC )
8454absge0d 11942 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( abs `  y ) )
8557rexrd 8897 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  e.  RR* )
86 peano2re 9001 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  y )  e.  RR  ->  (
( abs `  y
)  +  1 )  e.  RR )
8757, 86syl 15 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  +  1 )  e.  RR )
8887rehalfcld 9974 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  RR )
8988rexrd 8897 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e. 
RR* )
90 iccssxr 10748 . . . . . . . . . . . . . . 15  |-  ( 0 [,]  +oo )  C_  RR*
91 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
m  =  0  <->  j  =  0 ) )
92 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  j  ->  (
1  /  m )  =  ( 1  / 
j ) )
9391, 92ifbieq2d 3598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  j  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( j  =  0 ,  0 ,  ( 1  /  j ) ) )
94 eqid 2296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )  =  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) )
95 c0ex 8848 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
96 ovex 5899 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  j )  e. 
_V
9795, 96ifex 3636 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  e.  _V
9893, 94, 97fvmpt 5618 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j )  =  if ( j  =  0 ,  0 ,  ( 1  / 
j ) ) )
9998eqcomd 2301 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  j ) )
10099oveq1d 5889 . . . . . . . . . . . . . . . . . 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 ) ) )
101100mpteq2ia 4118 . . . . . . . . . . . . . . . . 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 ) ) )
102101mpteq2i 4119 . . . . . . . . . . . . . . . 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 ) ) ) )
10313a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  m  e.  NN0 )  /\  m  =  0 )  -> 
0  e.  CC )
104 nn0cn 9991 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN0  ->  m  e.  CC )
105104adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  m  e. 
NN0 )  ->  m  e.  CC )
106 df-ne 2461 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =/=  0  <->  -.  m  =  0 )
107106biimpri 197 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  m  =  0  ->  m  =/=  0 )
108 reccl 9447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  CC  /\  m  =/=  0 )  -> 
( 1  /  m
)  e.  CC )
109105, 107, 108syl2an 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  m  e.  NN0 )  /\  -.  m  =  0 )  ->  ( 1  /  m )  e.  CC )
110103, 109ifclda 3605 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  m  e. 
NN0 )  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  e.  CC )
111110, 94fmptd 5700 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
112 recn 8843 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  e.  RR  ->  r  e.  CC )
113 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  r  ->  (
x ^ j )  =  ( r ^
j ) )
114113oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  r  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^
j ) ) )
115114mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
116 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
117 nn0ex 9987 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN0  e.  _V
118117mptex 5762 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( r ^ j ) ) )  e.  _V
119115, 116, 118fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
120112, 119syl 15 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
121120eqcomd 2301 . . . . . . . . . . . . . . . . . . . 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
) )
122121seqeq3d 11070 . . . . . . . . . . . . . . . . . . 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
) ) )
123122eleq1d 2362 . . . . . . . . . . . . . . . . . 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  ~~>  ) )
124123rabbiia 2791 . . . . . . . . . . . . . . . . 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  ~~>  }
125124supeq1i 7216 . . . . . . . . . . . . . . . 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* ,  <  )
126102, 111, 125radcnvcl 19809 . . . . . . . . . . . . . . 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 ) )
12790, 126sseldi 3191 . . . . . . . . . . . . . 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* )
12847, 127mp1i 11 . . . . . . . . . . . . 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* )
129 1re 8853 . . . . . . . . . . . . . . 15  |-  1  e.  RR
130 avglt1 9965 . . . . . . . . . . . . . . 15  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) ) )
13157, 129, 130sylancl 643 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( abs `  y
)  <  ( (
( abs `  y
)  +  1 )  /  2 ) ) )
13267, 131mpbid 201 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  y )  <  (
( ( abs `  y
)  +  1 )  /  2 ) )
133 0re 8854 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR
134133a1i 10 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  RR )
135134, 57, 88, 84, 132lelttrd 8990 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <  ( ( ( abs `  y
)  +  1 )  /  2 ) )
136134, 88, 135ltled 8983 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  <_  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13788, 136absidd 11921 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  =  ( ( ( abs `  y
)  +  1 )  /  2 ) )
13847, 111mp1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) : NN0 --> CC )
13988recnd 8877 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  e.  CC )
140 oveq1 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( ( ( abs `  y )  +  1 )  / 
2 )  ->  (
x ^ j )  =  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) )
141140oveq2d 5890 . . . . . . . . . . . . . . . . . . . 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 ) ) )
142141mpteq2dv 4123 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
143117mptex 5762 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( ( ( ( abs `  y
)  +  1 )  /  2 ) ^
j ) ) )  e.  _V
144142, 116, 143fvmpt 5618 . . . . . . . . . . . . . . . . . 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 ) ) ) )
145139, 144syl 15 . . . . . . . . . . . . . . . . 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 ) ) ) )
146145seqeq3d 11070 . . . . . . . . . . . . . . . 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 ) ) ) ) )
147 avglt2 9966 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( abs `  y
)  e.  RR  /\  1  e.  RR )  ->  ( ( abs `  y
)  <  1  <->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 ) )
14857, 129, 147sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( abs `  y )  <  1  <->  ( ( ( abs `  y )  +  1 )  / 
2 )  <  1
) )
14967, 148mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( abs `  y
)  +  1 )  /  2 )  <  1 )
150137, 149eqbrtrd 4059 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( ( ( abs `  y )  +  1 )  /  2 ) )  <  1 )
151 logtayllem 20022 . . . . . . . . . . . . . . . . 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  ~~>  )
152139, 150, 151syl2anc 642 . . . . . . . . . . . . . . . 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  ~~>  )
153146, 152eqeltrd 2370 . . . . . . . . . . . . . . 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  ~~>  )
154102, 138, 125, 139, 153radcnvle 19812 . . . . . . . . . . . . . 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* ,  <  ) )
155137, 154eqbrtrrd 4061 . . . . . . . . . . . . 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* ,  <  )
)
15685, 89, 128, 132, 155xrltletrd 10508 . . . . . . . . . . . 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* ,  <  ) )
157 elico2 10730 . . . . . . . . . . . . 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* ,  <  )
) ) )
158133, 128, 157sylancr 644 . . . . . . . . . . . 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* ,  <  ) ) ) )
15957, 84, 156, 158mpbir3and 1135 . . . . . . . . . . 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* ,  <  ) ) )
160 absf 11837 . . . . . . . . . . . 12  |-  abs : CC
--> RR
161 ffn 5405 . . . . . . . . . . . 12  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
162 elpreima 5661 . . . . . . . . . . . 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* ,  <  ) ) ) ) )
163160, 161, 162mp2b 9 . . . . . . . . . . 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* ,  <  ) ) ) )
16454, 159, 163sylanbrc 645 . . . . . . . . . 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* ,  <  ) ) ) )
165 cnvimass 5049 . . . . . . . . . . . . . . . . . 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
166160fdmi 5410 . . . . . . . . . . . . . . . . . 18  |-  dom  abs  =  CC
167165, 166sseqtri 3223 . . . . . . . . . . . . . . . . 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
168167sseli 3189 . . . . . . . . . . . . . . . 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 )
169 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
x ^ j )  =  ( y ^
j ) )
170169oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( x ^ j ) )  =  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^
j ) ) )
171170mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
172117mptex 5762 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  NN0  |->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) ) )  e.  _V
173171, 116, 172fvmpt 5618 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
174173adantr 451 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
175174fveq1d 5543 . . . . . . . . . . . . . . . . . 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 ) )
176 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
j  =  0  <->  n  =  0 ) )
177 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  n  ->  (
1  /  j )  =  ( 1  /  n ) )
178176, 177ifbieq2d 3598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  if ( j  =  0 ,  0 ,  ( 1  /  j ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
179 oveq2 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  n  ->  (
y ^ j )  =  ( y ^
n ) )
180178, 179oveq12d 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  n  ->  ( if ( j  =  0 ,  0 ,  ( 1  /  j ) )  x.  ( y ^ j ) )  =  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) ) )
181 eqid 2296 . . . . . . . . . . . . . . . . . . . 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 ) ) )
182 ovex 5899 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^ n ) )  e.  _V
183180, 181, 182fvmpt 5618 . . . . . . . . . . . . . . . . . . 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 ) ) )
184183adantl 452 . . . . . . . . . . . . . . . . . 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
) ) )
185175, 184eqtr2d 2329 . . . . . . . . . . . . . . . . 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 ) )
186185sumeq2dv 12192 . . . . . . . . . . . . . . . 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 )
)
187168, 186syl 15 . . . . . . . . . . . . . . 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 )
)
188187mpteq2ia 4118 . . . . . . . . . . . . . 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 )
)
189 eqid 2296 . . . . . . . . . . . . . 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* ,  <  ) ) )
190 eqid 2296 . . . . . . . . . . . . . 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 ) )
191102, 188, 111, 125, 189, 190psercn 19818 . . . . . . . . . . . . 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 ) )
192 cncff 18413 . . . . . . . . . . . . 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 )
193191, 192syl 15 . . . . . . . . . . . 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 )
194 eqid 2296 . . . . . . . . . . . . 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 ) ) )
195194fmpt 5697 . . . . . . . . . . . 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 )
196193, 195sylibr 203 . . . . . . . . . . 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 )
197196r19.21bi 2654 . . . . . . . . . 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 )
198164, 197sylan2 460 . . . . . . . . 9  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  sum_ n  e. 
NN0  ( if ( n  =  0 ,  0 ,  ( 1  /  n ) )  x.  ( y ^
n ) )  e.  CC )
199 eqid 2296 . . . . . . . . 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 ) ) )
200198, 199fmptd 5700 . . . . . . . 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 )
201 cnex 8834 . . . . . . . . . . . . . 14  |-  CC  e.  _V
202201prid2 3748 . . . . . . . . . . . . 13  |-  CC  e.  { RR ,  CC }
203202a1i 10 . . . . . . . . . . . 12  |-  (  T. 
->  CC  e.  { RR ,  CC } )
20479adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  ( 1  -  y
) )  e.  CC )
205 ovex 5899 . . . . . . . . . . . . 13  |-  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V
206205a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  e. 
_V )
20730cnmetdval 18296 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  ( 1  -  y
)  e.  CC )  ->  ( 1 ( abs  o.  -  )
( 1  -  y
) )  =  ( abs `  ( 1  -  ( 1  -  y ) ) ) )
20851, 56, 207sylancr 644 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  (
1  -  ( 1  -  y ) ) ) )
209 nncan 9092 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  y  e.  CC )  ->  ( 1  -  (
1  -  y ) )  =  y )
21051, 54, 209sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  ( 1  -  y ) )  =  y )
211210fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( abs `  ( 1  -  (
1  -  y ) ) )  =  ( abs `  y ) )
212208, 211eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  =  ( abs `  y
) )
213212, 67eqbrtrd 4059 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 )
214 elbl 17965 . . . . . . . . . . . . . . . 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 ) ) )
21539, 51, 42, 214mp3an 1277 . . . . . . . . . . . . . . 15  |-  ( ( 1  -  y )  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  <->  ( ( 1  -  y )  e.  CC  /\  ( 1 ( abs  o.  -  ) ( 1  -  y ) )  <  1 ) )
21656, 213, 215sylanbrc 645 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
217216adantl 452 . . . . . . . . . . . . 13  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  -  y )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
218 neg1cn 9829 . . . . . . . . . . . . . 14  |-  -u 1  e.  CC
219218a1i 10 . . . . . . . . . . . . 13  |-  ( (  T.  /\  y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  -u 1  e.  CC )
220 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
221220dvlog2lem 20015 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
222221sseli 3189 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  ( CC  \  (  -oo (,] 0 ) ) )
223 eldifi 3311 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  x  e.  CC )
224222, 223syl 15 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  e.  CC )
225 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
226225logdmn0 20003 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( CC  \ 
(  -oo (,] 0 ) )  ->  x  =/=  0 )
227222, 226syl 15 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  x  =/=  0 )
228 logcl 19942 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  x  =/=  0 )  -> 
( log `  x
)  e.  CC )
229224, 227, 228syl2anc 642 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  x )  e.  CC )
230229adantl 452 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( log `  x )  e.  CC )
231 ovex 5899 . . . . . . . . . . . . . 14  |-  ( 1  /  x )  e. 
_V
232231a1i 10 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  ->  ( 1  /  x )  e. 
_V )
233 simpr 447 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  y  e.  CC )  ->  y  e.  CC )
23451, 233, 55sylancr 644 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  y  e.  CC )  ->  (
1  -  y )  e.  CC )
235218a1i 10 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  y  e.  CC )  ->  -u 1  e.  CC )
23651a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  y  e.  CC )  ->  1  e.  CC )
23713a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  y  e.  CC )  ->  0  e.  CC )
23851a1i 10 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  1  e.  CC )
239203, 238dvmptc 19323 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  1 ) )  =  ( y  e.  CC  |->  0 ) )
240203dvmptid 19322 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  y ) )  =  ( y  e.  CC  |->  1 ) )
241203, 236, 237, 239, 233, 236, 240dvmptsub 19332 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  ( 0  -  1 ) ) )
242 df-neg 9056 . . . . . . . . . . . . . . . 16  |-  -u 1  =  ( 0  -  1 )
243242mpteq2i 4119 . . . . . . . . . . . . . . 15  |-  ( y  e.  CC  |->  -u 1
)  =  ( y  e.  CC  |->  ( 0  -  1 ) )
244241, 243syl6eqr 2346 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( CC  _D  (
y  e.  CC  |->  ( 1  -  y ) ) )  =  ( y  e.  CC  |->  -u
1 ) )
24553a1i 10 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) 
C_  CC )
246 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
247246cnfldtop 18309 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  e.  Top
248246cnfldtopon 18308 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
249248toponunii 16686 . . . . . . . . . . . . . . . . 17  |-  CC  =  U. ( TopOpen ` fld )
250249restid 13354 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
251247, 250ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
252251eqcomi 2300 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
253246cnfldtopn 18307 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
254253blopn 18062 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  1  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld ) )
25539, 13, 42, 254mp3an 1277 . . . . . . . . . . . . . . 15  |-  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  (
TopOpen ` fld )
256255a1i 10 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  e.  ( TopOpen ` fld ) )
257203, 234, 235, 244, 245, 252, 246, 256dvmptres 19328 . . . . . . . . . . . . 13  |-  (  T. 
->  ( CC  _D  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  -  y ) ) )  =  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  -u 1 ) )
258220dvlog2 20016 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) )
259 logf1o 19938 . . . . . . . . . . . . . . . . . . . 20  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
260 f1of 5488 . . . . . . . . . . . . . . . . . . . 20  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
261259, 260ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  log :
( CC  \  {
0 } ) --> ran 
log
262225logdmss 20005 . . . . . . . . . . . . . . . . . . . 20  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
263221, 262sstri 3201 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
264 fssres 5424 . . . . . . . . . . . . . . . . . . 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 )
265261, 263, 264mp2an 653 . . . . . . . . . . . . . . . . . 18  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log
266265a1i 10 . . . . . . . . . . . . . . . . 17  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> ran  log )
267266feqmptd 5591 . . . . . . . . . . . . . . . 16  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) ) )
268 fvres 5558 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  x
)  =  ( log `  x ) )
269268mpteq2ia 4118 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  x ) )  =  ( x  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( log `  x
) )
270267, 269syl6eq 2344 . . . . . . . . . . . . . . 15  |-  (  T. 
->  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )
271270oveq2d 5890 . . . . . . . . . . . . . 14  |-  (  T. 
->  ( CC  _D  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) )  =  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) ) )
272258, 271syl5reqr 2343 . . . . . . . . . . . . 13  |-  (  T. 
->  ( CC  _D  (
x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( log `  x ) ) )  =  ( x  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  x
) ) )
273 fveq2 5541 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  ( log `  x )  =  ( log `  (
1  -  y ) ) )
274 oveq2 5882 . . . . . . . . . . . . 13  |-  ( x  =  ( 1  -  y )  ->  (
1  /  x )  =  ( 1  / 
( 1  -  y
) ) )
275203, 203, 217, 219, 230, 232, 257, 272, 273, 274dvmptco 19337 . . . . . . . . . . . 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
) ) )
276203, 204, 206, 275dvmptneg 19331 . . . . . . . . . . 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 ) ) )
27756, 77reccld 9545 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e.  CC )
278 mulcom 8839 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  /  (
1  -  y ) )  e.  CC  /\  -u 1  e.  CC )  ->  ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
279277, 218, 278sylancl 643 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( -u 1  x.  ( 1  /  (
1  -  y ) ) ) )
280277mulm1d 9247 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( -u 1  x.  ( 1  /  (
1  -  y ) ) )  =  -u ( 1  /  (
1  -  y ) ) )
281279, 280eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u ( 1  / 
( 1  -  y
) ) )
282281negeqd 9062 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  = 
-u -u ( 1  / 
( 1  -  y
) ) )
283277negnegd 9164 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u -u (
1  /  ( 1  -  y ) )  =  ( 1  / 
( 1  -  y
) ) )
284282, 283eqtrd 2328 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  -u ( ( 1  /  ( 1  -  y ) )  x.  -u 1 )  =  ( 1  /  (
1  -  y ) ) )
285284mpteq2ia 4118 . . . . . . . . . . 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 ) ) )
286276, 285syl6eq 2344 . . . . . . . . . 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
) ) ) )
287286dmeqd 4897 . . . . . . . . 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 ) ) ) )
288 dmmptg 5186 . . . . . . . . . 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 ) )
289 ovex 5899 . . . . . . . . . . 11  |-  ( 1  /  ( 1  -  y ) )  e. 
_V
290289a1i 10 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( 1  /  ( 1  -  y ) )  e. 
_V )
291288, 290mprg 2625 . . . . . . . . 9  |-  dom  (
y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  ( 1  -  y ) ) )  =  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )
292287, 291syl6eq 2344 . . . . . . . 8  |-  (  T. 
->  dom  ( CC  _D  ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  |->  -u ( log `  ( 1  -  y ) ) ) )  =  ( 0 ( ball `  ( abs  o.  -  ) ) 1 ) )
293 sumex 12176 . . . . . . . . . . . 12  |-  sum_ n  e.  NN  ( ( n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  x.  ( y ^ ( n  - 
1 ) ) )  e.  _V
294293a1i 10 . . . . . . . . . . 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 )
295 fveq2 5541 . . . . . . . . . . . . . . 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 )
)
296295cbvsumv 12185 . . . . . . . . . . . . . 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 )
297187, 296syl6eq 2344 . . . . . . . . . . . . 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 )
)
298297mpteq2ia 4118 . . . . . . . . . . . 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 )
)
299 eqid 2296 . . . . . . . . . . . 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
) )
300102, 298, 111, 125, 189, 190, 299pserdv2 19822 . . . . . . . . . . 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 ) ) ) ) )
301164ssriv 3197 . . . . . . . . . . . 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* ,  <  ) ) )
302301a1i 10 . . . . . . . . . . 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* ,  <  ) ) ) )
303203, 197, 294, 300, 302, 252, 246, 256dvmptres 19328 . . . . . . . . . 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 ) ) ) ) )
304 nnnn0 9988 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  NN0 )
305304adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  NN0 )
306 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
m  =  0  <->  n  =  0 ) )
307 oveq2 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  (
1  /  m )  =  ( 1  /  n ) )
308306, 307ifbieq2d 3598 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  if ( m  =  0 ,  0 ,  ( 1  /  m ) )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
309 ovex 5899 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  /  n )  e. 
_V
31095, 309ifex 3636 . . . . . . . . . . . . . . . . . . . 20  |-  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  e.  _V
311308, 94, 310fvmpt 5618 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n )  =  if ( n  =  0 ,  0 ,  ( 1  /  n ) ) )
312305, 311syl 15 . . . . . . . . . . . . . . . . . 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 ) ) )
313 nnne0 9794 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  n  =/=  0 )
314313adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  =/=  0 )
315314neneqd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  -.  n  =  0 )
316 iffalse 3585 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  n  =  0  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  =  ( 1  /  n ) )
317315, 316syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  if ( n  =  0 ,  0 ,  ( 1  /  n ) )  =  ( 1  /  n ) )
318312, 317eqtrd 2328 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n
)  =  ( 1  /  n ) )
319318oveq2d 5890 . . . . . . . . . . . . . . . 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 ) ) )
320 nncn 9770 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  n  e.  CC )
321320adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  n  e.  CC )
322321, 314recidd 9547 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( 1  /  n ) )  =  1 )
323319, 322eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
n  x.  ( ( m  e.  NN0  |->  if ( m  =  0 ,  0 ,  ( 1  /  m ) ) ) `  n ) )  =  1 )
324323oveq1d 5889 . . . . . . . . . . . . . 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 ) ) ) )
325 nnm1nn0 10021 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  ->  (
n  -  1 )  e.  NN0 )
326 expcl 11137 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  CC  /\  ( n  -  1
)  e.  NN0 )  ->  ( y ^ (
n  -  1 ) )  e.  CC )
32754, 325, 326syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
y ^ ( n  -  1 ) )  e.  CC )
328327mulid2d 8869 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ( 0 ( ball `  ( abs  o.  -  ) ) 1 )  /\  n  e.  NN )  ->  (
1  x.  ( y ^ ( n  - 
1 ) ) )  =  ( y ^
( n  -  1 ) ) )
329324, 328eqtrd 2328 . . . . . . . . . . . . 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 ) ) )
330329sumeq2dv 12192 . . . . . . . . . . . 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 ) ) )
331 nnuz 10279 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
332 1e0p1 10168 . . . . . . . . . . . . . . . 16  |-  1  =  ( 0  +  1 )
333332fveq2i 5544 . . . . . . . . . . . . . . 15  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
334331, 333eqtri 2316 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  ( 0  +  1 ) )
335 oveq1 5881 . . . . . . . . . . . . . . 15  |-  ( n  =  ( 1  +  m )  ->  (
n  -  1 )  =  ( ( 1  +  m )  - 
1 ) )
336335oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( n  =  ( 1  +  m )  ->  (
y ^ ( n  -  1 ) )  =  ( y ^
( ( 1  +  m )  -  1 ) ) )
337 1z 10069 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
338337a1i 10 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  e.  ZZ )
3392a1i 10 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  0  e.  ZZ )
3401, 334, 336, 338, 339, 327isumshft 12314 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ ( ( 1  +  m )  - 
1 ) ) )
341 pncan2 9074 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  m  e.  CC )  ->  ( ( 1  +  m )  -  1 )  =  m )
34251, 104, 341sylancr 644 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( 1  +  m )  -  1 )  =  m )
343342oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( y ^ ( ( 1  +  m )  - 
1 ) )  =  ( y ^ m
) )
344343sumeq2i 12188 . . . . . . . . . . . . 13  |-  sum_ m  e.  NN0  ( y ^
( ( 1  +  m )  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m )
345340, 344syl6eq 2344 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ n  e.  NN  ( y ^
( n  -  1 ) )  =  sum_ m  e.  NN0  ( y ^ m ) )
346 geoisum 12349 . . . . . . . . . . . . 13  |-  ( ( y  e.  CC  /\  ( abs `  y )  <  1 )  ->  sum_ m  e.  NN0  (
y ^ m )  =  ( 1  / 
( 1  -  y
) ) )
34754, 67, 346syl2anc 642 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  sum_ m  e. 
NN0  ( y ^
m )  =  ( 1  /  ( 1  -  y ) ) )
348330, 345, 3473eqtrd 2332 . . . . . . . . . . 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
) ) )
349348mpteq2ia 4118 . . . . . . . . . 10  |-  ( y  e.  ( 0 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  sum_ n  e.  NN  ( ( n  x.  ( ( m  e. 
NN0  |->  if ( m  =  0 ,