Metamath Proof Explorer

Theorem efrlim

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 ). (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypothesis efrlim.1 
|- S = ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) )
Assertion efrlim 
|- ( A e. CC -> ( k e. RR+ |-> ( ( 1 + ( A / k ) ) ^c k ) ) ~~>r ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 efrlim.1 
 |-  S = ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) )
2 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
3 ax-resscn 
 |-  RR C_ CC
4 2 3 sstri 
 |-  ( 0 [,) +oo ) C_ CC
5 4 sseli 
 |-  ( x e. ( 0 [,) +oo ) -> x e. CC )
6 simpll 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> A e. CC )
7 1cnd 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> 1 e. CC )
8 simplr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> x e. CC )
9 ax-1ne0 
 |-  1 =/= 0
10 9 a1i 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> 1 =/= 0 )
11 simpr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> -. x = 0 )
12 11 neqned 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> x =/= 0 )
13 6 7 8 10 12 divdiv2d 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( A / ( 1 / x ) ) = ( ( A x. x ) / 1 ) )
14 mulcl 
 |-  ( ( A e. CC /\ x e. CC ) -> ( A x. x ) e. CC )
15 14 adantr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( A x. x ) e. CC )
16 15 div1d 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( ( A x. x ) / 1 ) = ( A x. x ) )
17 13 16 eqtrd 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( A / ( 1 / x ) ) = ( A x. x ) )
18 17 oveq2d 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( 1 + ( A / ( 1 / x ) ) ) = ( 1 + ( A x. x ) ) )
19 18 oveq1d 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( ( 1 + ( A / ( 1 / x ) ) ) ^c ( 1 / x ) ) = ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) )
20 19 ifeq2da 
 |-  ( ( 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 ) ) ) )
21 5 20 sylan2 
 |-  ( ( 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 ) ) ) )
22 21 mpteq2dva 
 |-  ( 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 ) ) ) ) )
23 resmpt 
 |-  ( ( 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 ) ) ) ) )
24 4 23 ax-mp 
 |-  ( ( 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 ) ) ) )
25 22 24 eqtr4di 
 |-  ( 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 ) ) )
26 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
27 26 a1i 
 |-  ( A e. CC -> 0 e. ( 0 [,) +oo ) )
28 eqeq2 
 |-  ( ( 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 ) ) ) ) ) ) )
29 eqeq2 
 |-  ( ( 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 ) ) ) ) ) ) )
30 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
31 0cnd 
 |-  ( A e. CC -> 0 e. CC )
32 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
33 peano2re 
 |-  ( ( abs ` A ) e. RR -> ( ( abs ` A ) + 1 ) e. RR )
34 32 33 syl 
 |-  ( A e. CC -> ( ( abs ` A ) + 1 ) e. RR )
35 0red 
 |-  ( A e. CC -> 0 e. RR )
36 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
37 32 ltp1d 
 |-  ( A e. CC -> ( abs ` A ) < ( ( abs ` A ) + 1 ) )
38 35 32 34 36 37 lelttrd 
 |-  ( A e. CC -> 0 < ( ( abs ` A ) + 1 ) )
39 34 38 elrpd 
 |-  ( A e. CC -> ( ( abs ` A ) + 1 ) e. RR+ )
40 39 rpreccld 
 |-  ( A e. CC -> ( 1 / ( ( abs ` A ) + 1 ) ) e. RR+ )
41 40 rpxrd 
 |-  ( A e. CC -> ( 1 / ( ( abs ` A ) + 1 ) ) e. RR* )
42 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( 1 / ( ( abs ` A ) + 1 ) ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) C_ CC )
43 30 31 41 42 mp3an2i 
 |-  ( A e. CC -> ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) C_ CC )
44 1 43 eqsstrid 
 |-  ( A e. CC -> S C_ CC )
45 44 sselda 
 |-  ( ( A e. CC /\ x e. S ) -> x e. CC )
46 mul0or 
 |-  ( ( A e. CC /\ x e. CC ) -> ( ( A x. x ) = 0 <-> ( A = 0 \/ x = 0 ) ) )
