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) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

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 8 12 reccld 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
49 45 48 syldanl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
50 49 adantlr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 / x ) e. CC )
51 50 1cxpd 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 ^c ( 1 / x ) ) = 1 )
52 simplr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> A = 0 )
53 52 oveq1d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( A x. x ) = ( 0 x. x ) )
54 45 ad2antrr 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> x e. CC )
55 54 mul02d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 0 x. x ) = 0 )
56 53 55 eqtrd 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( A x. x ) = 0 )
57 56 oveq2d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) = ( 1 + 0 ) )
58 1p0e1 
 |-  ( 1 + 0 ) = 1
59 57 58 eqtrdi 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) = 1 )
60 59 oveq1d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) = ( 1 ^c ( 1 / x ) ) )
61 52 fveq2d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( exp ` A ) = ( exp ` 0 ) )
62 ef0 
 |-  ( exp ` 0 ) = 1
63 61 62 eqtrdi 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( exp ` A ) = 1 )
64 51 60 63 3eqtr4d 
 |-  ( ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) = ( exp ` A ) )
65 64 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 ) ) )
66 ifid 
 |-  if ( x = 0 , ( exp ` A ) , ( exp ` A ) ) = ( exp ` A )
67 65 66 eqtrdi 
 |-  ( ( ( A e. CC /\ x e. S ) /\ A = 0 ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
68 iftrue 
 |-  ( x = 0 -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
69 68 adantl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ x = 0 ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) = ( exp ` A ) )
70 67 69 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 ) )
71 mulrid 
 |-  ( A e. CC -> ( A x. 1 ) = A )
72 71 ad2antrr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A = 0 \/ x = 0 ) ) -> ( A x. 1 ) = A )
73 72 fveq2d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A = 0 \/ x = 0 ) ) -> ( exp ` ( A x. 1 ) ) = ( exp ` A ) )
74 70 73 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 ) ) )
75 47 74 sylbida 
 |-  ( ( ( 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 ) ) )
76 mulne0b 
 |-  ( ( A e. CC /\ x e. CC ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> ( A x. x ) =/= 0 ) )
77 45 76 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> ( A x. x ) =/= 0 ) )
78 df-ne 
 |-  ( ( A x. x ) =/= 0 <-> -. ( A x. x ) = 0 )
79 77 78 bitrdi 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( A =/= 0 /\ x =/= 0 ) <-> -. ( A x. x ) = 0 ) )
80 simprr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> x =/= 0 )
81 80 neneqd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> -. x = 0 )
82 81 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 ) ) )
83 ax-1cn 
 |-  1 e. CC
84 45 14 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( A x. x ) e. CC )
85 addcl 
 |-  ( ( 1 e. CC /\ ( A x. x ) e. CC ) -> ( 1 + ( A x. x ) ) e. CC )
86 83 84 85 sylancr 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. CC )
87 86 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 + ( A x. x ) ) e. CC )
88 eqid 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
89 88 dvlog2lem 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
90 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
91 90 logdmss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
92 89 91 sstri 
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
93 eqid 
 |-  ( abs o. - ) = ( abs o. - )
94 93 cnmetdval 
 |-  ( ( ( 1 + ( A x. x ) ) e. CC /\ 1 e. CC ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) )
95 86 83 94 sylancl 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) )
96 pncan2 
 |-  ( ( 1 e. CC /\ ( A x. x ) e. CC ) -> ( ( 1 + ( A x. x ) ) - 1 ) = ( A x. x ) )
97 83 84 96 sylancr 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) - 1 ) = ( A x. x ) )
98 97 fveq2d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( ( 1 + ( A x. x ) ) - 1 ) ) = ( abs ` ( A x. x ) ) )
99 95 98 eqtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) = ( abs ` ( A x. x ) ) )
100 84 abscld 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) e. RR )
101 34 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) + 1 ) e. RR )
102 45 abscld 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` x ) e. RR )
103 101 102 remulcld 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) e. RR )
104 1red 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. RR )
105 absmul 
 |-  ( ( A e. CC /\ x e. CC ) -> ( abs ` ( A x. x ) ) = ( ( abs ` A ) x. ( abs ` x ) ) )
106 45 105 syldan 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) = ( ( abs ` A ) x. ( abs ` x ) ) )
107 32 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` A ) e. RR )
108 107 33 syl 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) + 1 ) e. RR )
109 45 absge0d 
 |-  ( ( A e. CC /\ x e. S ) -> 0 <_ ( abs ` x ) )
110 107 lep1d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` A ) <_ ( ( abs ` A ) + 1 ) )
111 107 108 102 109 110 lemul1ad 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( abs ` A ) x. ( abs ` x ) ) <_ ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) )
112 106 111 eqbrtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) <_ ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) )
113 0cn 
 |-  0 e. CC
114 93 cnmetdval 
 |-  ( ( x e. CC /\ 0 e. CC ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
115 45 113 114 sylancl 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
116 45 subid1d 
 |-  ( ( A e. CC /\ x e. S ) -> ( x - 0 ) = x )
117 116 fveq2d 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )
118 115 117 eqtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) = ( abs ` x ) )
119 simpr 
 |-  ( ( A e. CC /\ x e. S ) -> x e. S )
120 119 1 eleqtrdi 
 |-  ( ( A e. CC /\ x e. S ) -> x e. ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) )
