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 ⊢ 𝑆 = ( 0 ( ball ‘ ( abs ∘ − ) ) ( 1 / ( ( abs ‘ 𝐴 ) + 1 ) ) )
Assertion efrlim ( 𝐴 ∈ ℂ → ( 𝑘 ∈ ℝ+ ↦ ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑𝑐 𝑘 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) )

Proof

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