47 45 46 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( A x. x ) = 0 <-> ( A = 0 \/ x = 0 ) ) )
48 47 biimpa 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A x. x ) = 0 ) -> ( A = 0 \/ x = 0 ) )
49 8 12 reccld 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
50 45 49 syldanl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
51 50 adantlr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
52 51 1cxpd 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 ^c ( 1 / x ) ) = 1 )
53 simplr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> A = 0 )
54 53 oveq1d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( A x. x ) = ( 0 x. x ) )
55 45 ad2antrr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> x e. CC )
56 55 mul02d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 0 x. x ) = 0 )
57 54 56 eqtrd 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( A x. x ) = 0 )
58 57 oveq2d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) = ( 1 + 0 ) )
59 1p0e1 
 |-  ( 1 + 0 ) = 1
60 58 59 eqtrdi 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) = 1 )
61 60 oveq1d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) = ( 1 ^c ( 1 / x ) ) )
62 53 fveq2d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( exp ` A ) = ( exp ` 0 ) )
63 ef0 
 |-  ( exp ` 0 ) = 1
64 62 63 eqtrdi 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( exp ` A ) = 1 )
65 52 61 64 3eqtr4d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) = ( exp ` A ) )
66 65 ifeq2da 
 |-  ( ( ( 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 ) ) )
67 ifid 
 |-  if ( x = 0 , ( exp ` A ) , ( exp ` A ) ) = ( exp ` A )
68 66 67 eqtrdi 
 |-  ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
69 iftrue 
 |-  ( x = 0 -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
70 69 adantl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ x = 0 ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
71 68 70 jaodan 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A = 0 \/ x = 0 ) ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
72 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
73 72 ad2antrr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A = 0 \/ x = 0 ) ) -> ( A x. 1 ) = A )
74 73 fveq2d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A = 0 \/ x = 0 ) ) -> ( exp ` ( A x. 1 ) ) = ( exp ` A ) )
75 71 74 eqtr4d 
 |-  ( ( ( 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 ) ) )
76 48 75 syldan 
 |-  ( ( ( 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 ) ) )
77 mulne0b 
 |-  ( ( A e. CC /\ x e. CC ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> ( A x. x ) =/= 0 ) )
78 45 77 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> ( A x. x ) =/= 0 ) )
79 df-ne 
 |-  ( ( A x. x ) =/= 0 <-> -. ( A x. x ) = 0 )
80 78 79 bitrdi 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> -. ( A x. x ) = 0 ) )
81 simprr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> x =/= 0 )
82 81 neneqd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> -. x = 0 )
83 82 iffalsed 
 |-  ( ( ( 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 ) ) )
84 ax-1cn 
 |-  1 e. CC
85 45 14 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( A x. x ) e. CC )
86 addcl 
 |-  ( ( 1 e. CC /\ ( A x. x ) e. CC ) -> ( 1 + ( A x. x ) ) e. CC )
87 84 85 86 sylancr 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. CC )
88 87 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 + ( A x. x ) ) e. CC )
89 eqid 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
90 89 dvlog2lem 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
91 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
92 91 logdmss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
93 90 92 sstri 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
94 eqid 
 |-  ( abs o. - ) = ( abs o. - )
95 94 cnmetdval 
 |-  ( ( ( 1 + ( A x. x ) ) e. CC /\ 1 e. CC ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) )
96 87 84 95 sylancl 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) )
97 pncan2 
 |-  ( ( 1 e. CC /\ ( A x. x ) e. CC ) -> ( ( 1 + ( A x. x ) ) - 1 ) = ( A x. x ) )
98 84 85 97 sylancr 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) - 1 ) = ( A x. x ) )
99 98 fveq2d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) = ( abs ` ( A x. x ) ) )
100 96 99 eqtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( A x. x ) ) )
101 85 abscld 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) e. RR )
102 34 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) + 1 ) e. RR )
103 45 abscld 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` x ) e. RR )
104 102 103 remulcld 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) e. RR )
105 1red 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. RR )
106 absmul 
 |-  ( ( A e. CC /\ x e. CC ) -> ( abs ` ( A x. x ) ) = ( ( abs ` A ) x. ( abs ` x ) ) )
107 45 106 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) = ( ( abs ` A ) x. ( abs ` x ) ) )
108 32 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` A ) e. RR )
109 108 33 syl 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) + 1 ) e. RR )
110 45 absge0d 
 |-  ( ( A e. CC /\ x e. S ) -> 0 <_ ( abs ` x ) )
111 108 lep1d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` A ) <_ ( ( abs ` A ) + 1 ) )
112 108 109 103 110 111 lemul1ad 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) x. ( abs ` x ) ) <_ ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) )
113 107 112 eqbrtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) <_ ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) )
114 0cn 
 |-  0 e. CC