121 30 a1i 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs o. - ) e. ( *Met ` CC ) )
122 41 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 / ( ( abs ` A ) + 1 ) ) e. RR* )
123 0cnd 
 |-  ( ( A e. CC /\ x e. S ) -> 0 e. CC )
124 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 ) ) ) )
125 121 122 123 45 124 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 ) ) ) )
126 120 125 mpbid 
 |-  ( ( A e. CC /\ x e. S ) -> ( x ( abs o. - ) 0 ) < ( 1 / ( ( abs ` A ) + 1 ) ) )
127 118 126 eqbrtrrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` x ) < ( 1 / ( ( abs ` A ) + 1 ) ) )
128 38 adantr 
 |-  ( ( A e. CC /\ x e. S ) -> 0 < ( ( abs ` A ) + 1 ) )
129 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 ) ) ) )
130 102 104 108 128 129 syl112anc 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) < 1 <-> ( abs ` x ) < ( 1 / ( ( abs ` A ) + 1 ) ) ) )
131 127 130 mpbird 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( ( abs ` A ) + 1 ) x. ( abs ` x ) ) < 1 )
132 100 103 104 112 131 lelttrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( abs ` ( A x. x ) ) < 1 )
133 99 132 eqbrtrd 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) ( abs o. - ) 1 ) < 1 )
134 1rp 
 |-  1 e. RR+
135 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
136 134 135 mp1i 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. RR* )
137 1cnd 
 |-  ( ( A e. CC /\ x e. S ) -> 1 e. CC )
138 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 ) )
139 121 136 137 86 138 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 ) )
140 133 139 mpbird 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
141 92 140 sselid 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) e. ( CC \ { 0 } ) )
142 eldifsni 
 |-  ( ( 1 + ( A x. x ) ) e. ( CC \ { 0 } ) -> ( 1 + ( A x. x ) ) =/= 0 )
143 141 142 syl 
 |-  ( ( A e. CC /\ x e. S ) -> ( 1 + ( A x. x ) ) =/= 0 )
144 143 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 + ( A x. x ) ) =/= 0 )
145 45 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> x e. CC )
146 145 80 reccld 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
147 87 144 146 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 ) ) ) ) ) )
148 86 143 logcld 
 |-  ( ( A e. CC /\ x e. S ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
149 148 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
150 146 149 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 ) ) )
151 simpll 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> A e. CC )
152 simprl 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> A =/= 0 )
153 151 152 dividd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A / A ) = 1 )
154 153 oveq1d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( ( A / A ) / x ) = ( 1 / x ) )
155 151 151 145 152 80 divdiv1d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( ( A / A ) / x ) = ( A / ( A x. x ) ) )
156 154 155 eqtr3d 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( 1 / x ) = ( A / ( A x. x ) ) )
157 156 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 ) ) ) )
158 84 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A x. x ) e. CC )
159 77 biimpa 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A =/= 0 /\ x =/= 0 ) ) -> ( A x. x ) =/= 0 )
160 149 151 158 159 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 ) ) ) )
161 150 157 160 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 ) ) ) )
162 161 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 ) ) ) ) )
163 82 147 162 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 ) ) ) ) )
164 163 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 ) ) ) ) ) )
165 79 164 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 ) ) ) ) ) )
166 165 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 ) ) ) ) )
167 28 29 75 166 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 ) ) ) ) ) )
168 167 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 ) ) ) ) ) ) )
169 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 ) ) ) ) )
170 1cnd 
 |-  ( ( ( A e. CC /\ x e. S ) /\ ( A x. x ) = 0 ) -> 1 e. CC )
171 148 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( log ` ( 1 + ( A x. x ) ) ) e. CC )
172 84 adantr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( A x. x ) e. CC )
173 simpr 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> -. ( A x. x ) = 0 )
174 173 neqned 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( A x. x ) =/= 0 )
175 171 172 174 divcld 
 |-  ( ( ( A e. CC /\ x e. S ) /\ -. ( A x. x ) = 0 ) -> ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) e. CC )
