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

Theorem efrlim 20676
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 20677). (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 9025 . . . . . . . . 9  |-  0  e.  RR
2 pnfxr 10646 . . . . . . . . 9  |-  +oo  e.  RR*
3 icossre 10924 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
41, 2, 3mp2an 654 . . . . . . . 8  |-  ( 0 [,)  +oo )  C_  RR
5 ax-resscn 8981 . . . . . . . 8  |-  RR  C_  CC
64, 5sstri 3301 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  CC
76sseli 3288 . . . . . 6  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  CC )
8 simpll 731 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  A  e.  CC )
9 ax-1cn 8982 . . . . . . . . . . . 12  |-  1  e.  CC
109a1i 11 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  e.  CC )
11 simplr 732 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  e.  CC )
12 ax-1ne0 8993 . . . . . . . . . . . 12  |-  1  =/=  0
1312a1i 11 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  =/=  0 )
14 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  -.  x  =  0 )
1514neneqad 2621 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  =/=  0 )
168, 10, 11, 13, 15divdiv2d 9755 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( ( A  x.  x )  /  1
) )
17 mulcl 9008 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( A  x.  x
)  e.  CC )
1817adantr 452 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  x.  x )  e.  CC )
1918div1d 9715 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( A  x.  x
)  /  1 )  =  ( A  x.  x ) )
2016, 19eqtrd 2420 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( A  x.  x
) )
2120oveq2d 6037 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  /  ( 1  /  x ) ) )  =  ( 1  +  ( A  x.  x
) ) )
2221oveq1d 6036 . . . . . . 7  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
2322ifeq2da 3709 . . . . . 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 461 . . . . 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 4237 . . . 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 5132 . . . . 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 2438 . . 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 10014 . . . . . 6  |-  0  <_  0
31 elrege0 10940 . . . . . 6  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
321, 30, 31mpbir2an 887 . . . . 5  |-  0  e.  ( 0 [,)  +oo )
3332a1i 11 . . . 4  |-  ( A  e.  CC  ->  0  e.  ( 0 [,)  +oo ) )
34 eqeq2 2397 . . . . . . . . 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 2397 . . . . . . . . 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 18679 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
3837a1i 11 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
39 0cn 9018 . . . . . . . . . . . . . . . 16  |-  0  e.  CC
4039a1i 11 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  0  e.  CC )
41 abscl 12011 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
42 peano2re 9172 . . . . . . . . . . . . . . . . . . 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 12020 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  0  <_  ( abs `  A
) )
4641ltp1d 9874 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  < 
( ( abs `  A
)  +  1 ) )
4744, 41, 43, 45, 46lelttrd 9161 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  0  <  ( ( abs `  A
)  +  1 ) )
4843, 47elrpd 10579 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  (
( abs `  A
)  +  1 )  e.  RR+ )
4948rpreccld 10591 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR+ )
5049rpxrd 10582 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR* )
51 blssm 18343 . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  C_  CC )
5336, 52syl5eqss 3336 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  S  C_  CC )
5453sselda 3292 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  CC )
55 mul0or 9595 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5654, 55syldan 457 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5756biimpa 471 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  ( A  =  0  \/  x  =  0 ) )
58 simpl 444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  A  e.  CC )
5958, 54jca 519 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  e.  CC  /\  x  e.  CC ) )
6011, 15reccld 9716 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6159, 60sylan 458 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6261adantlr 696 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  /  x )  e.  CC )
63621cxpd 20466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  ^ c  ( 1  /  x ) )  =  1 )
64 simplr 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  A  = 
0 )
6564oveq1d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  ( 0  x.  x ) )
6654ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  x  e.  CC )
6766mul02d 9197 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 0  x.  x )  =  0 )
6865, 67eqtrd 2420 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  0 )
6968oveq2d 6037 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 ) )
709addid1i 9186 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  0 )  =  1
7169, 70syl6eq 2436 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  1 )
7271oveq1d 6036 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( 1  ^ c  ( 1  /  x ) ) )
7364fveq2d 5673 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  ( exp `  0 ) )
74 ef0 12621 . . . . . . . . . . . . . . . 16  |-  ( exp `  0 )  =  1
7573, 74syl6eq 2436 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  1 )
7663, 72, 753eqtr4d 2430 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( exp `  A
) )
7776ifeq2da 3709 . . . . . . . . . . . . 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 3715 . . . . . . . . . . . . 13  |-  if ( x  =  0 ,  ( exp `  A
) ,  ( exp `  A ) )  =  ( exp `  A
)
7977, 78syl6eq 2436 . . . . . . . . . . . 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 3689 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
8180adantl 453 . . . . . . . . . . . 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 761 . . . . . . . . . . 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 9022 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
8483ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( A  x.  1 )  =  A )
8584fveq2d 5673 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( exp `  ( A  x.  1 ) )  =  ( exp `  A ) )
8682, 85eqtr4d 2423 . . . . . . . . . 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 457 . . . . . . . . 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 9596 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
8954, 88syldan 457 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
90 df-ne 2553 . . . . . . . . . . . 12  |-  ( ( A  x.  x )  =/=  0  <->  -.  ( A  x.  x )  =  0 )
9189, 90syl6bb 253 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  -.  ( A  x.  x )  =  0 ) )
92 simprr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  =/=  0 )
9392neneqd 2567 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  -.  x  =  0
)
94 iffalse 3690 . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  x.  x
)  e.  CC )
97 addcl 9006 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( 1  +  ( A  x.  x
) )  e.  CC )
989, 96, 97sylancr 645 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  CC )
9998adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  e.  CC )
100 eqid 2388 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
101100dvlog2lem 20411 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
102 eqid 2388 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
103102logdmss 20401 . . . . . . . . . . . . . . . . . 18  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
104101, 103sstri 3301 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
105 eqid 2388 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
106105cnmetdval 18677 . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( 1  +  ( A  x.  x
) )  -  1 ) ) )
108 pncan2 9245 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( ( 1  +  ( A  x.  x ) )  - 
1 )  =  ( A  x.  x ) )
1099, 96, 108sylancr 645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  -  1 )  =  ( A  x.  x ) )
110109fveq2d 5673 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
( 1  +  ( A  x.  x ) )  -  1 ) )  =  ( abs `  ( A  x.  x
) ) )
111107, 110eqtrd 2420 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( A  x.  x
) ) )
11296abscld 12166 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  e.  RR )
11343adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  +  1 )  e.  RR )
11454abscld 12166 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  e.  RR )
115113, 114remulcld 9050 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  e.  RR )
116 1re 9024 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  RR
117116a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  RR )
118 absmul 12027 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
11954, 118syldan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
12041adantr 452 . . . . . . . . . . . . . . . . . . . . . 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 12174 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <_  ( abs `  x ) )
123120lep1d 9875 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  A
)  <_  ( ( abs `  A )  +  1 ) )
124120, 121, 114, 122, 123lemul1ad 9883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  x.  ( abs `  x ) )  <_ 
( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) ) )
125119, 124eqbrtrd 4174 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <_  ( (
( abs `  A
)  +  1 )  x.  ( abs `  x
) ) )
126105cnmetdval 18677 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  CC  /\  0  e.  CC )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12754, 39, 126sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12854subid1d 9333 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x  -  0 )  =  x )
129128fveq2d 5673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
x  -  0 ) )  =  ( abs `  x ) )
130127, 129eqtrd 2420 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  x ) )
131 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  S )
132131, 36syl6eleq 2478 . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . 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 18326 . . . . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
139130, 138eqbrtrrd 4176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
14047adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <  ( ( abs `  A )  +  1 ) )
141 ltmuldiv2 9814 . . . . . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( ( abs `  A )  +  1 )  x.  ( abs `  x
) )  <  1  <->  ( abs `  x )  <  ( 1  / 
( ( abs `  A
)  +  1 ) ) ) )
143139, 142mpbird 224 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  <  1 )
144112, 115, 117, 125, 143lelttrd 9161 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <  1 )
145111, 144eqbrtrd 4174 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  <  1 )
146 1rp 10549 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
147 rpxr 10552 . . . . . . . . . . . . . . . . . . . 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 18326 . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
153104, 152sseldi 3290 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( CC 
\  { 0 } ) )
154 eldifsni 3872 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  =/=  0 )
15754adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  e.  CC )
158157, 92reccld 9716 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  e.  CC )
15999, 156, 158cxpefd 20471 . . . . . . . . . . . . 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 20336 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
161160adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
162158, 161mulcomd 9043 . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  e.  CC )
164 simprl 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  =/=  0 )
165163, 164dividd 9721 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  /  A
)  =  1 )
166165oveq1d 6036 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( 1  /  x ) )
167163, 163, 157, 164, 92divdiv1d 9754 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( A  /  ( A  x.  x ) ) )
168166, 167eqtr3d 2422 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  =  ( A  /  ( A  x.  x ) ) )
169168oveq2d 6037 . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  e.  CC )
17189biimpa 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  =/=  0 )
172161, 163, 170, 171div12d 9759 . . . . . . . . . . . . . . 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 2424 . . . . . . . . . . . . . 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 5673 . . . . . . . . . . . . 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 2424 . . . . . . . . . . . 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 424 . . . . . . . . . . 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 227 . . . . . . . . . 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 419 . . . . . . . . 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 3713 . . . . . . . 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 4237 . . . . . . 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 5132 . . . . . . . 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 452 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( log `  ( 1  +  ( A  x.  x
) ) )  e.  CC )
18596adantr 452 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  e.  CC )
186 simpr 448 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  -.  ( A  x.  x
)  =  0 )
187186neneqad 2621 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  =/=  0 )
188184, 185, 187divcld 9723 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) )  e.  CC )
189183, 188ifclda 3710 . . . . . . . 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 2389 . . . . . . . 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 2389 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  =  ( y  e.  CC  |->  ( exp `  ( A  x.  y
) ) ) )
192 oveq2 6029 . . . . . . . . . 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 5673 . . . . . . . . 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 6029 . . . . . . . . . . 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 5673 . . . . . . . . . 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 6029 . . . . . . . . . . 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 5673 . . . . . . . . . 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 3692 . . . . . . . . 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 2436 . . . . . . . 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 5841 . . . . . . 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 2430 . . . . . 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 2389 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )
203 eqidd 2389 . . . . . . . . . 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 2394 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  =  1  <->  (
1  +  ( A  x.  x ) )  =  1 ) )
205 fveq2 5669 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  ( log `  y )  =  ( log `  (
1  +  ( A  x.  x ) ) ) )
206 oveq1 6028 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  -  1 )  =  ( ( 1  +  ( A  x.  x ) )  - 
1 ) )
207205, 206oveq12d 6039 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
( log `  y
)  /  ( y  -  1 ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  (
( 1  +  ( A  x.  x ) )  -  1 ) ) )
208204, 207ifbieq2d 3703 . . . . . . . . . 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 5841 . . . . . . . . 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 2398 . . . . . . . . . . . 12  |-  ( ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 )  <->  ( 1  +  ( A  x.  x ) )  =  1 )
211149, 96, 135addcand 9202 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  ( 1  +  0 )  <-> 
( A  x.  x
)  =  0 ) )
212210, 211syl5bbr 251 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  1  <-> 
( A  x.  x
)  =  0 ) )
213109oveq2d 6037 . . . . . . . . . . 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 3703 . . . . . . . . . 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 4237 . . . . . . . . 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 2420 . . . . . . . 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 2388 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
218 eqid 2388 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
219218cnfldtopon 18689 . . . . . . . . . . . . 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 17616 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  1 )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
223 id 20 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  A  e.  CC )
224220, 220, 223cnmptc 17616 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
225220cnmptid 17615 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  x )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
226218mulcn 18769 . . . . . . . . . . . . . . 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 17620 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( A  x.  x ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
229218addcn 18767 . . . . . . . . . . . . . 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 17620 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
232217, 220, 53, 231cnmpt1res 17630 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  ( TopOpen
` fld
) ) )
233 eqid 2388 . . . . . . . . . . . . . 14  |-  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x
) ) )
234152, 233fmptd 5833 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) : S --> ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
235 frn 5538 . . . . . . . . . . . . 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 3418 . . . . . . . . . . . . . 14  |-  ( CC 
\  { 0 } )  C_  CC
238104, 237sstri 3301 . . . . . . . . . . . . 13  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
239238a1i 11 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
240 cnrest2 17273 . . . . . . . . . . . 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 1184 . . . . . . . . . . 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 202 . . . . . . . . . 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 18339 . . . . . . . . . . . . 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 1184 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  0  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) ) )
245244, 36syl6eleqr 2479 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  0  e.  S )
246 resttopon 17148 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
247219, 53, 246sylancr 645 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
248 toponuni 16916 . . . . . . . . . . . 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 2464 . . . . . . . . . 10  |-  ( A  e.  CC  ->  0  e.  U. ( ( TopOpen ` fld )t  S
) )
251 eqid 2388 . . . . . . . . . . 11  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
252251cncnpi 17265 . . . . . . . . . 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 643 . . . . . . . . 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 9005 . . . . . . . . . . . 12  |-  CC  e.  _V
255254prid2 3857 . . . . . . . . . . 11  |-  CC  e.  { RR ,  CC }
256 logf1o 20330 . . . . . . . . . . . . . 14  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
257 f1of 5615 . . . . . . . . . . . . . 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 20328 . . . . . . . . . . . . . 14  |-  ( x  e.  ran  log  ->  x  e.  CC )
260259ssriv 3296 . . . . . . . . . . . . 13  |-  ran  log  C_  CC
261 fss 5540 . . . . . . . . . . . . 13  |-  ( ( log : ( CC 
\  { 0 } ) --> ran  log  /\  ran  log  C_  CC )  ->  log : ( CC  \  {
0 } ) --> CC )
262258, 260, 261mp2an 654 . . . . . . . . . . . 12  |-  log :
( CC  \  {
0 } ) --> CC
263 fssres 5551 . . . . . . . . . . . 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 654 . . . . . . . . . . 11  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC
265 blcntr 18339 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  CC  /\  1  e.  RR+ )  ->  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
26637, 9, 146, 265mp3an 1279 . . . . . . . . . . . . 13  |-  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
267 ovex 6046 . . . . . . . . . . . . . 14  |-  ( 1  /  y )  e. 
_V
268100dvlog2 20412 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  y
) )
269267, 268dmmpti 5515 . . . . . . . . . . . . 13  |-  dom  ( CC  _D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )
270266, 269eleqtrri 2461 . . . . . . . . . . . 12  |-  1  e.  dom  ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
271 eqid 2388 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
272268fveq1i 5670 . . . . . . . . . . . . . . . . 17  |-  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `  1
)  =  ( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )
273 oveq2 6029 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  1  ->  (
1  /  y )  =  ( 1  / 
1 ) )
2749div1i 9675 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
275273, 274syl6eq 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  1  ->  (
1  /  y )  =  1 )
276 eqid 2388 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( 1  / 
y ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) )
277 1ex 9020 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  _V
278275, 276, 277fvmpt 5746 . . . . . . . . . . . . . . . . . 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 2409 . . . . . . . . . . . . . . . 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 5686 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  y
)  =  ( log `  y ) )
283 fvres 5686 . . . . . . . . . . . . . . . . . . . 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 20348 . . . . . . . . . . . . . . . . . . 19  |-  ( log `  1 )  =  0
286284, 285syl6eq 2436 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  0 )
287282, 286oveq12d 6039 . . . . . . . . . . . . . . . . 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 3288 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  ( CC  \  { 0 } ) )
289 eldifsn 3871 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( CC  \  { 0 } )  <-> 
( y  e.  CC  /\  y  =/=  0 ) )
290288, 289sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  CC  /\  y  =/=  0 ) )
291 logcl 20334 . . . . . . . . . . . . . . . . . . 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 9333 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log `  y )  - 
0 )  =  ( log `  y ) )
294287, 293eqtr2d 2421 . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . 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 3699 . . . . . . . . . . . . . 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 4233 . . . . . . . . . . . . 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 19673 . . . . . . . . . . . 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 653 . . . . . . . . . . 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 1279 . . . . . . . . . 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 6029 . . . . . . . . . . . . . . 15  |-  ( x  =  0  ->  ( A  x.  x )  =  ( A  x.  0 ) )
302301oveq2d 6037 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  (
1  +  ( A  x.  x ) )  =  ( 1  +  ( A  x.  0 ) ) )
303 ovex 6046 . . . . . . . . . . . . . 14  |-  ( 1  +  ( A  x.  0 ) )  e. 
_V
304302, 233, 303fvmpt 5746 . . . . . . . . . . . . 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 9178 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
307306oveq2d 6037 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  ( 1  +  0 ) )
308307, 70syl6eq 2436 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  1 )
309305, 308eqtrd 2420 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  1 )
310309fveq2d 5673 . . . . . . . . . 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 2475 . . . . . . . . 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 17254 . . . . . . . . 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 643 . . . . . . . 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 2463 . . . . . . 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 17616 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
316220cnmptid 17615 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  y )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
317220, 315, 316, 227cnmpt12f 17620 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( A  x.  y ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
318 efcn 20227 . . . . . . . . . . 11  |-  exp  e.  ( CC -cn-> CC )
319218cncfcn1 18812 . . . . . . . . . . 11  |-  ( CC
-cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
320318, 319eleqtri 2460 . . . . . . . . . 10  |-  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
321320a1i 11 . . . . . . . . 9  |-  ( A  e.  CC  ->  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
322220, 317, 321cnmpt11f 17618 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
323 eqid 2388 . . . . . . . . . 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 5833 . . . . . . . . 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 5811 . . . . . . . 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 16921 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
327326cncnpi 17265 . . . . . . . 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 643 . . . . . . 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 17254 . . . . . . 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 643 . . . . . 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 2462 . . . . 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 18690 . . . . . . 7  |-  ( TopOpen ` fld )  e.  Top
333332a1i 11 . . . . . 6  |-  ( A  e.  CC  ->  ( TopOpen
` fld
)  e.  Top )
334218cnfldtopn 18688 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
335334blopn 18421 . . . . . . . . . 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 1184 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  e.  (
TopOpen ` fld ) )
33736, 336syl5eqel 2472 . . . . . . . 8  |-  ( A  e.  CC  ->  S  e.  ( TopOpen ` fld ) )
338 isopn3i 17070 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  ( TopOpen ` fld )
)  ->  ( ( int `  ( TopOpen ` fld ) ) `  S
)  =  S )
339332, 337, 338sylancr 645 . . . . . . 7  |-  ( A  e.  CC  ->  (
( int `  ( TopOpen
` fld
) ) `  S
)  =  S )
340245, 339eleqtrrd 2465 . . . . . 6  |-  ( A  e.  CC  ->  0  e.  ( ( int `  ( TopOpen
` fld
) ) `  S
) )
341 efcl 12613 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( exp `  A )  e.  CC )
342341ad2antrr 707 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  x  =  0 )  ->  ( exp `  A )  e.  CC )
3439, 18, 97sylancr 645 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  x.  x ) )  e.  CC )
344343, 60cxpcld 20467 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  e.  CC )
345342, 344ifclda 3710 . . . . . . 7  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  e.  CC )
346 eqid 2388 . . . . . . 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 5833 . . . . . 6  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) : CC --> CC )
348326, 326cnprest 17276 . . . . . 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 1185 . . . . 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 224 . . . 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 17275 . . . 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 1184 . . 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 2462 . 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 444 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  ->  A  e.  CC )
355 rpcn 10553 . . . . . . 7  |-  ( k  e.  RR+  ->  k  e.  CC )
356355adantl 453 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  e.  CC )
357 rpne0 10560 . . . . . . 7  |-  ( k  e.  RR+  ->  k  =/=  0 )
358357adantl 453 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  =/=  0 )
359354, 356, 358divcld 9723 . . . . 5  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( A  /  k
)  e.  CC )
360 addcl 9006 . . . . 5  |-  ( ( 1  e.  CC  /\  ( A  /  k
)  e.  CC )  ->  ( 1  +  ( A  /  k
) )  e.  CC )
3619, 359, 360sylancr 645 . . . 4  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( 1  +  ( A  /  k ) )  e.  CC )
362361, 356cxpcld 20467 . . 3  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( ( 1  +  ( A  /  k
) )  ^ c 
k )  e.  CC )
363 oveq2 6029 . . . . 5  |-  ( k  =  ( 1  /  x )  ->  ( A  /  k )  =  ( A  /  (
1  /  x ) ) )
364363oveq2d 6037 . . . 4  |-  ( k  =  ( 1  /  x )  ->  (
1  +  ( A  /  k ) )  =  ( 1  +  ( A  /  (
1  /  x ) ) ) )
365 id 20 . . . 4  |-  ( k  =  ( 1  /  x )  ->  k  =  ( 1  /  x ) )
366364, 365oveq12d 6039 . . 3  |-  ( k  =  ( 1  /  x )  ->  (
( 1  +  ( A  /  k ) )  ^ c  k )  =  ( ( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) ) )
367 eqid 2388 . . 3  |-  ( (
TopOpen ` fld )t  ( 0 [,)  +oo ) )  =  ( ( TopOpen ` fld )t  ( 0 [,) 
+oo ) )
368341, 362, 366, 218, 367rlimcnp3 20674 . 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 )t