Metamath Proof Explorer

Theorem logtayl

Description: The Taylor series for -u log ( 1 - A ) . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logtayl 
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 0zd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3 eqeq1 
 |-  ( k = n -> ( k = 0 <-> n = 0 ) )
4 oveq2 
 |-  ( k = n -> ( 1 / k ) = ( 1 / n ) )
5 3 4 ifbieq2d 
 |-  ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
6 oveq2 
 |-  ( k = n -> ( A ^ k ) = ( A ^ n ) )
7 5 6 oveq12d 
 |-  ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
8 eqid 
 |-  ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) = ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
9 ovex 
 |-  ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( 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 ) ) )
11 10 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
12 0cnd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
13 simpr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
14 elnn0 
 |-  ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
15 13 14 sylib 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
16 15 ord 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
17 16 con1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
18 17 imp 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
19 18 nnrecred 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
20 19 recnd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
21 12 20 ifclda 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
22 expcl 
 |-  ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
23 22 adantlr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
24 21 23 mulcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
25 logtayllem 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. dom ~~> )
26 1 2 11 24 25 isumclim2 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
27 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
28 0cn 
 |-  0 e. CC
29 eqid 
 |-  ( abs o. - ) = ( abs o. - )
30 29 cnmetdval 
 |-  ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
31 27 28 30 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32 subid1 
 |-  ( A e. CC -> ( A - 0 ) = A )
33 32 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
34 33 fveq2d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
35 31 34 eqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
36 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
37 35 36 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
38 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
39 1xr 
 |-  1 e. RR*
40 elbl3 
 |-  ( ( ( ( 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 ) )
41 38 39 40 mpanl12 
 |-  ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
42 28 27 41 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
43 37 42 mpbird 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
44 tru 
 |-  T.
45 eqid 
 |-  ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
46 0cnd 
 |-  ( T. -> 0 e. CC )
47 39 a1i 
 |-  ( T. -> 1 e. RR* )
48 ax-1cn 
 |-  1 e. CC
49 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
50 38 28 39 49 mp3an 
 |-  ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
51 50 sseli 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
52 subcl 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
53 48 51 52 sylancr 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
54 51 abscld 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
55 29 cnmetdval 
 |-  ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
56 51 28 55 sylancl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
57 51 subid1d 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
58 57 fveq2d 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
59 56 58 eqtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
60 elbl3 
 |-  ( ( ( ( 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 ) )
61 38 39 60 mpanl12 
 |-  ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
62 28 51 61 sylancr 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
63 62 ibi 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
64 59 63 eqbrtrrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
65 54 64 gtned 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
66 abs1 
 |-  ( abs ` 1 ) = 1
67 fveq2 
 |-  ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
68 66 67 eqtr3id 
 |-  ( 1 = y -> 1 = ( abs ` y ) )
69 68 necon3i 
 |-  ( 1 =/= ( abs ` y ) -> 1 =/= y )
70 65 69 syl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
71 subeq0 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
72 71 necon3bid 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
73 48 51 72 sylancr 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
74 70 73 mpbird 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
75 53 74 logcld 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
76 75 negcld 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
77 76 adantl 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
78 77 fmpttd 
 |-  ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
79 51 absge0d 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
80 54 rexrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
81 peano2re 
 |-  ( ( abs ` y ) e. RR -> ( ( abs ` y ) + 1 ) e. RR )
82 54 81 syl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) + 1 ) e. RR )
83 82 rehalfcld 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
84 83 rexrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
85 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
86 eqeq1 
 |-  ( m = j -> ( m = 0 <-> j = 0 ) )
87 oveq2 
 |-  ( m = j -> ( 1 / m ) = ( 1 / j ) )
88 86 87 ifbieq2d 
 |-  ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
89 eqid 
 |-  ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) )
90 c0ex 
 |-  0 e. _V
91 ovex 
 |-  ( 1 / j ) e. _V
92 90 91 ifex 
 |-  if ( j = 0 , 0 , ( 1 / j ) ) e. _V
93 88 89 92 fvmpt 
 |-  ( j e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
94 93 eqcomd 
 |-  ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
95 94 oveq1d 
 |-  ( 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 ) ) )
96 95 mpteq2ia 
 |-  ( 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 ) ) )
97 96 mpteq2i 
 |-  ( 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 ) ) ) )
98 0cnd 
 |-  ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
99 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
100 99 adantl 
 |-  ( ( T. /\ m e. NN0 ) -> m e. CC )
101 neqne 
 |-  ( -. m = 0 -> m =/= 0 )
102 reccl 
 |-  ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
103 100 101 102 syl2an 
 |-  ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
104 98 103 ifclda 
 |-  ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
105 104 fmpttd 
 |-  ( T. -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
106 recn 
 |-  ( r e. RR -> r e. CC )
107 oveq1 
 |-  ( x = r -> ( x ^ j ) = ( r ^ j ) )
108 107 oveq2d 
 |-  ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
109 108 mpteq2dv 
 |-  ( 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 ) ) ) )
110 eqid 
 |-  ( 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 ) ) ) )
111 nn0ex 
 |-  NN0 e. _V
112 111 mptex 
 |-  ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
113 109 110 112 fvmpt 
 |-  ( 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 ) ) ) )
114 106 113 syl 
 |-  ( 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 ) ) ) )
115 114 eqcomd 
 |-  ( 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 ) )
116 115 seqeq3d 
 |-  ( 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 ) ) )
117 116 eleq1d 
 |-  ( 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 ~~> ) )
118 117 rabbiia 
 |-  { 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 ~~> }
119 118 supeq1i 
 |-  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* , < )
120 97 105 119 radcnvcl 
 |-  ( 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 ) )
121 85 120 sselid 
 |-  ( T. -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
122 44 121 mp1i 
 |-  ( 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* )
123 1re 
 |-  1 e. RR
124 avglt1 
 |-  ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
125 54 123 124 sylancl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
126 64 125 mpbid 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
127 0red 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
128 127 54 83 79 126 lelttrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
129 127 83 128 ltled 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
130 83 129 absidd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( ( ( abs ` y ) + 1 ) / 2 ) )
131 44 105 mp1i 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
132 83 recnd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
133 oveq1 
 |-  ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
134 133 oveq2d 
 |-  ( 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 ) ) )
