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