176 170 175 ifclda 
 |-  ( ( A e. CC /\ x e. S ) -> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) e. CC )
177 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 ) ) ) ) )
178 eqidd 
 |-  ( A e. CC -> ( y e. CC |-> ( exp ` ( A x. y ) ) ) = ( y e. CC |-> ( exp ` ( A x. y ) ) ) )
179 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 ) ) ) ) )
180 179 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 ) ) ) ) ) )
181 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 ) )
182 181 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 ) ) )
183 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 ) ) ) )
184 183 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 ) ) ) ) )
185 182 184 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 ) ) ) ) )
186 180 185 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 ) ) ) ) ) )
187 176 177 178 186 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 ) ) ) ) ) ) )
188 168 169 187 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 ) ) ) ) ) )
189 eqidd 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) = ( x e. S |-> ( 1 + ( A x. x ) ) ) )
190 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 ) ) ) ) )
191 eqeq1 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( y = 1 <-> ( 1 + ( A x. x ) ) = 1 ) )
192 fveq2 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( log ` y ) = ( log ` ( 1 + ( A x. x ) ) ) )
193 oveq1 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( y - 1 ) = ( ( 1 + ( A x. x ) ) - 1 ) )
194 192 193 oveq12d 
 |-  ( y = ( 1 + ( A x. x ) ) -> ( ( log ` y ) / ( y - 1 ) ) = ( ( log ` ( 1 + ( A x. x ) ) ) / ( ( 1 + ( A x. x ) ) - 1 ) ) )
195 191 194 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 ) ) ) )
196 140 189 190 195 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 ) ) ) ) )
197 58 eqeq2i 
 |-  ( ( 1 + ( A x. x ) ) = ( 1 + 0 ) <-> ( 1 + ( A x. x ) ) = 1 )
198 137 84 123 addcand 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) = ( 1 + 0 ) <-> ( A x. x ) = 0 ) )
199 197 198 bitr3id 
 |-  ( ( A e. CC /\ x e. S ) -> ( ( 1 + ( A x. x ) ) = 1 <-> ( A x. x ) = 0 ) )