115 94 cnmetdval 
 |-  ( ( x e. CC /\ 0 e. CC ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
116 45 114 115 sylancl 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
117 45 subid1d 
 |-  ( ( A e. CC /\ x e. S ) -> ( x - 0 ) = x )
118 117 fveq2d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )
119 116 118 eqtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) = ( abs ` x ) )
120 simpr 
 |-  ( ( A e. CC /\ x e. S ) -> x e. S )
121 120 1 eleqtrdi 
 |-  ( ( A e. CC /\ x e. S ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) )
122 30 a1i 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs o. - ) e. ( *Met ` CC ) )
123 41 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 / ( ( abs ` A ) + 1 ) ) e. RR* )
124 0cnd 
 |-  ( ( A e. CC /\ x e. S ) -> 0 e. CC )
125 elbl3 
 |-  ( ( ( ( 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 ) ) ) )
126 122 123 124 45 125 syl22anc 
 |-  ( ( A e. CC /\ x e. S ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) <-> ( x ( abs o. - ) 0 ) < ( 1 / ( ( abs ` A ) + 1 ) ) ) )
127 121 126 mpbid 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) < ( 1 / ( ( abs ` A ) + 1 ) ) )
128 119 127 eqbrtrrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` x ) < ( 1 / ( ( abs ` A ) + 1 ) ) )
129 38 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> 0 < ( ( abs ` A ) + 1 ) )
130 ltmuldiv2 
 |-  ( ( ( 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 ) ) ) )
131 103 105 109 129 130 syl112anc 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) < 1 <-> ( abs ` x ) < ( 1 / ( ( abs ` A ) + 1 ) ) ) )
132 128 131 mpbird 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) < 1 )
133 101 104 105 113 132 lelttrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) < 1 )
134 100 133 eqbrtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) < 1 )
135 1rp 
 |-  1 e. RR+
136 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
137 135 136 mp1i 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. RR* )
138 1cnd 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. CC )
139 elbl3 
 |-  ( ( ( ( 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 ) )
140 122 137 138 87 139 syl22anc 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) < 1 ) )
141 134 140 mpbird 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
142 93 141 sseldi 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. ( CC \ { 0 } ) )
143 eldifsni 
 |-  ( ( 1 + ( A x. x ) ) e. ( CC \ { 0 } ) -> ( 1 + ( A x. x ) ) =/= 0 )
144 142 143 syl 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) =/= 0 )
145 144 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 + ( A x. x ) ) =/= 0 )
146 45 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> x e. CC )
147 146 81 reccld 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
148 88 145 147 cxpefd 
 |-  ( ( ( 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 ) ) ) ) ) )
149 87 144 logcld 
 |-  ( ( A e. CC /\ x e. S ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
150 149 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
151 147 150 mulcomd 
 |-  ( ( ( 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 ) ) )
152 simpll 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> A e. CC )
153 simprl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> A =/= 0 )
154 152 153 dividd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A / A ) = 1 )
155 154 oveq1d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( ( A / A ) / x ) = ( 1 / x ) )
156 152 152 146 153 81 divdiv1d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( ( A / A ) / x ) = ( A / ( A x. x ) ) )
157 155 156 eqtr3d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 / x ) = ( A / ( A x. x ) ) )
158 157 oveq2d 
 |-  ( ( ( 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 ) ) ) )
159 85 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A x. x ) e. CC )
160 78 biimpa 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A x. x ) =/= 0 )
161 150 152 159 160 div12d 
 |-  ( ( ( 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 ) ) ) )
162 151 158 161 3eqtrd 
 |-  ( ( ( 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 ) ) ) )
163 162 fveq2d 
 |-  ( ( ( 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 ) ) ) ) )
164 83 148 163 3eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
165 164 ex 
 |-  ( ( 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 ) ) ) ) ) )
166 80 165 sylbird 
 |-  ( ( 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 ) ) ) ) ) )
