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

Theorem efrlim 20280
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 20281). (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 8854 . . . . . . . . 9  |-  0  e.  RR
2 pnfxr 10471 . . . . . . . . 9  |-  +oo  e.  RR*
3 icossre 10746 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
41, 2, 3mp2an 653 . . . . . . . 8  |-  ( 0 [,)  +oo )  C_  RR
5 ax-resscn 8810 . . . . . . . 8  |-  RR  C_  CC
64, 5sstri 3201 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  CC
76sseli 3189 . . . . . 6  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  CC )
8 simpll 730 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  A  e.  CC )
9 ax-1cn 8811 . . . . . . . . . . . 12  |-  1  e.  CC
109a1i 10 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  e.  CC )
11 simplr 731 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  e.  CC )
12 ax-1ne0 8822 . . . . . . . . . . . 12  |-  1  =/=  0
1312a1i 10 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  1  =/=  0 )
14 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  -.  x  =  0 )
15 df-ne 2461 . . . . . . . . . . . 12  |-  ( x  =/=  0  <->  -.  x  =  0 )
1614, 15sylibr 203 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  x  =/=  0 )
178, 10, 11, 13, 16divdiv2d 9584 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( ( A  x.  x )  /  1
) )
18 mulcl 8837 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( A  x.  x
)  e.  CC )
1918adantr 451 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  x.  x )  e.  CC )
2019div1d 9544 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( A  x.  x
)  /  1 )  =  ( A  x.  x ) )
2117, 20eqtrd 2328 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  ( A  /  ( 1  /  x ) )  =  ( A  x.  x
) )
2221oveq2d 5890 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  /  ( 1  /  x ) ) )  =  ( 1  +  ( A  x.  x
) ) )
2322oveq1d 5889 . . . . . . 7  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  /  ( 1  /  x ) ) )  ^ c  ( 1  /  x ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
2423ifeq2da 3604 . . . . . 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 ) ) ) )
257, 24sylan2 460 . . . . 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 ) ) ) )
2625mpteq2dva 4122 . . . 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 ) ) ) ) )
27 resmpt 5016 . . . . 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 ) ) ) ) )
286, 27ax-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 ) ) ) )
2926, 28syl6eqr 2346 . . 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 ) ) )
306a1i 10 . . . 4  |-  ( A  e.  CC  ->  (
0 [,)  +oo )  C_  CC )
31 0le0 9843 . . . . . 6  |-  0  <_  0
32 elrege0 10762 . . . . . 6  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
331, 31, 32mpbir2an 886 . . . . 5  |-  0  e.  ( 0 [,)  +oo )
3433a1i 10 . . . 4  |-  ( A  e.  CC  ->  0  e.  ( 0 [,)  +oo ) )
35 eqeq2 2305 . . . . . . . . 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 ) ) ) ) ) ) )
36 eqeq2 2305 . . . . . . . . 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 ) ) ) ) ) ) )
37 efrlim.1 . . . . . . . . . . . . . 14  |-  S  =  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) )
38 cnxmet 18298 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
3938a1i 10 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
40 0cn 8847 . . . . . . . . . . . . . . . 16  |-  0  e.  CC
4140a1i 10 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  0  e.  CC )
42 abscl 11779 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
43 peano2re 9001 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs `  A )  e.  RR  ->  (
( abs `  A
)  +  1 )  e.  RR )
4442, 43syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  (
( abs `  A
)  +  1 )  e.  RR )
451a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  0  e.  RR )
46 absge0 11788 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  0  <_  ( abs `  A
) )
4742ltp1d 9703 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  ( abs `  A )  < 
( ( abs `  A
)  +  1 ) )
4845, 42, 44, 46, 47lelttrd 8990 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  0  <  ( ( abs `  A
)  +  1 ) )
4944, 48elrpd 10404 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  (
( abs `  A
)  +  1 )  e.  RR+ )
5049rpreccld 10416 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR+ )
5150rpxrd 10407 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  (
1  /  ( ( abs `  A )  +  1 ) )  e.  RR* )
52 blssm 17984 . . . . . . . . . . . . . . 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 )
5339, 41, 51, 52syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  C_  CC )
5437, 53syl5eqss 3235 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  S  C_  CC )
5554sselda 3193 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  CC )
56 mul0or 9424 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5755, 56syldan 456 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  x.  x )  =  0  <-> 
( A  =  0  \/  x  =  0 ) ) )
5857biimpa 470 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  ( A  =  0  \/  x  =  0 ) )
59 simpl 443 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  A  e.  CC )
6059, 55jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  e.  CC  /\  x  e.  CC ) )
6111, 16reccld 9545 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6260, 61sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  x  =  0 )  ->  (
1  /  x )  e.  CC )
6362adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  /  x )  e.  CC )
64631cxpd 20070 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  ^ c  ( 1  /  x ) )  =  1 )
65 simplr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  A  = 
0 )
6665oveq1d 5889 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  ( 0  x.  x ) )
6755ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  x  e.  CC )
6867mul02d 9026 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 0  x.  x )  =  0 )
6966, 68eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( A  x.  x )  =  0 )
7069oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 ) )
719addid1i 9015 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  0 )  =  1
7270, 71syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( 1  +  ( A  x.  x ) )  =  1 )
7372oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( 1  ^ c  ( 1  /  x ) ) )
7465fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  ( exp `  0 ) )
75 ef0 12388 . . . . . . . . . . . . . . . 16  |-  ( exp `  0 )  =  1
7674, 75syl6eq 2344 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( exp `  A )  =  1 )
7764, 73, 763eqtr4d 2338 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  /\  -.  x  =  0
)  ->  ( (
1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  =  ( exp `  A
) )
7877ifeq2da 3604 . . . . . . . . . . . . 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 ) ) )
79 ifid 3610 . . . . . . . . . . . . 13  |-  if ( x  =  0 ,  ( exp `  A
) ,  ( exp `  A ) )  =  ( exp `  A
)
8078, 79syl6eq 2344 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  A  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
81 iftrue 3584 . . . . . . . . . . . . 13  |-  ( x  =  0  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
8281adantl 452 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  x  =  0 )  ->  if (
x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( exp `  A ) )
8380, 82jaodan 760 . . . . . . . . . . 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 ) )
84 mulid1 8851 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
8584ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( A  x.  1 )  =  A )
8685fveq2d 5545 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =  0  \/  x  =  0 ) )  -> 
( exp `  ( A  x.  1 ) )  =  ( exp `  A ) )
8783, 86eqtr4d 2331 . . . . . . . . . 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 ) ) )
8858, 87syldan 456 . . . . . . . . 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 ) ) )
89 mulne0b 9425 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
9055, 89syldan 456 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  ( A  x.  x )  =/=  0
) )
91 df-ne 2461 . . . . . . . . . . . 12  |-  ( ( A  x.  x )  =/=  0  <->  -.  ( A  x.  x )  =  0 )
9290, 91syl6bb 252 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( A  =/=  0  /\  x  =/=  0 )  <->  -.  ( A  x.  x )  =  0 ) )
93 simprr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  =/=  0 )
9493, 15sylib 188 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  -.  x  =  0
)
95 iffalse 3585 . . . . . . . . . . . . . 14  |-  ( -.  x  =  0  ->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  =  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )
9694, 95syl 15 . . . . . . . . . . . . 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 ) ) )
9755, 18syldan 456 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( A  x.  x
)  e.  CC )
98 addcl 8835 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( 1  +  ( A  x.  x
) )  e.  CC )
999, 97, 98sylancr 644 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  CC )
10099adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  e.  CC )
101 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  =  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
102101dvlog2lem 20015 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  (  -oo (,] 0 ) )
103 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
\  (  -oo (,] 0 ) )  =  ( CC  \  (  -oo (,] 0 ) )
104103logdmss 20005 . . . . . . . . . . . . . . . . . 18  |-  ( CC 
\  (  -oo (,] 0 ) )  C_  ( CC  \  { 0 } )
105102, 104sstri 3201 . . . . . . . . . . . . . . . . 17  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  ( CC  \  { 0 } )
106 eqid 2296 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
107106cnmetdval 18296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  +  ( A  x.  x ) )  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( 1  +  ( A  x.  x
) )  -  1 ) ) )
10899, 9, 107sylancl 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( ( 1  +  ( A  x.  x
) )  -  1 ) ) )
109 pncan2 9074 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( A  x.  x
)  e.  CC )  ->  ( ( 1  +  ( A  x.  x ) )  - 
1 )  =  ( A  x.  x ) )
1109, 97, 109sylancr 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  -  1 )  =  ( A  x.  x ) )
111110fveq2d 5545 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
( 1  +  ( A  x.  x ) )  -  1 ) )  =  ( abs `  ( A  x.  x
) ) )
112108, 111eqtrd 2328 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  =  ( abs `  ( A  x.  x
) ) )
11397abscld 11934 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  e.  RR )
11444adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  +  1 )  e.  RR )
11555abscld 11934 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  e.  RR )
116114, 115remulcld 8879 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  e.  RR )
117 1re 8853 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  RR
118117a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  RR )
119 absmul 11795 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
12055, 119syldan 456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  =  ( ( abs `  A )  x.  ( abs `  x
) ) )
12142adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  A
)  e.  RR )
122121, 43syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  +  1 )  e.  RR )
12355absge0d 11942 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <_  ( abs `  x ) )
124121lep1d 9704 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  A
)  <_  ( ( abs `  A )  +  1 ) )
125121, 122, 115, 123, 124lemul1ad 9712 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( abs `  A
)  x.  ( abs `  x ) )  <_ 
( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) ) )
126120, 125eqbrtrd 4059 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <_  ( (
( abs `  A
)  +  1 )  x.  ( abs `  x
) ) )
127106cnmetdval 18296 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  CC  /\  0  e.  CC )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12855, 40, 127sylancl 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  ( x  -  0 ) ) )
12955subid1d 9162 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x  -  0 )  =  x )
130129fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  (
x  -  0 ) )  =  ( abs `  x ) )
131128, 130eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  =  ( abs `  x ) )
132 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  S )
133132, 37syl6eleq 2386 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  x  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) ) )
13438a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
13551adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  /  (
( abs `  A
)  +  1 ) )  e.  RR* )
13640a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  e.  CC )
137 elbl3 17967 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
138134, 135, 136, 55, 137syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
139133, 138mpbid 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( x ( abs 
o.  -  ) 0 )  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
140131, 139eqbrtrrd 4061 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  x
)  <  ( 1  /  ( ( abs `  A )  +  1 ) ) )
14148adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  0  <  ( ( abs `  A )  +  1 ) )
142 ltmuldiv2 9643 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
143115, 118, 122, 141, 142syl112anc 1186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( ( abs `  A )  +  1 )  x.  ( abs `  x
) )  <  1  <->  ( abs `  x )  <  ( 1  / 
( ( abs `  A
)  +  1 ) ) ) )
144140, 143mpbird 223 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( ( abs `  A )  +  1 )  x.  ( abs `  x ) )  <  1 )
145113, 116, 118, 126, 144lelttrd 8990 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( abs `  ( A  x.  x )
)  <  1 )
146112, 145eqbrtrd 4059 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) ) ( abs 
o.  -  ) 1 )  <  1 )
147 1rp 10374 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
148 rpxr 10377 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  RR+  ->  1  e. 
RR* )
149147, 148mp1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  RR* )
1509a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  1  e.  CC )
151 elbl3 17967 . . . . . . . . . . . . . . . . . . 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 ) )
152134, 149, 150, 99, 151syl22anc 1183 . . . . . . . . . . . . . . . . . 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 ) )
153146, 152mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
154105, 153sseldi 3191 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  e.  ( CC 
\  { 0 } ) )
155 eldifsni 3763 . . . . . . . . . . . . . . . 16  |-  ( ( 1  +  ( A  x.  x ) )  e.  ( CC  \  { 0 } )  ->  ( 1  +  ( A  x.  x
) )  =/=  0
)
156154, 155syl 15 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( 1  +  ( A  x.  x ) )  =/=  0 )
157156adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  +  ( A  x.  x ) )  =/=  0 )
15855adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  x  e.  CC )
159158, 93reccld 9545 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  e.  CC )
160100, 157, 159cxpefd 20075 . . . . . . . . . . . . 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 ) ) ) ) ) )
161 logcl 19942 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  +  ( A  x.  x ) )  e.  CC  /\  ( 1  +  ( A  x.  x ) )  =/=  0 )  ->  ( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
16299, 156, 161syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
163162adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( log `  (
1  +  ( A  x.  x ) ) )  e.  CC )
164159, 163mulcomd 8872 . . . . . . . . . . . . . . 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 ) ) )
165 simpll 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  e.  CC )
166 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  ->  A  =/=  0 )
167165, 166dividd 9550 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  /  A
)  =  1 )
168167oveq1d 5889 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( 1  /  x ) )
169165, 165, 158, 166, 93divdiv1d 9583 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( ( A  /  A )  /  x
)  =  ( A  /  ( A  x.  x ) ) )
170168, 169eqtr3d 2330 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( 1  /  x
)  =  ( A  /  ( A  x.  x ) ) )
171170oveq2d 5890 . . . . . . . . . . . . . . 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 ) ) ) )
17297adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  e.  CC )
17390biimpa 470 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  =/=  0  /\  x  =/=  0 ) )  -> 
( A  x.  x
)  =/=  0 )
174163, 165, 172, 173div12d 9588 . . . . . . . . . . . . . . 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 ) ) ) )
175164, 171, 1743eqtrd 2332 . . . . . . . . . . . . . 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 ) ) ) )
176175fveq2d 5545 . . . . . . . . . . . . 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
) ) ) ) )
17796, 160, 1763eqtrd 2332 . . . . . . . . . . . 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 ) ) ) ) )
178177ex 423 . . . . . . . . . . 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 ) ) ) ) ) )
17992, 178sylbird 226 . . . . . . . . . 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 ) ) ) ) ) )
180179imp 418 . . . . . . . . 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 ) ) ) ) )
18135, 36, 88, 180ifbothda 3608 . . . . . . . 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 ) ) ) ) ) )
182181mpteq2dva 4122 . . . . . . 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 ) ) ) ) ) ) )
183 resmpt 5016 . . . . . . . 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 ) ) ) ) )
18454, 183syl 15 . . . . . . 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 ) ) ) ) )
1859a1i 10 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  ( A  x.  x )  =  0 )  ->  1  e.  CC )
186162adantr 451 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( log `  ( 1  +  ( A  x.  x
) ) )  e.  CC )
18797adantr 451 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  e.  CC )
188 simpr 447 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  -.  ( A  x.  x
)  =  0 )
189188, 91sylibr 203 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  ( A  x.  x )  =/=  0 )
190186, 187, 189divcld 9552 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  S )  /\  -.  ( A  x.  x )  =  0 )  ->  (
( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) )  e.  CC )
191185, 190ifclda 3605 . . . . . . . 8  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) )  e.  CC )
192 eqidd 2297 . . . . . . . 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 ) ) ) ) )
193 eqidd 2297 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  =  ( y  e.  CC  |->  ( exp `  ( A  x.  y
) ) ) )
194 oveq2 5882 . . . . . . . . . 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 ) ) ) ) )
195194fveq2d 5545 . . . . . . . . 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 ) ) ) ) ) )
196 oveq2 5882 . . . . . . . . . . 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 ) )
197196fveq2d 5545 . . . . . . . . . 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 ) ) )
198 oveq2 5882 . . . . . . . . . . 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 ) ) ) )
199198fveq2d 5545 . . . . . . . . . 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 )
) ) ) )
200197, 199ifsb 3587 . . . . . . . . 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 )
) ) ) )
201195, 200syl6eq 2344 . . . . . . . 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 )
) ) ) ) )
202191, 192, 193, 201fmptco 5707 . . . . . . 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 ) ) ) ) ) ) )
203182, 184, 2023eqtr4d 2338 . . . . . 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 ) ) ) ) ) )
204 eqidd 2297 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) )
205 eqidd 2297 . . . . . . . . . 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 ) ) ) ) )
206 eqeq1 2302 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  =  1  <->  (
1  +  ( A  x.  x ) )  =  1 ) )
207 fveq2 5541 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  ( log `  y )  =  ( log `  (
1  +  ( A  x.  x ) ) ) )
208 oveq1 5881 . . . . . . . . . . . 12  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
y  -  1 )  =  ( ( 1  +  ( A  x.  x ) )  - 
1 ) )
209207, 208oveq12d 5892 . . . . . . . . . . 11  |-  ( y  =  ( 1  +  ( A  x.  x
) )  ->  (
( log `  y
)  /  ( y  -  1 ) )  =  ( ( log `  ( 1  +  ( A  x.  x ) ) )  /  (
( 1  +  ( A  x.  x ) )  -  1 ) ) )
210206, 209ifbieq2d 3598 . . . . . . . . . 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 ) ) ) )
211153, 204, 205, 210fmptco 5707 . . . . . . . . 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 ) ) ) ) )
21271eqeq2i 2306 . . . . . . . . . . . 12  |-  ( ( 1  +  ( A  x.  x ) )  =  ( 1  +  0 )  <->  ( 1  +  ( A  x.  x ) )  =  1 )
213150, 97, 136addcand 9031 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  ( 1  +  0 )  <-> 
( A  x.  x
)  =  0 ) )
214212, 213syl5bbr 250 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  x  e.  S )  ->  ( ( 1  +  ( A  x.  x
) )  =  1  <-> 
( A  x.  x
)  =  0 ) )
215110oveq2d 5890 . . . . . . . . . . 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 )
) )
216214, 215ifbieq2d 3598 . . . . . . . . . 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 ) ) ) )
217216mpteq2dva 4122 . . . . . . . . 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 ) ) ) ) )
218211, 217eqtrd 2328 . . . . . . . 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 ) ) ) ) )
219 eqid 2296 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
220 eqid 2296 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
221220cnfldtopon 18308 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
222221a1i 10 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  ( TopOpen
` fld
)  e.  (TopOn `  CC ) )
2239a1i 10 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  1  e.  CC )
224222, 222, 223cnmptc 17372 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  1 )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
225 id 19 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  A  e.  CC )
226222, 222, 225cnmptc 17372 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
227222cnmptid 17371 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  x )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
228220mulcn 18387 . . . . . . . . . . . . . . 15  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
229228a1i 10 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) ) )
230222, 226, 227, 229cnmpt12f 17376 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( A  x.  x ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
231220addcn 18385 . . . . . . . . . . . . . 14  |-  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
232231a1i 10 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) ) )
233222, 224, 230, 232cnmpt12f 17376 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
234219, 222, 54, 233cnmpt1res 17386 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  e.  ( ( ( TopOpen ` fld )t  S )  Cn  ( TopOpen
` fld
) ) )
235 eqid 2296 . . . . . . . . . . . . . 14  |-  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  =  ( x  e.  S  |->  ( 1  +  ( A  x.  x
) ) )
236153, 235fmptd 5700 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) : S --> ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
237 frn 5411 . . . . . . . . . . . . 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 ) )
238236, 237syl 15 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  ran  ( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) )  C_  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) )
239 difss 3316 . . . . . . . . . . . . . 14  |-  ( CC 
\  { 0 } )  C_  CC
240105, 239sstri 3201 . . . . . . . . . . . . 13  |-  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC
241240a1i 10 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1 ( ball `  ( abs  o.  -  ) ) 1 )  C_  CC )
242 cnrest2 17030 . . . . . . . . . . . 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 ) ) ) ) )
243222, 238, 241, 242syl3anc 1182 . . . . . . . . . . 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 ) ) ) ) )
244234, 243mpbid 201 . . . . . . . . . 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 ) ) ) )
245 blcntr 17980 . . . . . . . . . . . . 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 ) ) ) )
24639, 41, 50, 245syl3anc 1182 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  0  e.  ( 0 ( ball `  ( abs  o.  -  ) ) ( 1  /  ( ( abs `  A )  +  1 ) ) ) )
247246, 37syl6eleqr 2387 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  0  e.  S )
248 resttopon 16908 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
249221, 54, 248sylancr 644 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
250 toponuni 16681 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
251249, 250syl 15 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
252247, 251eleqtrd 2372 . . . . . . . . . 10  |-  ( A  e.  CC  ->  0  e.  U. ( ( TopOpen ` fld )t  S
) )
253 eqid 2296 . . . . . . . . . . 11  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
254253cncnpi 17023 . . . . . . . . . 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
) )
255244, 252, 254syl2anc 642 . . . . . . . . 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 ) )
256 cnex 8834 . . . . . . . . . . . 12  |-  CC  e.  _V
257256prid2 3748 . . . . . . . . . . 11  |-  CC  e.  { RR ,  CC }
258 logf1o 19938 . . . . . . . . . . . . . 14  |-  log :
( CC  \  {
0 } ) -1-1-onto-> ran  log
259 f1of 5488 . . . . . . . . . . . . . 14  |-  ( log
: ( CC  \  { 0 } ) -1-1-onto-> ran 
log  ->  log : ( CC 
\  { 0 } ) --> ran  log )
260258, 259ax-mp 8 . . . . . . . . . . . . 13  |-  log :
( CC  \  {
0 } ) --> ran 
log
261 logrncn 19936 . . . . . . . . . . . . . 14  |-  ( x  e.  ran  log  ->  x  e.  CC )
262261ssriv 3197 . . . . . . . . . . . . 13  |-  ran  log  C_  CC
263 fss 5413 . . . . . . . . . . . . 13  |-  ( ( log : ( CC 
\  { 0 } ) --> ran  log  /\  ran  log  C_  CC )  ->  log : ( CC  \  {
0 } ) --> CC )
264260, 262, 263mp2an 653 . . . . . . . . . . . 12  |-  log :
( CC  \  {
0 } ) --> CC
265 fssres 5424 . . . . . . . . . . . 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 )
266264, 105, 265mp2an 653 . . . . . . . . . . 11  |-  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) : ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) --> CC
267 blcntr 17980 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  1  e.  CC  /\  1  e.  RR+ )  ->  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
26838, 9, 147, 267mp3an 1277 . . . . . . . . . . . . 13  |-  1  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )
269 ovex 5899 . . . . . . . . . . . . . 14  |-  ( 1  /  y )  e. 
_V
270101dvlog2 20016 . . . . . . . . . . . . . 14  |-  ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) 
|->  ( 1  /  y
) )
271269, 270dmmpti 5389 . . . . . . . . . . . . 13  |-  dom  ( CC  _D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )  =  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )
272268, 271eleqtrri 2369 . . . . . . . . . . . 12  |-  1  e.  dom  ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) )
273 eqid 2296 . . . . . . . . . . . . 13  |-  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )  =  ( (
TopOpen ` fld )t  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) )
274270fveq1i 5542 . . . . . . . . . . . . . . . . 17  |-  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `  1
)  =  ( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )
275 oveq2 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  1  ->  (
1  /  y )  =  ( 1  / 
1 ) )
2769div1i 9504 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  1 )  =  1
277275, 276syl6eq 2344 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  1  ->  (
1  /  y )  =  1 )
278 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  |->  ( 1  / 
y ) )  =  ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) )
279 1ex 8849 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  _V
280277, 278, 279fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( (
y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )  =  1 )
281268, 280ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 1 ( ball `  ( abs  o.  -  ) ) 1 )  |->  ( 1  /  y ) ) `
 1 )  =  1