135 134 mpteq2dv 
 |-  ( 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 ) ) ) )
136 111 mptex 
 |-  ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
137 135 110 136 fvmpt 
 |-  ( ( ( ( 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 ) ) ) )
138 132 137 syl 
 |-  ( 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 ) ) ) )
139 138 seqeq3d 
 |-  ( 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 ) ) ) ) )
140 avglt2 
 |-  ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
141 54 123 140 sylancl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
142 64 141 mpbid 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
143 130 142 eqbrtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
144 logtayllem 
 |-  ( ( ( ( ( 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 ~~> )
145 132 143 144 syl2anc 
 |-  ( 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 ~~> )
146 139 145 eqeltrd 
 |-  ( 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 ~~> )
147 97 131 119 132 146 radcnvle 
 |-  ( 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* , < ) )
148 130 147 eqbrtrrd 
 |-  ( 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* , < ) )
149 80 84 122 126 148 xrltletrd 
 |-  ( 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* , < ) )
150 0re 
 |-  0 e. RR
151 elico2 
 |-  ( ( 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* , < ) ) ) )
152 150 122 151 sylancr 
 |-  ( 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* , < ) ) ) )
153 54 79 149 152 mpbir3and 
 |-  ( 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* , < ) ) )
154 absf 
 |-  abs : CC --> RR
155 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
156 elpreima 
 |-  ( 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* , < ) ) ) ) )
157 154 155 156 mp2b 
 |-  ( 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* , < ) ) ) )
158 51 153 157 sylanbrc 
 |-  ( 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* , < ) ) ) )
159 cnvimass 
 |-  ( `' 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
160 154 fdmi 
 |-  dom abs = CC
161 159 160 sseqtri 
 |-  ( `' 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
162 161 sseli 
 |-  ( 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 )
163 oveq1 
 |-  ( x = y -> ( x ^ j ) = ( y ^ j ) )
164 163 oveq2d 
 |-  ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
165 164 mpteq2dv 
 |-  ( 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 ) ) ) )
166 111 mptex 
 |-  ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
167 165 110 166 fvmpt 
 |-  ( 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 ) ) ) )
168 167 adantr 
 |-  ( ( 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 ) ) ) )
169 168 fveq1d 
 |-  ( ( 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 ) )
170 eqeq1 
 |-  ( j = n -> ( j = 0 <-> n = 0 ) )
171 oveq2 
 |-  ( j = n -> ( 1 / j ) = ( 1 / n ) )