200 97 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 ) ) )
201 199 200 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 ) ) ) )
202 201 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 ) ) ) ) )
203 196 202 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 ) ) ) ) )
204 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
205 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
206 205 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
207 206 a1i 
 |-  ( A e. CC -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
208 1cnd 
 |-  ( A e. CC -> 1 e. CC )
209 207 207 208 cnmptc 
 |-  ( A e. CC -> ( x e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
210 id 
 |-  ( A e. CC -> A e. CC )
211 207 207 210 cnmptc 
 |-  ( A e. CC -> ( x e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
212 207 cnmptid 
 |-  ( A e. CC -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
213 205 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
214 213 a1i 
 |-  ( A e. CC -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
215 oveq12 
 |-  ( ( u = A /\ v = x ) -> ( u x. v ) = ( A x. x ) )
216 207 211 212 207 207 214 215 cnmpt12 
 |-  ( A e. CC -> ( x e. CC |-> ( A x. x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
217 205 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 207 209 216 218 cnmpt12f 
 |-  ( A e. CC -> ( x e. CC |-> ( 1 + ( A x. x ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
220 204 207 44 219 cnmpt1res 
 |-  ( A e. CC -> ( x e. S |-> ( 1 + ( A x. x ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t S ) Cn ( TopOpen ` CCfld ) ) )
221 140 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 92 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 206 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 206 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 92 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 83 134 250 mp3an 
 |-  1 e. ( 1 ( ball ` ( abs o. - ) ) 1 )
252 ovex 
 |-  ( 1 / y ) e. _V
253 88 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 92 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 205 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 58 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 203 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 207 207 210 cnmptc 
 |-  ( A e. CC -> ( y e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
302 207 cnmptid 
 |-  ( A e. CC -> ( y e. CC |-> y ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
303 oveq12 
 |-  ( ( u = A /\ v = y ) -> ( u x. v ) = ( A x. y ) )
304 207 301 302 207 207 214 303 cnmpt12 
 |-  ( A e. CC -> ( y e. CC |-> ( A x. y ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
305 efcn 
 |-  exp e. ( CC -cn-> CC )
306 205 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
307 305 306 eleqtri 
 |-  exp e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
308 307 a1i 
 |-  ( A e. CC -> exp e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
309 207 304 308 cnmpt11f 
 |-  ( A e. CC -> ( y e. CC |-> ( exp ` ( A x. y ) ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
310 176 fmpttd 
 |-  ( A e. CC -> ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) : S --> CC )
311 310 231 ffvelcdmd 
 |-  ( A e. CC -> ( ( x e. S |-> if ( ( A x. x ) = 0 , 1 , ( ( log ` ( 1 + ( A x. x ) ) ) / ( A x. x ) ) ) ) ` 0 ) e. CC )
312 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
313 312 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 ) ) )
314 309 311 313 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 ) ) )
315 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 ) )
316 300 314 315 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 ) )
317 188 316 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 ) )
318 205 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
319 318 a1i 
 |-  ( A e. CC -> ( TopOpen ` CCfld ) e. Top )
320 205 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
321 320 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 ) )
322 30 31 41 321 mp3an2i 
 |-  ( A e. CC -> ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) e. ( TopOpen ` CCfld ) )
323 1 322 eqeltrid 
 |-  ( A e. CC -> S e. ( TopOpen ` CCfld ) )
324 isopn3i 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S )
325 318 323 324 sylancr 
 |-  ( A e. CC -> ( ( int ` ( TopOpen ` CCfld ) ) ` S ) = S )
326 231 325 eleqtrrd 
 |-  ( A e. CC -> 0 e. ( ( int ` ( TopOpen ` CCfld ) ) ` S ) )
327 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
328 327 ad2antrr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ x = 0 ) -> ( exp ` A ) e. CC )
329 83 15 85 sylancr 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( 1 + ( A x. x ) ) e. CC )
330 329 48 cxpcld 
 |-  ( ( ( A e. CC /\ x e. CC ) /\ -. x = 0 ) -> ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) e. CC )
331 328 330 ifclda 
 |-  ( ( A e. CC /\ x e. CC ) -> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) e. CC )
332 331 fmpttd 
 |-  ( A e. CC -> ( x e. CC |-> if ( x = 0 , ( exp ` A ) , ( ( 1 + ( A x. x ) ) ^c ( 1 / x ) ) ) ) : CC --> CC )
333 312 312 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 ) ) )
334 319 44 326 332 333 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 ) ) )
335 317 334 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 ) )
336 312 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 ) )
337 4 27 335 336 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 ) )
338 25 337 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 ) )
339 simpl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> A e. CC )
340 rpcn 
 |-  ( k e. RR+ -> k e. CC )
341 340 adantl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> k e. CC )
342 rpne0 
 |-  ( k e. RR+ -> k =/= 0 )
343 342 adantl 
 |-  ( ( A e. CC /\ k e. RR+ ) -> k =/= 0 )
344 339 341 343 divcld 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( A / k ) e. CC )
345 addcl 
 |-  ( ( 1 e. CC /\ ( A / k ) e. CC ) -> ( 1 + ( A / k ) ) e. CC )
346 83 344 345 sylancr 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( 1 + ( A / k ) ) e. CC )
347 346 341 cxpcld 
 |-  ( ( A e. CC /\ k e. RR+ ) -> ( ( 1 + ( A / k ) ) ^c k ) e. CC )
348 oveq2 
 |-  ( k = ( 1 / x ) -> ( A / k ) = ( A / ( 1 / x ) ) )
349 348 oveq2d 
 |-  ( k = ( 1 / x ) -> ( 1 + ( A / k ) ) = ( 1 + ( A / ( 1 / x ) ) ) )
350 id 
 |-  ( k = ( 1 / x ) -> k = ( 1 / x ) )
351 349 350 oveq12d 
 |-  ( k = ( 1 / x ) -> ( ( 1 + ( A / k ) ) ^c k ) = ( ( 1 + ( A / ( 1 / x ) ) ) ^c ( 1 / x ) ) )
352 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) ) = ( ( TopOpen ` CCfld ) |`t ( 0 [,) +oo ) )
353 327 347 351 205 352 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 ) ) )
354 338 353 mpbird 
 |-  ( A e. CC -> ( k e. RR+ |-> ( ( 1 + ( A / k ) ) ^c k ) ) ~~>r ( exp ` A ) )