282274, 281eqtr2i 2317 . . . . . . . . . . . . . . . 16  |-  1  =  ( ( CC 
_D  ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `
 1 )
283282a1i 10 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  1  =  ( ( CC  _D  ( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ) `
 1 ) )
284 fvres 5558 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  y
)  =  ( log `  y ) )
285 fvres 5558 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  ( log `  1 ) )
286268, 285mp1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  ( log `  1 ) )
287 log1 19955 . . . . . . . . . . . . . . . . . . 19  |-  ( log `  1 )  =  0
288286, 287syl6eq 2344 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log  |`  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 ) ) `  1
)  =  0 )
289284, 288oveq12d 5892 . . . . . . . . . . . . . . . . 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 ) )
290105sseli 3189 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  y  e.  ( CC  \  { 0 } ) )
291 eldifsn 3762 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( CC  \  { 0 } )  <-> 
( y  e.  CC  /\  y  =/=  0 ) )
292290, 291sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( y  e.  CC  /\  y  =/=  0 ) )
293 logcl 19942 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  CC  /\  y  =/=  0 )  -> 
( log `  y
)  e.  CC )
294292, 293syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  y )  e.  CC )
295294subid1d 9162 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( ( log `  y )  - 
0 )  =  ( log `  y ) )
296289, 295eqtr2d 2329 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 1 (
ball `  ( abs  o. 
-  ) ) 1 )  ->  ( log `  y )  =  ( ( ( log  |`  (
1 ( ball `  ( abs  o.  -  ) ) 1 ) ) `  y )  -  (
( log  |`  ( 1 ( ball `  ( abs  o.  -  ) ) 1 ) ) ` 
1 ) ) )
297296oveq1d 5889 . . . . . . . . . . . . . . 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 ) ) )
298283, 297ifeq12d 3594 . . . . . . . . . . . . . 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 ) ) ) )
299298mpteq2ia 4118 . . . . . . . . . . . . 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 ) ) ) )
300273, 220, 299dvcnp 19284 . . . . . . . . . . . 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
) )
301272, 300mpan2 652 . . . . . . . . . . 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
) )
302257, 266, 240, 301mp3an 1277 . . . . . . . . . 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 )
303 oveq2 5882 . . . . . . . . . . . . . . 15  |-  ( x  =  0  ->  ( A  x.  x )  =  ( A  x.  0 ) )
304303oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( x  =  0  ->  (
1  +  ( A  x.  x ) )  =  ( 1  +  ( A  x.  0 ) ) )
305 ovex 5899 . . . . . . . . . . . . . 14  |-  ( 1  +  ( A  x.  0 ) )  e. 
_V
306304, 235, 305fvmpt 5618 . . . . . . . . . . . . 13  |-  ( 0  e.  S  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  ( 1  +  ( A  x.  0 ) ) )
307247, 306syl 15 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  ( 1  +  ( A  x.  0 ) ) )
308 mul01 9007 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
309308oveq2d 5890 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  ( 1  +  0 ) )
310309, 71syl6eq 2344 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
1  +  ( A  x.  0 ) )  =  1 )
311307, 310eqtrd 2328 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  ( 1  +  ( A  x.  x ) ) ) `  0
)  =  1 )
312311fveq2d 5545 . . . . . . . . . 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
) )
313302, 312syl5eleqr 2383 . . . . . . . . 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
) ) )
314 cnpco 17012 . . . . . . . . 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 )
)
315255, 313, 314syl2anc 642 . . . . . . . 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
) )
316218, 315eqeltrrd 2371 . . . . . . 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 )
)
317222, 222, 225cnmptc 17372 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  A )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
318222cnmptid 17371 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  y )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
319222, 317, 318, 229cnmpt12f 17376 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( A  x.  y ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
320 efcn 19835 . . . . . . . . . . 11  |-  exp  e.  ( CC -cn-> CC )
321220cncfcn1 18430 . . . . . . . . . . 11  |-  ( CC
-cn-> CC )  =  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
322320, 321eleqtri 2368 . . . . . . . . . 10  |-  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) )
323322a1i 10 . . . . . . . . 9  |-  ( A  e.  CC  ->  exp  e.  ( ( TopOpen ` fld )  Cn  ( TopOpen
` fld
) ) )
324222, 319, 323cnmpt11f 17374 . . . . . . . 8  |-  ( A  e.  CC  ->  (
y  e.  CC  |->  ( exp `  ( A  x.  y ) ) )  e.  ( (
TopOpen ` fld )  Cn  ( TopOpen ` fld )
) )
325 eqid 2296 . . . . . . . . . 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 ) ) ) )
326191, 325fmptd 5700 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) : S --> CC )
327 ffvelrn 5679 . . . . . . . . 9  |-  ( ( ( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) : S --> CC  /\  0  e.  S
)  ->  ( (
x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
)  e.  CC )
328326, 247, 327syl2anc 642 . . . . . . . 8  |-  ( A  e.  CC  ->  (
( x  e.  S  |->  if ( ( A  x.  x )  =  0 ,  1 ,  ( ( log `  (
1  +  ( A  x.  x ) ) )  /  ( A  x.  x ) ) ) ) `  0
)  e.  CC )
329221toponunii 16686 . . . . . . . . 9  |-  CC  =  U. ( TopOpen ` fld )
330329cncnpi 17023 . . . . . . . 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
) ) )
331324, 328, 330syl2anc 642 . . . . . . 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
) ) )
332 cnpco 17012 . . . . . . 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
) )
333316, 331, 332syl2anc 642 . . . . . 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 )
)
334203, 333eqeltrd 2370 . . . . 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
) )
335220cnfldtop 18309 . . . . . . 7  |-  ( TopOpen ` fld )  e.  Top
336335a1i 10 . . . . . 6  |-  ( A  e.  CC  ->  ( TopOpen
` fld
)  e.  Top )
337220cnfldtopn 18307 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
338337blopn 18062 . . . . . . . . . 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 ) )
33939, 41, 51, 338syl3anc 1182 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0 ( ball `  ( abs  o.  -  ) ) ( 1  /  (
( abs `  A
)  +  1 ) ) )  e.  (
TopOpen ` fld ) )
34037, 339syl5eqel 2380 . . . . . . . 8  |-  ( A  e.  CC  ->  S  e.  ( TopOpen ` fld ) )
341 isopn3i 16835 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  ( TopOpen ` fld )
)  ->  ( ( int `  ( TopOpen ` fld ) ) `  S
)  =  S )
342335, 340, 341sylancr 644 . . . . . . 7  |-  ( A  e.  CC  ->  (
( int `  ( TopOpen
` fld
) ) `  S
)  =  S )
343247, 342eleqtrrd 2373 . . . . . 6  |-  ( A  e.  CC  ->  0  e.  ( ( int `  ( TopOpen
` fld
) ) `  S
) )
344 efcl 12380 . . . . . . . . 9  |-  ( A  e.  CC  ->  ( exp `  A )  e.  CC )
345344ad2antrr 706 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  x  =  0 )  ->  ( exp `  A )  e.  CC )
3469, 19, 98sylancr 644 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
1  +  ( A  x.  x ) )  e.  CC )
347346, 61cxpcld 20071 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  x  e.  CC )  /\  -.  x  =  0 )  ->  (
( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) )  e.  CC )
348345, 347ifclda 3605 . . . . . . 7  |-  ( ( A  e.  CC  /\  x  e.  CC )  ->  if ( x  =  0 ,  ( exp `  A ) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) )  e.  CC )
349 eqid 2296 . . . . . . 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 ) ) ) )
350348, 349fmptd 5700 . . . . . 6  |-  ( A  e.  CC  ->  (
x  e.  CC  |->  if ( x  =  0 ,  ( exp `  A
) ,  ( ( 1  +  ( A  x.  x ) )  ^ c  ( 1  /  x ) ) ) ) : CC --> CC )
351329, 329cnprest 17033 . . . . . 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
) ) )
352336, 54, 343, 350, 351syl22anc 1183 . . . . 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
) ) )
353334, 352mpbird 223 . . . 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 )
)
354329cnpresti 17032 . . . 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
) )
35530, 34, 353, 354syl3anc 1182 . . 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
) )
35629, 355eqeltrd 2370 . 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
) )
357 simpl 443 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  ->  A  e.  CC )
358 rpcn 10378 . . . . . . 7  |-  ( k  e.  RR+  ->  k  e.  CC )
359358adantl 452 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  e.  CC )
360 rpne0 10385 . . . . . . 7  |-  ( k  e.  RR+  ->  k  =/=  0 )
361360adantl 452 . . . . . 6  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
k  =/=  0 )
362357, 359, 361divcld 9552 . . . . 5  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( A  /  k
)  e.  CC )
363 addcl 8835 . . . . 5  |-  ( ( 1  e.  CC  /\  ( A  /  k
)  e.  CC )  ->  ( 1  +  ( A  /  k
) )  e.  CC )
3649, 362, 363sylancr 644 . . . 4  |-  ( ( A  e.  CC  /\  k  e.  RR+ )  -> 
( 1  +  ( A  /  k ) )  e.  CC )
365364,