172 170 171 ifbieq2d 
 |-  ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
173 oveq2 
 |-  ( j = n -> ( y ^ j ) = ( y ^ n ) )
174 172 173 oveq12d 
 |-  ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
175 eqid 
 |-  ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
176 ovex 
 |-  ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
177 174 175 176 fvmpt 
 |-  ( 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 ) ) )
178 177 adantl 
 |-  ( ( 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 ) ) )
179 169 178 eqtr2d 
 |-  ( ( 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 ) )
180 179 sumeq2dv 
 |-  ( 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 ) )
181 162 180 syl 
 |-  ( 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 ) )
182 181 mpteq2ia 
 |-  ( 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 ) )
183 eqid 
 |-  ( `' 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* , < ) ) )
184 eqid 
 |-  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 ) )
185 97 182 105 119 183 184 psercn 
 |-  ( 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 ) )
186 cncff 
 |-  ( ( 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 )
187 185 186 syl 
 |-  ( 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 )
188 187 fvmptelcdm 
 |-  ( ( 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 )
189 158 188 sylan2 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
190 189 fmpttd 
 |-  ( 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 )
191 cnelprrecn 
 |-  CC e. { RR , CC }
192 191 a1i 
 |-  ( T. -> CC e. { RR , CC } )
193 75 adantl 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
194 ovexd 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V )
195 29 cnmetdval 
 |-  ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
196 48 53 195 sylancr 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
197 nncan 
 |-  ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
198 48 51 197 sylancr 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
199 198 fveq2d 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
200 196 199 eqtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
201 200 64 eqbrtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
202 elbl 
 |-  ( ( ( 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 ) ) )
203 38 48 39 202 mp3an 
 |-  ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
204 53 201 203 sylanbrc 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
205 204 adantl 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
206 neg1cn 
 |-  -u 1 e. CC
207 206 a1i 
 |-  ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
208 eqid 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
209 208 dvlog2lem 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
210 209 sseli 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
211 210 eldifad 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
212 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
213 212 logdmn0 
 |-  ( x e. ( CC \ ( -oo (,] 0 ) ) -> x =/= 0 )
214 210 213 syl 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x =/= 0 )
215 211 214 logcld 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
216 215 adantl 
 |-  ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
217 ovexd 
 |-  ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
218 simpr 
 |-  ( ( T. /\ y e. CC ) -> y e. CC )
219 48 218 52 sylancr 
 |-  ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
220 206 a1i 
 |-  ( ( T. /\ y e. CC ) -> -u 1 e. CC )
221 1cnd 
 |-  ( ( T. /\ y e. CC ) -> 1 e. CC )
222 0cnd 
 |-  ( ( T. /\ y e. CC ) -> 0 e. CC )
223 1cnd 
 |-  ( T. -> 1 e. CC )
224 192 223 dvmptc 
 |-  ( T. -> ( CC _D ( y e. CC |-> 1 ) ) = ( y e. CC |-> 0 ) )
225 192 dvmptid 
 |-  ( T. -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
226 192 221 222 224 218 221 225 dvmptsub 
 |-  ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> ( 0 - 1 ) ) )
227 df-neg 
 |-  -u 1 = ( 0 - 1 )
228 227 mpteq2i 
 |-  ( y e. CC |-> -u 1 ) = ( y e. CC |-> ( 0 - 1 ) )
229 226 228 eqtr4di 
 |-  ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> -u 1 ) )
230 50 a1i 
 |-  ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
231 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
232 231 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
233 232 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
234 231 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
235 234 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) )
236 38 28 39 235 mp3an 
 |-  ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld )
237 236 a1i 
 |-  ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) )
238 192 219 220 229 230 233 231 237 dvmptres 
 |-  ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u 1 ) )
239 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
240 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
241 239 240 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
242 212 logdmss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
243 209 242 sstri 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
244 fssres 
 |-  ( ( 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 )
245 241 243 244 mp2an 
 |-  ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log
246 245 a1i 
 |-  ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
247 246 feqmptd 
 |-  ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
248 fvres 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
249 248 mpteq2ia 
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) )
250 247 249 eqtrdi 
 |-  ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) )
251 250 oveq2d 
 |-  ( T. -> ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) )
252 208 dvlog2 
 |-  ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) )
253 251 252 eqtr3di 
 |-  ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) ) )
254 fveq2 
 |-  ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
255 oveq2 
 |-  ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
256 192 192 205 207 216 217 238 253 254 255 dvmptco 
 |-  ( 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 ) ) )
257 192 193 194 256 dvmptneg 
 |-  ( 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 ) ) )
258 53 74 reccld 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
259 mulcom 
 |-  ( ( ( 1 / ( 1 - y ) ) e. CC /\ -u 1 e. CC ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
260 258 206 259 sylancl 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
261 258 mulm1d 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
262 260 261 eqtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
263 262 negeqd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
264 258 negnegd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
265 263 264 eqtrd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
266 265 mpteq2ia 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) )
267 257 266 eqtrdi 
 |-  ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
268 267 dmeqd 
 |-  ( 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 ) ) ) )
269 dmmptg 
 |-  ( 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 ) )
270 ovexd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. _V )
271 269 270 mprg 
 |-  dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
272 268 271 eqtrdi 
 |-  ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
273 sumex 
 |-  sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V
274 273 a1i 
 |-  ( ( 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 )
275 fveq2 
 |-  ( 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 ) )
276 275 cbvsumv 
 |-  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 )
277 181 276 eqtrdi 
 |-  ( 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 ) )
278 277 mpteq2ia 
 |-  ( 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 ) )
279 eqid 
 |-  ( 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 ) )
280 97 278 105 119 183 184 279 pserdv2 
 |-  ( 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 ) ) ) ) )
281 158 ssriv 
 |-  ( 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* , < ) ) )
282 281 a1i 
 |-  ( 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* , < ) ) ) )
283 192 188 274 280 282 233 231 237 dvmptres 
 |-  ( 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 ) ) ) ) )
284 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
285 284 adantl 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
286 eqeq1 
 |-  ( m = n -> ( m = 0 <-> n = 0 ) )
287 oveq2 
 |-  ( m = n -> ( 1 / m ) = ( 1 / n ) )
288 286 287 ifbieq2d 
 |-  ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
289 ovex 
 |-  ( 1 / n ) e. _V
290 90 289 ifex 
 |-  if ( n = 0 , 0 , ( 1 / n ) ) e. _V
291 288 89 290 fvmpt 
 |-  ( n e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
292 285 291 syl 
 |-  ( ( 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 ) ) )
293 nnne0 
 |-  ( n e. NN -> n =/= 0 )
294 293 adantl 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
295 294 neneqd 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
296 295 iffalsed 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
297 292 296 eqtrd 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = ( 1 / n ) )
298 297 oveq2d 
 |-  ( ( 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 ) ) )
299 nncn 
 |-  ( n e. NN -> n e. CC )
300 299 adantl 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
301 300 294 recidd 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
302 298 301 eqtrd 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = 1 )
303 302 oveq1d 
 |-  ( ( 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 ) ) ) )
304 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
305 expcl 
 |-  ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
306 51 304 305 syl2an 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
307 306 mullidd 
 |-  ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
308 303 307 eqtrd 
 |-  ( ( 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 ) ) )
309 308 sumeq2dv 
 |-  ( 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 ) ) )
310 nnuz 
 |-  NN = ( ZZ>= ` 1 )
