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

Theorem efrlim 20810
Description: The limit of the sequence  ( 1  +  A  /  k
) ^ k is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 20811). (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypothesis
Ref Expression
efrlim.1  |-  S  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) )
Assertion
Ref Expression
efrlim  |-  ( A  e.  CC  ->  (
k  e.  RR+  |->  ( ( 1  +  ( A  /  k ) )  ^ c  k ) )  ~~> r  ( exp `  A ) )
Distinct variable group:    A, k
Allowed substitution hint:    S( k)

Proof of Theorem efrlim
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 9093 . . . . . . . . 9  |-  0  e.  RR
2 pnfxr 10715 . . . . . . . . 9  |-  +oo  e.  RR*
3 icossre 10993 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
41, 2, 3mp2an 655 . . . . . . . 8  |-  ( 0 [,)  +oo )  C_  RR
5 ax-resscn 9049 . . . . . . . 8  |-  RR  C_  CC
64, 5sstri 3359 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  CC
76sseli 3346 . . . . . 6  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  CC )
8 simpll 732 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  A  e.  CC )
9 ax-1cn 9050 . . . . . . . . . . . 12  |-  1  e.  CC
109a1i 11 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  e.  CC )
11 simplr 733 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  e.  CC )
12 ax-1ne0 9061 . . . . . . . . . . . 12  |-  1  =/=  0
1312a1i 11 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  =/=  0 )
14 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  -.  x  =  0 )
1514neneqad 2676 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  =/=  0 )
168, 10, 11, 13, 15divdiv2d 9824 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( ( A  x.  x )  /  1
) )
17 mulcl 9076 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( A  x.  x
)  e.  CC )
1817adantr 453 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  x.  x )  e.  CC )
1918div1d 9784 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( A  x.  x
)  /  1 )  =  ( A  x.  x ) )
2016, 19eqtrd 2470 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( A  x.  x
) )
2120oveq2d 6099 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  /  ( 1  /  x ) ) )  =  ( 1  +  ( A  x.  x
) ) )
2221oveq1d 6098 . . . . . . 7  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
2322ifeq2da 3767 . . . . . 6  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) )  =  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )
247, 23sylan2 462 . . . . 5  |-  ( ( A  e.  CC  /\  x  e.  ( 0 [,)  +oo ) )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) )  =  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )
2524mpteq2dva 4297 . . . 4  |-  ( A  e.  CC  ->  (
x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) ) )  =  ( x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) )
26 resmpt 5193 . . . . 5  |-  ( ( 0 [,)  +oo )  C_  CC  ->  ( (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  (
0 [,)  +oo ) )  =  ( x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) )
276, 26ax-mp 8 . . . 4  |-  ( ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  (
0 [,)  +oo ) )  =  ( x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )
2825, 27syl6eqr 2488 . . 3  |-  ( A  e.  CC  ->  (
x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) ) )  =  ( ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  (
0 [,)  +oo ) ) )
296a1i 11 . . . 4  |-  ( A  e.  CC  ->  (
0 [,)  +oo )  C_  CC )
30 0le0 10083 . . . . . 6  |-  0  <_  0
31 elrege0 11009 . . . . . 6  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
321, 30, 31mpbir2an 888 . . . . 5  |-  0  e.  ( 0 [,)  +oo )
3332a1i 11 . . . 4  |-  ( A  e.  CC  ->  0  e.  ( 0 [,)  +oo ) )
34 eqeq2 2447 . . . . . . . . 9  |-  ( ( exp `  ( A  x.  1 ) )  =  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x
) ) )  / 
( A  x.  x
) ) ) ) )  ->  ( if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  1 ) )  <->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  if ( ( A  x.  x
)  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) ) )
35 eqeq2 2447 . . . . . . . . 9  |-  ( ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) ) )  =  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) ) ) )  ->  ( if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  <->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  if ( ( A  x.  x
)  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) ) )
36 efrlim.1 . . . . . . . . . . . . . 14  |-  S  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) )
37 cnxmet 18809 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
3837a1i 11 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
39 0cn 9086 . . . . . . . . . . . . . . . 16  |-  0  e.  CC
4039a1i 11 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  0  e.  CC )
41 abscl 12085 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
42 peano2re 9241 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs `  A )  e.  RR  ->  (
( abs `  A
)  +  1 )  e.  RR )
4341, 42syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  (
( abs `  A
)  +  1 )  e.  RR )
441a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  0  e.  RR )
45 absge0 12094 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  0  <_  ( abs `  A
) )
4641ltp1d 9943 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  < 
( ( abs `  A
)  +  1 ) )
4744, 41, 43, 45, 46lelttrd 9230 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  0  <  ( ( abs `  A
)  +  1 ) )
4843, 47elrpd 10648 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  (
( abs `  A
)  +  1 )  e.  RR+ )
4948rpreccld 10660 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR+ )
5049rpxrd 10651 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR* )
51 blssm 18450 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  C_  CC )
5238, 40, 50, 51syl3anc 1185 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  C_  CC )
5336, 52syl5eqss 3394 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  S  C_  CC )
5453sselda 3350 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  CC )
55 mul0or 9664 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5654, 55syldan 458 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5756biimpa 472 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  ( A  =  0  \/  x  =  0 ) )
58 simpl 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  A  e.  CC )
5958, 54jca 520 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  e.  CC  /\  x  e.  CC ) )
6011, 15reccld 9785 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6159, 60sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6261adantlr 697 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  /  x )  e.  CC )
63621cxpd 20600 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  ^ c  ( 1  /  x ) )  =  1 )
64 simplr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  A  = 
0 )
6564oveq1d 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  ( 0  x.  x ) )
6654ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  x  e.  CC )
6766mul02d 9266 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 0  x.  x )  =  0 )
6865, 67eqtrd 2470 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  0 )
6968oveq2d 6099 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 ) )
709addid1i 9255 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  0 )  =  1
7169, 70syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  1 )
7271oveq1d 6098 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( 1  ^ c  ( 1  /  x ) ) )
7364fveq2d 5734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  ( exp `  0 ) )
74 ef0 12695 . . . . . . . . . . . . . . . 16  |-  ( exp `  0 )  =  1
7573, 74syl6eq 2486 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  1 )
7663, 72, 753eqtr4d 2480 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( exp `  A
) )
7776ifeq2da 3767 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  if ( x  =  0 ,  ( exp `  A
) ,  ( exp `  A ) ) )
78 ifid 3773 . . . . . . . . . . . . 13  |-  if ( x  =  0 ,  ( exp `  A
) ,  ( exp `  A ) )  =  ( exp `  A
)
7977, 78syl6eq 2486 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
80 iftrue 3747 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
8180adantl 454 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  x  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
8279, 81jaodan 762 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
83 mulid1 9090 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
8483ad2antrr 708 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( A  x.  1 )  =  A )
8584fveq2d 5734 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( exp `  ( A  x.  1 ) )  =  ( exp `  A ) )
8682, 85eqtr4d 2473 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  1 ) ) )
8757, 86syldan 458 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  1 ) ) )
88 mulne0b 9665 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
8954, 88syldan 458 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
90 df-ne 2603 . . . . . . . . . . . 12  |-  ( ( A  x.  x )  =/=  0  <->  -.  ( A  x.  x )  =  0 )
9189, 90syl6bb 254 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  -.  ( A  x.  x )  =  0 ) )
92 simprr 735 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  =/=  0 )
9392neneqd 2619 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  -.  x  =  0
)
94 iffalse 3748 . . . . . . . . . . . . . 14  |-  ( -.  x  =  0  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
9593, 94syl 16 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
9654, 17syldan 458 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  x.  x
)  e.  CC )
97 addcl 9074 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( 1  +  ( A  x.  x
) )  e.  CC )
989, 96, 97sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  CC )
9998adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  e.  CC )
100 eqid 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
101100dvlog2lem 20545 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
102 eqid 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
103102logdmss 20535 . . . . . . . . . . . . . . . . . 18  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
104101, 103sstri 3359 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
105 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
106105cnmetdval 18807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  +  ( A  x.  x ) )  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( 1  +  ( A  x.  x
) )  -  1 ) ) )
10798, 9, 106sylancl 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( 1  +  ( A  x.  x
) )  -  1 ) ) )
108 pncan2 9314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( ( 1  +  ( A  x.  x ) )  - 
1 )  =  ( A  x.  x ) )
1099, 96, 108sylancr 646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  -  1 )  =  ( A  x.  x ) )
110109fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
( 1  +  ( A  x.  x ) )  -  1 ) )  =  ( abs `  ( A  x.  x
) ) )
111107, 110eqtrd 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( A  x.  x
) ) )
11296abscld 12240 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  e.  RR )
11343adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  +  1 )  e.  RR )
11454abscld 12240 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  e.  RR )
115113, 114remulcld 9118 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  e.  RR )
116 1re 9092 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  RR
117116a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  RR )
118 absmul 12101 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
11954, 118syldan 458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
12041adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  A
)  e.  RR )
121120, 42syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  +  1 )  e.  RR )
12254absge0d 12248 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <_  ( abs `  x ) )
123120lep1d 9944 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  A
)  <_  ( ( abs `  A )  +  1 ) )
124120, 121, 114, 122, 123lemul1ad 9952 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  x.  ( abs `  x ) )  <_ 
( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) ) )
125119, 124eqbrtrd 4234 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <_  ( (
( abs `  A
)  +  1 )  x.  ( abs `  x
) ) )
126105cnmetdval 18807 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  CC  /\  0  e.  CC )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12754, 39, 126sylancl 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12854subid1d 9402 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x  -  0 )  =  x )
129128fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
x  -  0 ) )  =  ( abs `  x ) )
130127, 129eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  x ) )
131 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  S )
132131, 36syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) ) )
13337a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
13450adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  /  (
( abs `  A
)  +  1 ) )  e.  RR* )
13539a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  e.  CC )
136 elbl3 18424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  ( 1  / 
( ( abs `  A
)  +  1 ) )  e.  RR* )  /\  ( 0  e.  CC  /\  x  e.  CC ) )  ->  ( x  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) )  <->  ( x
( abs  o.  -  )
0 )  <  (
1  /  ( ( abs `  A )  +  1 ) ) ) )
137133, 134, 135, 54, 136syl22anc 1186 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  <->  ( x
( abs  o.  -  )
0 )  <  (
1  /  ( ( abs `  A )  +  1 ) ) ) )
138132, 137mpbid 203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
139130, 138eqbrtrrd 4236 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
14047adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <  ( ( abs `  A )  +  1 ) )
141 ltmuldiv2 9883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( abs `  x
)  e.  RR  /\  1  e.  RR  /\  (
( ( abs `  A
)  +  1 )  e.  RR  /\  0  <  ( ( abs `  A
)  +  1 ) ) )  ->  (
( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  <  1  <->  ( abs `  x
)  <  ( 1  /  ( ( abs `  A )  +  1 ) ) ) )
142114, 117, 121, 140, 141syl112anc 1189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( ( abs `  A )  +  1 )  x.  ( abs `  x
) )  <  1  <->  ( abs `  x )  <  ( 1  / 
( ( abs `  A
)  +  1 ) ) ) )
143139, 142mpbird 225 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  <  1 )
144112, 115, 117, 125, 143lelttrd 9230 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <  1 )
145111, 144eqbrtrd 4234 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  <  1 )
146 1rp 10618 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
147 rpxr 10621 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
148146, 147mp1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  RR* )
1499a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  CC )
150 elbl3 18424 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  RR* )  /\  ( 1  e.  CC  /\  ( 1  +  ( A  x.  x ) )  e.  CC ) )  -> 
( ( 1  +  ( A  x.  x
) )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( (
1  +  ( A  x.  x ) ) ( abs  o.  -  ) 1 )  <  1 ) )
151133, 148, 149, 98, 150syl22anc 1186 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  <->  ( (
1  +  ( A  x.  x ) ) ( abs  o.  -  ) 1 )  <  1 ) )
152145, 151mpbird 225 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
153104, 152sseldi 3348 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( CC 
\  { 0 } ) )
154 eldifsni 3930 . . . . . . . . . . . . . . . 16  |-  ( ( 1  +  ( A  x.  x ) )  e.  ( CC  \  { 0 } )  ->  ( 1  +  ( A  x.  x
) )  =/=  0
)
155153, 154syl 16 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  =/=  0 )
156155adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  =/=  0 )
15754adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  e.  CC )
158157, 92reccld 9785 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  e.  CC )
15999, 156, 158cxpefd 20605 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( 1  +  ( A  x.  x
) )  ^ c 
( 1  /  x
) )  =  ( exp `  ( ( 1  /  x )  x.  ( log `  (
1  +  ( A  x.  x ) ) ) ) ) )
16098, 155logcld 20470 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
161160adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
162158, 161mulcomd 9111 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( 1  /  x )  x.  ( log `  ( 1  +  ( A  x.  x
) ) ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  x.  (
1  /  x ) ) )
163 simpll 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  e.  CC )
164 simprl 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  =/=  0 )
165163, 164dividd 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  /  A
)  =  1 )
166165oveq1d 6098 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( 1  /  x ) )
167163, 163, 157, 164, 92divdiv1d 9823 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( A  /  ( A  x.  x ) ) )
168166, 167eqtr3d 2472 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  =  ( A  /  ( A  x.  x ) ) )
169168oveq2d 6099 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( log `  (
1  +  ( A  x.  x ) ) )  x.  ( 1  /  x ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  x.  ( A  /  ( A  x.  x ) ) ) )
17096adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  e.  CC )
17189biimpa 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  =/=  0 )
172161, 163, 170, 171div12d 9828 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( log `  (
1  +  ( A  x.  x ) ) )  x.  ( A  /  ( A  x.  x ) ) )  =  ( A  x.  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )
173162, 169, 1723eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( 1  /  x )  x.  ( log `  ( 1  +  ( A  x.  x
) ) ) )  =  ( A  x.  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )
174173fveq2d 5734 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( exp `  (
( 1  /  x
)  x.  ( log `  ( 1  +  ( A  x.  x ) ) ) ) )  =  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x
) ) )  / 
( A  x.  x
) ) ) ) )
17595, 159, 1743eqtrd 2474 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
176175ex 425 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) )
17791, 176sylbird 228 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( -.  ( A  x.  x )  =  0  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) )
178177imp 420 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
17934, 35, 87, 178ifbothda 3771 . . . . . . . 8  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) )
180179mpteq2dva 4297 . . . . . . 7  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) ) )
181 resmpt 5193 . . . . . . . 8  |-  ( S 
C_  CC  ->  ( ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  =  ( x  e.  S  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) )
18253, 181syl 16 . . . . . . 7  |-  ( A  e.  CC  ->  (
( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  =  ( x  e.  S  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) )
1839a1i 11 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  1  e.  CC )
184160adantr 453 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( log `  ( 1  +  ( A  x.  x
) ) )  e.  CC )
18596adantr 453 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  e.  CC )
186 simpr 449 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  -.  ( A  x.  x
)  =  0 )
187186neneqad 2676 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  =/=  0 )
188184, 185, 187divcld 9792 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) )  e.  CC )
189183, 188ifclda 3768 . . . . . . . 8  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  e.  CC )
190 eqidd 2439 . . . . . . . 8  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
191 eqidd 2439 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  =  ( y  e.  CC  |->  ( exp `  ( A  x.  y
) ) ) )
192 oveq2 6091 . . . . . . . . . 10  |-  ( y  =  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) )  ->  ( A  x.  y )  =  ( A  x.  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
193192fveq2d 5734 . . . . . . . . 9  |-  ( y  =  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) )  ->  ( exp `  ( A  x.  y ) )  =  ( exp `  ( A  x.  if (
( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) )
194 oveq2 6091 . . . . . . . . . . 11  |-  ( if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  =  1  -> 
( A  x.  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  =  ( A  x.  1 ) )
195194fveq2d 5734 . . . . . . . . . 10  |-  ( if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  =  1  -> 
( exp `  ( A  x.  if (
( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  =  ( exp `  ( A  x.  1 ) ) )
196 oveq2 6091 . . . . . . . . . . 11  |-  ( if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) )  -> 
( A  x.  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  =  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )
197196fveq2d 5734 . . . . . . . . . 10  |-  ( if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) )  -> 
( exp `  ( A  x.  if (
( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  =  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) ) ) )
198195, 197ifsb 3750 . . . . . . . . 9  |-  ( exp `  ( A  x.  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  =  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) ) ) )
199193, 198syl6eq 2486 . . . . . . . 8  |-  ( y  =  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) )  ->  ( exp `  ( A  x.  y ) )  =  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) ) ) ) )
200189, 190, 191, 199fmptco 5903 . . . . . . 7  |-  ( A  e.  CC  ->  (
( y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  o.  ( x  e.  S  |->  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  ( exp `  ( A  x.  1 ) ) ,  ( exp `  ( A  x.  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) ) )
201180, 182, 2003eqtr4d 2480 . . . . . 6  |-  ( A  e.  CC  ->  (
( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  =  ( ( y  e.  CC  |->  ( exp `  ( A  x.  y
) ) )  o.  ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) ) )
202 eqidd 2439 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )
203 eqidd 2439 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  =  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  (
y  -  1 ) ) ) ) )
204 eqeq1 2444 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  =  1  <->  (
1  +  ( A  x.  x ) )  =  1 ) )
205 fveq2 5730 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  ( log `  y )  =  ( log `  (
1  +  ( A  x.  x ) ) ) )
206 oveq1 6090 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  -  1 )  =  ( ( 1  +  ( A  x.  x ) )  - 
1 ) )
207205, 206oveq12d 6101 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
( log `  y
)  /  ( y  -  1 ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  (
( 1  +  ( A  x.  x ) )  -  1 ) ) )
208204, 207ifbieq2d 3761 . . . . . . . . . 10  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  if ( y  =  1 ,  1 ,  ( ( log `  y
)  /  ( y  -  1 ) ) )  =  if ( ( 1  +  ( A  x.  x ) )  =  1 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( ( 1  +  ( A  x.  x ) )  - 
1 ) ) ) )
209152, 202, 203, 208fmptco 5903 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  o.  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )  =  ( x  e.  S  |->  if ( ( 1  +  ( A  x.  x ) )  =  1 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( ( 1  +  ( A  x.  x ) )  - 
1 ) ) ) ) )
21070eqeq2i 2448 . . . . . . . . . . . 12  |-  ( ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 )  <->  ( 1  +  ( A  x.  x ) )  =  1 )
211149, 96, 135addcand 9271 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  ( 1  +  0 )  <-> 
( A  x.  x
)  =  0 ) )
212210, 211syl5bbr 252 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  1  <-> 
( A  x.  x
)  =  0 ) )
213109oveq2d 6099 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( ( 1  +  ( A  x.  x ) )  -  1 ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x )
) )
214212, 213ifbieq2d 3761 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  if ( ( 1  +  ( A  x.  x ) )  =  1 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( ( 1  +  ( A  x.  x ) )  -  1 ) ) )  =  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )
215214mpteq2dva 4297 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( ( 1  +  ( A  x.  x
) )  =  1 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( ( 1  +  ( A  x.  x ) )  -  1 ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
216209, 215eqtrd 2470 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  o.  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )
217 eqid 2438 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
218 eqid 2438 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
219218cnfldtopon 18819 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
220219a1i 11 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  ( TopOpen
` fld
)  e.  (TopOn `  CC ) )
2219a1i 11 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  1  e.  CC )
222220, 220, 221cnmptc 17696 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  1 )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
223 id 21 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  A  e.  CC )
224220, 220, 223cnmptc 17696 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
225220cnmptid 17695 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  x )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
226218mulcn 18899 . . . . . . . . . . . . . . 15  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
227226a1i 11 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) ) )
228220, 224, 225, 227cnmpt12f 17700 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( A  x.  x ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
229218addcn 18897 . . . . . . . . . . . . . 14  |-  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
230229a1i 11 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) ) )
231220, 222, 228, 230cnmpt12f 17700 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
232217, 220, 53, 231cnmpt1res 17710 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  ( TopOpen
` fld
) ) )
233 eqid 2438 . . . . . . . . . . . . . 14  |-  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x
) ) )
234152, 233fmptd 5895 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) : S --> ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
235 frn 5599 . . . . . . . . . . . . 13  |-  ( ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) : S --> ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  ->  ran  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  C_  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )
236234, 235syl 16 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  ran  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  C_  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )
237 difss 3476 . . . . . . . . . . . . . 14  |-  ( CC 
\  { 0 } )  C_  CC
238104, 237sstri 3359 . . . . . . . . . . . . 13  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
239238a1i 11 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
240 cnrest2 17352 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  ran  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  C_  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  /\  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )  ->  ( ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( (
TopOpen ` fld )t  S )  Cn  ( TopOpen
` fld
) )  <->  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( (
TopOpen ` fld )t  S )  Cn  (
( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) ) )
241220, 236, 239, 240syl3anc 1185 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  ( TopOpen
` fld
) )  <->  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( (
TopOpen ` fld )t  S )  Cn  (
( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) ) )
242232, 241mpbid 203 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  (
( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) )
243 blcntr 18445 . . . . . . . . . . . . 13  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR+ )  ->  0  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) ) )
24438, 40, 49, 243syl3anc 1185 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  0  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) ) )
245244, 36syl6eleqr 2529 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  0  e.  S )
246 resttopon 17227 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
247219, 53, 246sylancr 646 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
248 toponuni 16994 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
249247, 248syl 16 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
250245, 249eleqtrd 2514 . . . . . . . . . 10  |-  ( A  e.  CC  ->  0  e.  U. ( ( TopOpen ` fld )t  S
) )
251 eqid 2438 . . . . . . . . . . 11  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
252251cncnpi 17344 . . . . . . . . . 10  |-  ( ( ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  (
( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) )  /\  0  e.  U. (
( TopOpen ` fld )t  S ) )  -> 
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( ( TopOpen
` fld
)t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `  0
) )
253242, 250, 252syl2anc 644 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S )  CnP  (
( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) ` 
0 ) )
254 cnex 9073 . . . . . . . . . . . 12  |-  CC  e.  _V
255254prid2 3915 . . . . . . . . . . 11  |-  CC  e.  { RR ,  CC }
256 logf1o 20464 . . . . . . . . . . . . . 14  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
257 f1of 5676 . . . . . . . . . . . . . 14  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
258256, 257ax-mp 8 . . . . . . . . . . . . 13  |-  log :
( CC  \  {
0 } ) --> ran 
log
259 logrncn 20462 . . . . . . . . . . . . . 14  |-  ( x  e.  ran  log  ->  x  e.  CC )
260259ssriv 3354 . . . . . . . . . . . . 13  |-  ran  log  C_  CC
261 fss 5601 . . . . . . . . . . . . 13  |-  ( ( log : ( CC 
\  { 0 } ) --> ran  log  /\  ran  log  C_  CC )  ->  log : ( CC  \  {
0 } ) --> CC )
262258, 260, 261mp2an 655 . . . . . . . . . . . 12  |-  log :
( CC  \  {
0 } ) --> CC
263 fssres 5612 . . . . . . . . . . . 12  |-  ( ( log : ( CC 
\  { 0 } ) --> CC  /\  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } ) )  ->  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC )
264262, 104, 263mp2an 655 . . . . . . . . . . 11  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC
265 blcntr 18445 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  CC  /\  1  e.  RR+ )  ->  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
26637, 9, 146, 265mp3an 1280 . . . . . . . . . . . . 13  |-  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
267 ovex 6108 . . . . . . . . . . . . . 14  |-  ( 1  /  y )  e. 
_V
268100dvlog2 20546 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  y
) )
269267, 268dmmpti 5576 . . . . . . . . . . . . 13  |-  dom  ( CC  _D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )
270266, 269eleqtrri 2511 . . . . . . . . . . . 12  |-  1  e.  dom  ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
271 eqid 2438 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
272268fveq1i 5731 . . . . . . . . . . . . . . . . 17  |-  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `  1
)  =  ( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )
273 oveq2 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  1  ->  (
1  /  y )  =  ( 1  / 
1 ) )
2749div1i 9744 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
275273, 274syl6eq 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  1  ->  (
1  /  y )  =  1 )
276 eqid 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( 1  / 
y ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) )
277 1ex 9088 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  _V
278275, 276, 277fvmpt 5808 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )  =  1 )
279266, 278ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )  =  1
280272, 279eqtr2i 2459 . . . . . . . . . . . . . . . 16  |-  1  =  ( ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `
 1 )
281280a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `
 1 ) )