167 166 imp 
 |-  ( ( ( 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 ) ) ) ) )
168 28 29 76 167 ifbothda 
 |-  ( ( 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 ) ) ) ) ) )
169 168 mpteq2dva 
 |-  ( 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 ) ) ) ) ) ) )
170 44 resmptd 
 |-  ( 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 ) ) ) ) )
171 1cnd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A x. x ) = 0 ) -> 1 e. CC )
172 149 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
173 85 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( A x. x ) e. CC )
174 simpr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> -. ( A x. x ) = 0 )
175 174 neqned 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( A x. x ) =/= 0 )
176 172 173 175 divcld 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) e. CC )
177 171 176 ifclda 
 |-  ( ( A e. CC /\ x e. S ) -> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) e. CC )
178 eqidd 
 |-  ( 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 ) ) ) ) )
179 eqidd 
 |-  ( A e. CC -> ( y e. CC |-> ( exp ` ( A x. y ) ) ) = ( y e. CC |-> ( exp ` ( A x. y ) ) ) )
180 oveq2 
 |-  ( 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 ) ) ) ) )
181 180 fveq2d 
 |-  ( 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 ) ) ) ) ) )
182 oveq2 
 |-  ( 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 ) )
183 182 fveq2d 
 |-  ( 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 ) ) )
184 oveq2 
 |-  ( 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 ) ) ) )
185 184 fveq2d 
 |-  ( 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 ) ) ) ) )
186 183 185 ifsb 
 |-  ( 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 ) ) ) ) )
187 181 186 eqtrdi 
 |-  ( 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 ) ) ) ) ) )
188 177 178 179 187 fmptco 
 |-  ( 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 ) ) ) ) ) ) )
189 169 170 188 3eqtr4d 
 |-  ( 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 ) ) ) ) ) )
190 eqidd 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) = ( x e. S |-> ( 1 + ( A x. x ) ) ) )
191 eqidd 
 |-  ( 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 ) ) ) ) )
192 eqeq1 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( y = 1 <-> ( 1 + ( A x. x ) ) = 1 ) )
193 fveq2 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( log ` y ) = ( log ` ( 1 + ( A x. x ) ) ) )
194 oveq1 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( y - 1 ) = ( ( 1 + ( A x. x ) ) - 1 ) )
195 193 194 oveq12d 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( ( log ` y ) / ( y - 1 ) ) = ( ( log ` ( 1 + ( A x. x ) ) ) / ( ( 1 + ( A x. x ) ) - 1 ) ) )
196 192 195 ifbieq2d 
 |-  ( 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 ) ) ) )
197 141 190 191 196 fmptco 
 |-  ( 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 ) ) ) ) )
198 59 eqeq2i 
 |-  ( ( 1 + ( A x. x ) ) = ( 1 + 0 ) <-> ( 1 + ( A x. x ) ) = 1 )
199 138 85 124 addcand 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) = ( 1 + 0 ) <-> ( A x. x ) = 0 ) )
200 198 199 bitr3id 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) = 1 <-> ( A x. x ) = 0 ) )
201 98 oveq2d 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( log ` ( 1 + ( A x. x ) ) ) / ( ( 1 + ( A x. x ) ) - 1 ) ) = ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) )
202 200 201 ifbieq2d 
 |-  ( ( 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 ) ) ) )
203 202 mpteq2dva 
 |-  ( 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 ) ) ) ) )
204 197 203 eqtrd 
 |-  ( 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 ) ) ) ) )
205 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
206 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
207 206 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
208 207 a1i 
 |-  ( A e. CC -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
209 1cnd 
 |-  ( A e. CC -> 1 e. CC )
210 208 208 209 cnmptc 
 |-  ( A e. CC -> ( x e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
211 id 
 |-  ( A e. CC -> A e. CC )
212 208 208 211 cnmptc 
 |-  ( A e. CC -> ( x e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
213 208 cnmptid 
 |-  ( A e. CC -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
214 206 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
215 214 a1i 
 |-  ( A e. CC -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
216 208 212 213 215 cnmpt12f 
 |-  ( A e. CC -> ( x e. CC |-> ( A x. x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
217 206 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
218 217 a1i 
 |-  ( A e. CC -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
219 208 210 216 218 cnmpt12f 
 |-  ( A e. CC -> ( x e. CC |-> ( 1 + ( A x. x ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
220 205 208 44 219 cnmpt1res 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
221 141 fmpttd 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) : S --> ( 1 ( ball ` ( abs o. - ) ) 1 ) )
222 221 frnd 
 |-  ( A e. CC -> ran ( x e. S |-> ( 1 + ( A x. x ) ) ) C_ ( 1 ( ball ` ( abs o. - ) ) 1 ) )
223 difss 
 |-  ( CC \ { 0 } ) C_ CC
224 93 223 sstri 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC
225 224 a1i 
 |-  ( A e. CC -> ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
226 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) 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 ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ) )
227 207 222 225 226 mp3an2i 
 |-  ( A e. CC -> ( ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ) )
228 220 227 mpbid 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) )
229 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( 1 / ( ( abs ` A ) + 1 ) ) e. RR+ ) -> 0 e. ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) )
230 30 31 40 229 mp3an2i 
 |-  ( A e. CC -> 0 e. ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) )