311 1e0p1 
 |-  1 = ( 0 + 1 )
312 311 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
313 310 312 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
314 oveq1 
 |-  ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
315 314 oveq2d 
 |-  ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
316 1zzd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
317 0zd 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
318 1 313 315 316 317 306 isumshft 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) )
319 pncan2 
 |-  ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
320 48 99 319 sylancr 
 |-  ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
321 320 oveq2d 
 |-  ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
322 321 sumeq2i 
 |-  sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
323 318 322 eqtrdi 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
324 geoisum 
 |-  ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
325 51 64 324 syl2anc 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
326 309 323 325 3eqtrd 
 |-  ( 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 ) ) )
327 326 mpteq2ia 
 |-  ( 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 ) ) )
328 283 327 eqtrdi 
 |-  ( 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 ) ) ) )
329 267 328 eqtr4d 
 |-  ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) )
330 1rp 
 |-  1 e. RR+
331 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR+ ) -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
332 38 28 330 331 mp3an 
 |-  0 e. ( 0 ( ball ` ( abs o. - ) ) 1 )
333 332 a1i 
 |-  ( T. -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
334 oveq2 
 |-  ( y = 0 -> ( 1 - y ) = ( 1 - 0 ) )
335 1m0e1 
 |-  ( 1 - 0 ) = 1
336 334 335 eqtrdi 
 |-  ( y = 0 -> ( 1 - y ) = 1 )
337 336 fveq2d 
 |-  ( y = 0 -> ( log ` ( 1 - y ) ) = ( log ` 1 ) )
338 log1 
 |-  ( log ` 1 ) = 0
339 337 338 eqtrdi 
 |-  ( y = 0 -> ( log ` ( 1 - y ) ) = 0 )
340 339 negeqd 
 |-  ( y = 0 -> -u ( log ` ( 1 - y ) ) = -u 0 )
341 neg0 
 |-  -u 0 = 0
342 340 341 eqtrdi 
 |-  ( y = 0 -> -u ( log ` ( 1 - y ) ) = 0 )
343 eqid 
 |-  ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) )
344 342 343 90 fvmpt 
 |-  ( 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
345 332 344 mp1i 
 |-  ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
346 oveq1 
 |-  ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( 0 x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
347 346 eqeq1d 
 |-  ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 0 x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
348 oveq1 
 |-  ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
349 348 eqeq1d 
 |-  ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( ( 1 / n ) x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
350 simpll 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y = 0 )
351 350 28 eqeltrdi 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y e. CC )
352 simplr 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> n e. NN0 )
353 351 352 expcld 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( y ^ n ) e. CC )
354 353 mul02d 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( 0 x. ( y ^ n ) ) = 0 )
355 simpll 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> y = 0 )
356 355 oveq1d 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = ( 0 ^ n ) )
357 simpr 
 |-  ( ( y = 0 /\ n e. NN0 ) -> n e. NN0 )
358 357 14 sylib 
 |-  ( ( y = 0 /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
359 358 ord 
 |-  ( ( y = 0 /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
360 359 con1d 
 |-  ( ( y = 0 /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
361 360 imp 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
362 361 0expd 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 0 ^ n ) = 0 )
363 356 362 eqtrd 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = 0 )
364 363 oveq2d 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( ( 1 / n ) x. 0 ) )
365 361 nnrecred 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
366 365 recnd 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
367 366 mul01d 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. 0 ) = 0 )
368 364 367 eqtrd 
 |-  ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = 0 )
369 347 349 354 368 ifbothda 
 |-  ( ( y = 0 /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
370 369 sumeq2dv 
 |-  ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 0 )
371 1 eqimssi 
 |-  NN0 C_ ( ZZ>= ` 0 )
372 371 orci 
 |-  ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin )
373 sumz 
 |-  ( ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin ) -> sum_ n e. NN0 0 = 0 )