282 fvres 5747 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  y
)  =  ( log `  y ) )
283 fvres 5747 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  ( log `  1 ) )
284266, 283mp1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  ( log `  1 ) )
285 log1 20482 . . . . . . . . . . . . . . . . . . 19  |-  ( log `  1 )  =  0
286284, 285syl6eq 2486 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  0 )
287282, 286oveq12d 6101 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  (
( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ` 
1 ) )  =  ( ( log `  y
)  -  0 ) )
288104sseli 3346 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  ( CC  \  { 0 } ) )
289 eldifsn 3929 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( CC  \  { 0 } )  <-> 
( y  e.  CC  /\  y  =/=  0 ) )
290288, 289sylib 190 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  CC  /\  y  =/=  0 ) )
291 logcl 20468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  CC  /\  y  =/=  0 )  -> 
( log `  y
)  e.  CC )
292290, 291syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  y )  e.  CC )
293292subid1d 9402 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log `  y )  - 
0 )  =  ( log `  y ) )
294287, 293eqtr2d 2471 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  y )  =  ( ( ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  (
( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ` 
1 ) ) )
295294oveq1d 6098 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log `  y )  / 
( y  -  1 ) )  =  ( ( ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  1 ) )  /  ( y  -  1 ) ) )
296281, 295ifeq12d 3757 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  if (
y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) )  =  if ( y  =  1 ,  ( ( CC  _D  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) ` 
1 ) ,  ( ( ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  1 ) )  /  ( y  -  1 ) ) ) )
297296mpteq2ia 4293 . . . . . . . . . . . . 13  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  (
y  -  1 ) ) ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `
 1 ) ,  ( ( ( ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  (
( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ` 
1 ) )  / 
( y  -  1 ) ) ) )
298271, 218, 297dvcnp 19807 . . . . . . . . . . . 12  |-  ( ( ( CC  e.  { RR ,  CC }  /\  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC  /\  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )  /\  1  e.  dom  ( CC  _D  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) ) )  ->  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  if ( y  =  1 ,  1 ,  ( ( log `  y
)  /  ( y  -  1 ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  CnP  ( TopOpen ` fld ) ) `  1
) )
299270, 298mpan2 654 . . . . . . . . . . 11  |-  ( ( CC  e.  { RR ,  CC }  /\  ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC  /\  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
C_  CC )  -> 
( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) )  CnP  ( TopOpen
` fld
) ) `  1
) )
300255, 264, 238, 299mp3an 1280 . . . . . . . . . 10  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  (
y  -  1 ) ) ) )  e.  ( ( ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  CnP  ( TopOpen ` fld )
) `  1 )
301 oveq2 6091 . . . . . . . . . . . . . . 15  |-  ( x  =  0  ->  ( A  x.  x )  =  ( A  x.  0 ) )
302301oveq2d 6099 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  (
1  +  ( A  x.  x ) )  =  ( 1  +  ( A  x.  0 ) ) )
303 ovex 6108 . . . . . . . . . . . . . 14  |-  ( 1  +  ( A  x.  0 ) )  e. 
_V
304302, 233, 303fvmpt 5808 . . . . . . . . . . . . 13  |-  ( 0  e.  S  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  ( 1  +  ( A  x.  0 ) ) )
305245, 304syl 16 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  ( 1  +  ( A  x.  0 ) ) )
306 mul01 9247 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
307306oveq2d 6099 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  ( 1  +  0 ) )
308307, 70syl6eq 2486 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  1 )
309305, 308eqtrd 2470 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  1 )
310309fveq2d 5734 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
( ( ( TopOpen ` fld )t  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  CnP  ( TopOpen ` fld ) ) `  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
) )  =  ( ( ( ( TopOpen ` fld )t  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  CnP  ( TopOpen ` fld ) ) `  1
) )
311300, 310syl5eleqr 2525 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) )  CnP  ( TopOpen
` fld
) ) `  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
) ) )
312 cnpco 17333 . . . . . . . . 9  |-  ( ( ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( ( TopOpen
` fld
)t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `  0
)  /\  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  if ( y  =  1 ,  1 ,  ( ( log `  y
)  /  ( y  -  1 ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )  CnP  ( TopOpen ` fld ) ) `  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
) ) )  -> 
( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  if ( y  =  1 ,  1 ,  ( ( log `  y
)  /  ( y  -  1 ) ) ) )  o.  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( TopOpen ` fld )
) `  0 )
)
313253, 311, 312syl2anc 644 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  if ( y  =  1 ,  1 ,  ( ( log `  y )  /  ( y  - 
1 ) ) ) )  o.  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S )  CnP  ( TopOpen
` fld
) ) `  0
) )
314216, 313eqeltrrd 2513 . . . . . . 7  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( TopOpen ` fld )
) `  0 )
)
315220, 220, 223cnmptc 17696 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
316220cnmptid 17695 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  y )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
317220, 315, 316, 227cnmpt12f 17700 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( A  x.  y ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
318 efcn 20361 . . . . . . . . . . 11  |-  exp  e.  ( CC -cn-> CC )
319218cncfcn1 18942 . . . . . . . . . . 11  |-  ( CC
-cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
320318, 319eleqtri 2510 . . . . . . . . . 10  |-  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
321320a1i 11 . . . . . . . . 9  |-  ( A  e.  CC  ->  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
322220, 317, 321cnmpt11f 17698 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
323 eqid 2438 . . . . . . . . . 10  |-  ( x  e.  S  |->  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  =  ( x  e.  S  |->  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )
324189, 323fmptd 5895 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) : S --> CC )
325324, 245ffvelrnd 5873 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
)  e.  CC )
326219toponunii 16999 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
327326cncnpi 17344 . . . . . . . 8  |-  ( ( ( y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
)  /\  ( (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
)  e.  CC )  ->  ( y  e.  CC  |->  ( exp `  ( A  x.  y )
) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  ( (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
) ) )
328322, 325, 327syl2anc 644 . . . . . . 7  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  ( (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
) ) )
329 cnpco 17333 . . . . . . 7  |-  ( ( ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( TopOpen ` fld )
) `  0 )  /\  ( y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  ( (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
) ) )  -> 
( ( y  e.  CC  |->  ( exp `  ( A  x.  y )
) )  o.  (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  e.  ( ( ( (
TopOpen ` fld )t  S )  CnP  ( TopOpen
` fld
) ) `  0
) )
330314, 328, 329syl2anc 644 . . . . . 6  |-  ( A  e.  CC  ->  (
( y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  o.  ( x  e.  S  |->  if ( ( A  x.  x
)  =  0 ,  1 ,  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  S
)  CnP  ( TopOpen ` fld )
) `  0 )
)
331201, 330eqeltrd 2512 . . . . 5  |-  ( A  e.  CC  ->  (
( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  e.  ( ( ( ( TopOpen ` fld )t  S )  CnP  ( TopOpen
` fld
) ) `  0
) )
332218cnfldtop 18820 . . . . . . 7  |-  ( TopOpen ` fld )  e.  Top
333332a1i 11 . . . . . 6  |-  ( A  e.  CC  ->  ( TopOpen
` fld
)  e.  Top )
334218cnfldtopn 18818 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
335334blopn 18532 . . . . . . . . . 10  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  0  e.  CC  /\  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR* )  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  e.  (
TopOpen ` fld ) )
33638, 40, 50, 335syl3anc 1185 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  e.  (
TopOpen ` fld ) )
33736, 336syl5eqel 2522 . . . . . . . 8  |-  ( A  e.  CC  ->  S  e.  ( TopOpen ` fld ) )
338 isopn3i 17148 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  ( TopOpen ` fld )
)  ->  ( ( int `  ( TopOpen ` fld ) ) `  S
)  =  S )
339332, 337, 338sylancr 646 . . . . . . 7  |-  ( A  e.  CC  ->  (
( int `  ( TopOpen
` fld
) ) `  S
)  =  S )
340245, 339eleqtrrd 2515 . . . . . 6  |-  ( A  e.  CC  ->  0  e.  ( ( int `  ( TopOpen
` fld
) ) `  S
) )
341 efcl 12687 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( exp `  A )  e.  CC )
342341ad2antrr 708 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  x  =  0 )  ->  ( exp `  A )  e.  CC )
3439, 18, 97sylancr 646 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  x.  x ) )  e.  CC )
344343, 60cxpcld 20601 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  e.  CC )
345342, 344ifclda 3768 . . . . . . 7  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  e.  CC )
346 eqid 2438 . . . . . . 7  |-  ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  =  ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )
347345, 346fmptd 5895 . . . . . 6  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) : CC --> CC )
348326, 326cnprest 17355 . . . . . 6  |-  ( ( ( ( TopOpen ` fld )  e.  Top  /\  S  C_  CC )  /\  ( 0  e.  ( ( int `  ( TopOpen
` fld
) ) `  S
)  /\  ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) : CC --> CC ) )  ->  ( (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  0 )  <->  ( ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  e.  ( ( ( ( TopOpen ` fld )t  S )  CnP  ( TopOpen
` fld
) ) `  0
) ) )
349333, 53, 340, 347, 348syl22anc 1186 . . . . 5  |-  ( A  e.  CC  ->  (
( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  0 )  <->  ( ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  S )  e.  ( ( ( ( TopOpen ` fld )t  S )  CnP  ( TopOpen
` fld
) ) `  0
) ) )
350331, 349mpbird 225 . . . 4  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  0 )
)
351326cnpresti 17354 . . . 4  |-  ( ( ( 0 [,)  +oo )  C_  CC  /\  0  e.  ( 0 [,)  +oo )  /\  ( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( TopOpen ` fld )  CnP  ( TopOpen ` fld )
) `  0 )
)  ->  ( (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  (
0 [,)  +oo ) )  e.  ( ( ( ( TopOpen ` fld )t  ( 0 [,) 
+oo ) )  CnP  ( TopOpen ` fld ) ) `  0
) )
35229, 33, 350, 351syl3anc 1185 . . 3  |-  ( A  e.  CC  ->  (
( x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) )  |`  (
0 [,)  +oo ) )  e.  ( ( ( ( TopOpen ` fld )t  ( 0 [,) 
+oo ) )  CnP  ( TopOpen ` fld ) ) `  0
) )
35328, 352eqeltrd 2512 . 2  |-  ( A  e.  CC  ->  (
x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
0 [,)  +oo ) )  CnP  ( TopOpen ` fld ) ) `  0
) )
354 simpl 445 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  ->  A  e.  CC )
355 rpcn 10622 . . . . . . 7  |-  ( k  e.  RR+  ->  k  e.  CC )
356355adantl 454 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  e.  CC )
357 rpne0 10629 . . . . . . 7  |-  ( k  e.  RR+  ->  k  =/=  0 )
358357adantl 454 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  =/=  0 )
359354, 356, 358divcld 9792 . . . . 5  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( A  /  k
)  e.  CC )
360 addcl 9074 . . . . 5  |-  ( ( 1  e.  CC  /\  ( A  /  k
)  e.  CC )  ->  ( 1  +  ( A  /  k
) )  e.  CC )
3619, 359, 360sylancr 646 . . . 4  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( 1  +  ( A  /  k ) )  e.  CC )
362361, 356cxpcld 20601 . . 3  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( ( 1  +  ( A  /  k
) )  ^ c 
k )  e.  CC )
363 oveq2 6091 . . . . 5  |-  ( k  =  ( 1  /  x )  ->  ( A  /  k )  =  ( A  /  (
1  /  x ) ) )
364363oveq2d 6099 . . . 4  |-  ( k  =  ( 1  /  x )  ->  (
1  +  ( A  /  k ) )  =  ( 1  +  ( A  /  (
1  /  x ) ) ) )
365 id 21 . . . 4  |-  ( k  =  ( 1  /  x )  ->  k  =  ( 1  /  x ) )
366364, 365oveq12d 6101 . . 3  |-  ( k  =  ( 1  /  x )  ->  (
( 1  +  ( A  /  k ) )  ^ c  k )  =  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) )
367 eqid 2438 . . 3  |-  ( (
TopOpen ` fld )t  ( 0 [,)  +oo ) )  =  ( ( TopOpen ` fld )t  ( 0 [,) 
+oo ) )
368341, 362, 366, 218, 367rlimcnp3 20808 . 2  |-  ( A  e.  CC  ->  (
( k  e.  RR+  |->  ( ( 1  +  ( A  /  k
) )  ^ c 
k ) )  ~~> r  ( exp `  A )  <-> 
( x  e.  ( 0 [,)  +oo )  |->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) ) )  e.  ( ( ( (
TopOpen ` fld