231 230 1 eleqtrrdi 
 |-  ( A e. CC -> 0 e. S )
232 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
233 207 44 232 sylancr 
 |-  ( A e. CC -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
234 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
235 233 234 syl 
 |-  ( A e. CC -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
236 231 235 eleqtrd 
 |-  ( A e. CC -> 0 e. U. ( ( TopOpen ` CCfld ) |`t S ) )
237 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t S ) = U. ( ( TopOpen ` CCfld ) |`t S )
238 237 cncnpi 
 |-  ( ( ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) /\ 0 e. U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 0 ) )
239 228 236 238 syl2anc 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 0 ) )
240 cnelprrecn 
 |-  CC e. { RR , CC }
241 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
242 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
243 241 242 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
244 logrncn 
 |-  ( x e. ran log -> x e. CC )
245 244 ssriv 
 |-  ran log C_ CC
246 fss 
 |-  ( ( log : ( CC \ { 0 } ) --> ran log /\ ran log C_ CC ) -> log : ( CC \ { 0 } ) --> CC )
247 243 245 246 mp2an 
 |-  log : ( CC \ { 0 } ) --> CC
248 fssres 
 |-  ( ( log : ( CC \ { 0 } ) --> CC /\ ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } ) ) -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> CC )
249 247 93 248 mp2an 
 |-  ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> CC
250 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR+ ) -> 1 e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
251 30 84 135 250 mp3an 
 |-  1 e. ( 1 ( ball ` ( abs o. - ) ) 1 )
252 ovex 
 |-  ( 1 / y ) e. _V
253 89 dvlog2 
 |-  ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) )
254 252 253 dmmpti 
 |-  dom ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
255 251 254 eleqtrri 
 |-  1 e. dom ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) )
256 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) )
257 253 fveq1i 
 |-  ( ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 1 ) = ( ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) ) ` 1 )
258 oveq2 
 |-  ( y = 1 -> ( 1 / y ) = ( 1 / 1 ) )
259 1div1e1 
 |-  ( 1 / 1 ) = 1
260 258 259 eqtrdi 
 |-  ( y = 1 -> ( 1 / y ) = 1 )
261 eqid 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) ) = ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) )
262 1ex 
 |-  1 e. _V
263 260 261 262 fvmpt 
 |-  ( 1 e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) ) ` 1 ) = 1 )
264 251 263 ax-mp 
 |-  ( ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / y ) ) ` 1 ) = 1
265 257 264 eqtr2i 
 |-  1 = ( ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 1 )
266 265 a1i 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> 1 = ( ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 1 ) )
267 fvres 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` y ) = ( log ` y ) )
268 fvres 
 |-  ( 1 e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` 1 ) = ( log ` 1 ) )
269 251 268 mp1i 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` 1 ) = ( log ` 1 ) )
270 log1 
 |-  ( log ` 1 ) = 0
271 269 270 eqtrdi 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` 1 ) = 0 )
272 267 271 oveq12d 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` y ) - ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` 1 ) ) = ( ( log ` y ) - 0 ) )
273 93 sseli 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> y e. ( CC \ { 0 } ) )
274 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
275 273 274 sylib 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. CC /\ y =/= 0 ) )
276 logcl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( log ` y ) e. CC )
277 275 276 syl 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` y ) e. CC )
278 277 subid1d 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log ` y ) - 0 ) = ( log ` y ) )
279 272 278 eqtr2d 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` y ) = ( ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` y ) - ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` 1 ) ) )
280 279 oveq1d 
 |-  ( 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 ) ) )