374 372 373 ax-mp 
 |-  sum_ n e. NN0 0 = 0
375 370 374 eqtrdi 
 |-  ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
376 eqid 
 |-  ( 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 ) ) )
377 375 376 90 fvmpt 
 |-  ( 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) = 0 )
378 332 377 mp1i 
 |-  ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) = 0 )
379 345 378 eqtr4d 
 |-  ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) )
380 45 46 47 78 190 272 329 333 379 dv11cn 
 |-  ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) )
381 380 fveq1d 
 |-  ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` A ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) )
382 44 381 mp1i 
 |-  ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` A ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) )
383 oveq2 
 |-  ( y = A -> ( 1 - y ) = ( 1 - A ) )
384 383 fveq2d 
 |-  ( y = A -> ( log ` ( 1 - y ) ) = ( log ` ( 1 - A ) ) )
385 384 negeqd 
 |-  ( y = A -> -u ( log ` ( 1 - y ) ) = -u ( log ` ( 1 - A ) ) )
386 negex 
 |-  -u ( log ` ( 1 - A ) ) e. _V
387 385 343 386 fvmpt 
 |-  ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` A ) = -u ( log ` ( 1 - A ) ) )
388 oveq1 
 |-  ( y = A -> ( y ^ n ) = ( A ^ n ) )
389 388 oveq2d 
 |-  ( y = A -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
390 389 sumeq2sdv 
 |-  ( y = A -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
391 sumex 
 |-  sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
392 390 376 391 fvmpt 
 |-  ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
393 382 387 392 3eqtr3d 
 |-  ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
394 43 393 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
395 26 394 breqtrrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> -u ( log ` ( 1 - A ) ) )
396 seqex 
 |-  seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V
397 396 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V )
398 seqex 
 |-  seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) e. _V
399 398 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) e. _V )
400 1zzd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ZZ )
401 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
402 fvres 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) ` n ) = ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) )
403 401 402 sylbi 
 |-  ( n e. NN -> ( ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) ` n ) = ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) )
