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		mulrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 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	ffvelcdmd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ 𝑆 ↦ 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 ‘ 𝐴 ) )