281 266 280 ifeq12d 
 |-  ( 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 ) ) ) )
282 281 mpteq2ia 
 |-  ( 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 ) ) ) )
283 256 206 282 dvcnp 
 |-  ( ( ( 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 ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
284 255 283 mpan2 
 |-  ( ( 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 ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
285 240 249 224 284 mp3an 
 |-  ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> if ( y = 1 , 1 , ( ( log ` y ) / ( y - 1 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` 1 )
286 oveq2 
 |-  ( x = 0 -> ( A x. x ) = ( A x. 0 ) )
287 286 oveq2d 
 |-  ( x = 0 -> ( 1 + ( A x. x ) ) = ( 1 + ( A x. 0 ) ) )
288 eqid 
 |-  ( x e. S |-> ( 1 + ( A x. x ) ) ) = ( x e. S |-> ( 1 + ( A x. x ) ) )
289 ovex 
 |-  ( 1 + ( A x. 0 ) ) e. _V
290 287 288 289 fvmpt 
 |-  ( 0 e. S -> ( ( x e. S |-> ( 1 + ( A x. x ) ) ) ` 0 ) = ( 1 + ( A x. 0 ) ) )
291 231 290 syl 
 |-  ( A e. CC -> ( ( x e. S |-> ( 1 + ( A x. x ) ) ) ` 0 ) = ( 1 + ( A x. 0 ) ) )
292 mul01 
 |-  ( A e. CC -> ( A x. 0 ) = 0 )
293 292 oveq2d 
 |-  ( A e. CC -> ( 1 + ( A x. 0 ) ) = ( 1 + 0 ) )
294 293 59 eqtrdi 
 |-  ( A e. CC -> ( 1 + ( A x. 0 ) ) = 1 )
295 291 294 eqtrd 
 |-  ( A e. CC -> ( ( x e. S |-> ( 1 + ( A x. x ) ) ) ` 0 ) = 1 )
296 295 fveq2d 
 |-  ( A e. CC -> ( ( ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` ( ( x e. S |-> ( 1 + ( A x. x ) ) ) ` 0 ) ) = ( ( ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` 1 ) )
297 285 296 eleqtrrid 
 |-  ( A e. CC -> ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> if ( y = 1 , 1 , ( ( log ` y ) / ( y - 1 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` ( ( x e. S |-> ( 1 + ( A x. x ) ) ) ` 0 ) ) )
298 cnpco 
 |-  ( ( ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) ` 0 ) /\ ( y e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> if ( y = 1 , 1 , ( ( log ` y ) / ( y - 1 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 1 ( ball ` ( abs o. - ) ) 1 ) ) CnP ( TopOpen ` CCfld ) ) ` ( ( 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 ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
299 239 297 298 syl2anc 
 |-  ( 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 ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
300 204 299 eqeltrrd 
 |-  ( A e. CC -> ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
301 208 208 211 cnmptc 
 |-  ( A e. CC -> ( y e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
302 208 cnmptid 
 |-  ( A e. CC -> ( y e. CC |-> y ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
303 208 301 302 215 cnmpt12f 
 |-  ( A e. CC -> ( y e. CC |-> ( A x. y ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
304 efcn 
 |-  exp e. ( CC -cn-> CC )
305 206 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
306 304 305 eleqtri 
 |-  exp e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
307 306 a1i 
 |-  ( A e. CC -> exp e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
308 208 303 307 cnmpt11f 
 |-  ( A e. CC -> ( y e. CC |-> ( exp ` ( A x. y ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
309 177 fmpttd 
 |-  ( A e. CC -> ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) : S --> CC )
310 309 231 ffvelrnd 
 |-  ( A e. CC -> ( ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) ` 0 ) e. CC )
311 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
312 311 cncnpi 
 |-  ( ( ( y e. CC |-> ( exp ` ( A x. y ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ ( ( 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 ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` ( ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) ` 0 ) ) )
313 308 310 312 syl2anc 
 |-  ( A e. CC -> ( y e. CC |-> ( exp ` ( A x. y ) ) ) e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` ( ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) ` 0 ) ) )
314 cnpco 
 |-  ( ( ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) /\ ( y e. CC |-> ( exp ` ( A x. y ) ) ) e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` ( ( 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 ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
315 300 313 314 syl2anc 
 |-  ( 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 ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
316 189 315 eqeltrd 
 |-  ( A e. CC -> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) |` S ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
317 206 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
318 317 a1i 
 |-  ( A e. CC -> ( TopOpen ` CCfld ) e. Top )
319 206 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
320 319 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ ( 1 / ( ( abs ` A ) + 1 ) ) e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) e. ( TopOpen ` CCfld ) )
321 30 31 41 320 mp3an2i 
 |-  ( A e. CC -> ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) e. ( TopOpen ` CCfld ) )
322 1 321 eqeltrid 
 |-  ( A e. CC -> S e. ( TopOpen ` CCfld ) )
323 isopn3i 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S )
324 317 322 323 sylancr 
 |-  ( A e. CC -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S )
325 231 324 eleqtrrd 
 |-  ( A e. CC -> 0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` S ) )
326 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
327 326 ad2antrr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ x = 0 ) -> ( exp ` A ) e. CC )
328 84 15 86 sylancr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) e. CC )
329 328 49 cxpcld 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) e. CC )
330 327 329 ifclda 
 |-  ( ( A e. CC /\ x e. CC ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) e. CC )
331 330 fmpttd 
 |-  ( A e. CC -> ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) : CC --> CC )
332 311 311 cnprest 
 |-  ( ( ( ( TopOpen ` CCfld ) e. Top /\ S C_ CC ) /\ ( 0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` 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 ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` 0 ) <-> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) |` S ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) ) )
333 318 44 325 331 332 syl22anc 
 |-  ( A e. CC -> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` 0 ) <-> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) |` S ) e. ( ( ( ( TopOpen ` CCfld ) |`t S ) CnP ( TopOpen ` CCfld ) ) ` 0 ) ) )
334 316 333 mpbird 
 |-  ( A e. CC -> ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
335 311 cnpresti 
 |-  ( ( ( 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 ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` 0 ) ) -> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) |` ( 0 [,) +oo ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
336 4 27 334 335 mp3an2i 
 |-  ( A e. CC -> ( ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) |` ( 0 [,) +oo ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
337 25 336 eqeltrd 
 |-  ( A e. CC -> ( x e. ( 0 [,) +oo ) |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A / ( 1 / x ) ) ) ^c ( 1 / x ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) )
338 simpl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> A e. CC )
339 rpcn 
 |-  ( k e. RR+ -> k e. CC )
340 339 adantl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> k e. CC )
341 rpne0 
 |-  ( k e. RR+ -> k =/= 0 )
342 341 adantl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> k =/= 0 )
343 338 340 342 divcld 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( A / k ) e. CC )
344 addcl 
 |-  ( ( 1 e. CC /\ ( A / k ) e. CC ) -> ( 1 + ( A / k ) ) e. CC )
345 84 343 344 sylancr 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( 1 + ( A / k ) ) e. CC )
346 345 340 cxpcld 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( ( 1 + ( A / k ) ) ^c k ) e. CC )
347 oveq2 
 |-  ( k = ( 1 / x ) -> ( A / k ) = ( A / ( 1 / x ) ) )
348 347 oveq2d 
 |-  ( k = ( 1 / x ) -> ( 1 + ( A / k ) ) = ( 1 + ( A / ( 1 / x ) ) ) )
349 id 
 |-  ( k = ( 1 / x ) -> k = ( 1 / x ) )
350 348 349 oveq12d 
 |-  ( k = ( 1 / x ) -> ( ( 1 + ( A / k ) ) ^c k ) = ( ( 1 + ( A / ( 1 / x ) ) ) ^c ( 1 / x ) ) )
351 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
352 326 346 350 206 351 rlimcnp3 
 |-  ( 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 ` CCfld ) |`t ( 0 [,) +oo ) ) CnP ( TopOpen ` CCfld ) ) ` 0 ) ) )
353 337 352 mpbird 
 |-  ( A e. CC -> ( k e. RR+ |-> ( ( 1 + ( A / k ) ) ^c k ) ) ~~>r ( exp ` A ) )