404 403 eqcomd 
 |-  ( n e. NN -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) = ( ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) ` n ) )
405 addlid 
 |-  ( n e. CC -> ( 0 + n ) = n )
406 405 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. CC ) -> ( 0 + n ) = n )
407 0cnd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. CC )
408 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
409 408 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ( ZZ>= ` 0 ) )
410 0cnd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ k = 0 ) -> 0 e. CC )
411 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
412 411 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> k e. CC )
413 neqne 
 |-  ( -. k = 0 -> k =/= 0 )
414 reccl 
 |-  ( ( k e. CC /\ k =/= 0 ) -> ( 1 / k ) e. CC )
415 412 413 414 syl2an 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ -. k = 0 ) -> ( 1 / k ) e. CC )
416 410 415 ifclda 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> if ( k = 0 , 0 , ( 1 / k ) ) e. CC )
417 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
418 417 adantlr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
419 416 418 mulcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. CC )
420 419 fmpttd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) : NN0 --> CC )
421 1nn0 
 |-  1 e. NN0
422 ffvelcdm 
 |-  ( ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) : NN0 --> CC /\ 1 e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 1 ) e. CC )
423 420 421 422 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 1 ) e. CC )
424 elfz1eq 
 |-  ( n e. ( 0 ... 0 ) -> n = 0 )
425 1m1e0 
 |-  ( 1 - 1 ) = 0
426 425 oveq2i 
 |-  ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
427 424 426 eleq2s 
 |-  ( n e. ( 0 ... ( 1 - 1 ) ) -> n = 0 )
428 427 fveq2d 
 |-  ( n e. ( 0 ... ( 1 - 1 ) ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) )
429 0nn0 
 |-  0 e. NN0
430 iftrue 
 |-  ( k = 0 -> if ( k = 0 , 0 , ( 1 / k ) ) = 0 )
431 oveq2 
 |-  ( k = 0 -> ( A ^ k ) = ( A ^ 0 ) )
432 430 431 oveq12d 
 |-  ( k = 0 -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( 0 x. ( A ^ 0 ) ) )
433 ovex 
 |-  ( 0 x. ( A ^ 0 ) ) e. _V
434 432 8 433 fvmpt 
 |-  ( 0 e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) ) )
435 429 434 ax-mp 
 |-  ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) )
436 expcl 
 |-  ( ( A e. CC /\ 0 e. NN0 ) -> ( A ^ 0 ) e. CC )
437 27 429 436 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 0 ) e. CC )
438 437 mul02d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 0 x. ( A ^ 0 ) ) = 0 )
439 435 438 eqtrid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = 0 )
440 428 439 sylan9eqr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = 0 )
441 406 407 409 423 440 seqid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) )
442 293 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n =/= 0 )
443 442 neneqd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> -. n = 0 )
444 443 iffalsed 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
445 444 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( 1 / n ) x. ( A ^ n ) ) )
446 284 23 sylan2 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( A ^ n ) e. CC )
447 299 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n e. CC )
448 446 447 442 divrec2d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( A ^ n ) / n ) = ( ( 1 / n ) x. ( A ^ n ) ) )
449 445 448 eqtr4d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( A ^ n ) / n ) )
450 284 11 sylan2 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
451 id 
 |-  ( k = n -> k = n )
452 6 451 oveq12d 
 |-  ( k = n -> ( ( A ^ k ) / k ) = ( ( A ^ n ) / n ) )
453 eqid 
 |-  ( k e. NN |-> ( ( A ^ k ) / k ) ) = ( k e. NN |-> ( ( A ^ k ) / k ) )
454 ovex 
 |-  ( ( A ^ n ) / n ) e. _V
455 452 453 454 fvmpt 
 |-  ( n e. NN -> ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
456 455 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
457 449 450 456 3eqtr4d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) )
458 401 457 sylan2br 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. ( ZZ>= ` 1 ) ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) )
459 400 458 seqfeq 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) = seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) )
460 441 459 eqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) )
461 460 fveq1d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) |` ( ZZ>= ` 1 ) ) ` n ) = ( seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ` n ) )
462 404 461 sylan9eqr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) = ( seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ` n ) )
463 310 397 399 400 462 climeq 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> -u ( log ` ( 1 - A ) ) <-> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) ) )
464 395 463 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )