efrlim - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efrlim		Structured version Visualization version GIF version

Theorem efrlim 24696

Description: The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 24697). (Contributed by Mario Carneiro, 1-Mar-2015.)

**Hypothesis**
Ref	Expression
efrlim.1	⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))

**Assertion**
Ref	Expression
efrlim	⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ⁺ ↦ ((1 + (𝐴 / 𝑘))↑_𝑐𝑘)) ⇝_𝑟 (exp‘𝐴))

Distinct variable group: 𝐴,𝑘 Allowed substitution hint: 𝑆(𝑘)

Proof of Theorem efrlim Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rge0ssre 12280	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
2		ax-resscn 9993	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
3	1, 2	sstri 3612	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℂ
4	3	sseli 3599	. . . . . 6 ⊢ (𝑥 ∈ (0[,)+∞) → 𝑥 ∈ ℂ)
5		simpll 790	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → 𝐴 ∈ ℂ)
6		1cnd 10056	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → 1 ∈ ℂ)
7		simplr 792	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → 𝑥 ∈ ℂ)
8		ax-1ne0 10005	. . . . . . . . . . . 12 ⊢ 1 ≠ 0
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → 1 ≠ 0)
10		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → ¬ 𝑥 = 0)
11	10	neqned 2801	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → 𝑥 ≠ 0)
12	5, 6, 7, 9, 11	divdiv2d 10833	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (𝐴 / (1 / 𝑥)) = ((𝐴 · 𝑥) / 1))
13		mulcl 10020	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ)
14	13	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) ∈ ℂ)
15	14	div1d 10793	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → ((𝐴 · 𝑥) / 1) = (𝐴 · 𝑥))
16	12, 15	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (𝐴 / (1 / 𝑥)) = (𝐴 · 𝑥))
17	16	oveq2d 6666	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 / (1 / 𝑥))) = (1 + (𝐴 · 𝑥)))
18	17	oveq1d 6665	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)) = ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))
19	18	ifeq2da 4117	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))))
20	4, 19	sylan2 491	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (0[,)+∞)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))))
21	20	mpteq2dva 4744	. . . 4 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)))) = (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))))
22		resmpt 5449	. . . . 5 ⊢ ((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))))
23	3, 22	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))))
24	21, 23	syl6eqr 2674	. . 3 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)))) = ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ (0[,)+∞)))
25	3	a1i 11	. . . 4 ⊢ (𝐴 ∈ ℂ → (0[,)+∞) ⊆ ℂ)
26		0e0icopnf 12282	. . . . 5 ⊢ 0 ∈ (0[,)+∞)
27	26	a1i 11	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ∈ (0[,)+∞))
28		eqeq2 2633	. . . . . . . . 9 ⊢ ((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 2633	. . . . . . . . 9 ⊢ ((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		efrlim.1	. . . . . . . . . . . . . 14 ⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))
31		cnxmet 22576	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
32	31	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (abs ∘ − ) ∈ (∞Met‘ℂ))
33		0cnd 10033	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ∈ ℂ)
34		abscl 14018	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
35		peano2re 10209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘𝐴) ∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ)
36	34, 35	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 1) ∈ ℝ)
37		0red 10041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → 0 ∈ ℝ)
38		absge0 14027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
39	34	ltp1d 10954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) < ((abs‘𝐴) + 1))
40	37, 34, 36, 38, 39	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → 0 < ((abs‘𝐴) + 1))
41	36, 40	elrpd 11869	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + 1) ∈ ℝ⁺)
42	41	rpreccld 11882	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (1 / ((abs‘𝐴) + 1)) ∈ ℝ⁺)
43	42	rpxrd 11873	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (1 / ((abs‘𝐴) + 1)) ∈ ℝ^*)
44		blssm 22223	. . . . . . . . . . . . . . 15 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (1 / ((abs‘𝐴) + 1)) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⊆ ℂ)
45	32, 33, 43, 44	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⊆ ℂ)
46	30, 45	syl5eqss 3649	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → 𝑆 ⊆ ℂ)
47	46	sselda 3603	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
48		mul0or 10667	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0)))
49	47, 48	syldan 487	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0)))
50	49	biimpa 501	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → (𝐴 = 0 ∨ 𝑥 = 0))
51		simpl 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ)
52	51, 47	jca 554	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ))
53	7, 11	reccld 10794	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ)
54	52, 53	sylan 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ)
55	54	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ)
56	55	1cxpd 24453	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1↑_𝑐(1 / 𝑥)) = 1)
57		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝐴 = 0)
58	57	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = (0 · 𝑥))
59	47	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝑥 ∈ ℂ)
60	59	mul02d 10234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (0 · 𝑥) = 0)
61	58, 60	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = 0)
62	61	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = (1 + 0))
63		1p0e1 11133	. . . . . . . . . . . . . . . . 17 ⊢ (1 + 0) = 1
64	62, 63	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = 1)
65	64	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)) = (1↑_𝑐(1 / 𝑥)))
66	57	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = (exp‘0))
67		ef0 14821	. . . . . . . . . . . . . . . 16 ⊢ (exp‘0) = 1
68	66, 67	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = 1)
69	56, 65, 68	3eqtr4d 2666	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)) = (exp‘𝐴))
70	69	ifeq2da 4117	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴)))
71		ifid 4125	. . . . . . . . . . . . 13 ⊢ if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴)) = (exp‘𝐴)
72	70, 71	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘𝐴))
73		iftrue 4092	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘𝐴))
74	73	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘𝐴))
75	72, 74	jaodan 826	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘𝐴))
76		mulid1 10037	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
77	76	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (𝐴 · 1) = 𝐴)
78	77	fveq2d 6195	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (exp‘(𝐴 · 1)) = (exp‘𝐴))
79	75, 78	eqtr4d 2659	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1)))
80	50, 79	syldan 487	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1)))
81		mulne0b 10668	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0))
82	47, 81	syldan 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0))
83		df-ne 2795	. . . . . . . . . . . 12 ⊢ ((𝐴 · 𝑥) ≠ 0 ↔ ¬ (𝐴 · 𝑥) = 0)
84	82, 83	syl6bb 276	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ ¬ (𝐴 · 𝑥) = 0))
85		simprr 796	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ≠ 0)
86	85	neneqd 2799	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ¬ 𝑥 = 0)
87	86	iffalsed 4097	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))
88		ax-1cn 9994	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
89	47, 13	syldan 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝐴 · 𝑥) ∈ ℂ)
90		addcl 10018	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ (𝐴 · 𝑥) ∈ ℂ) → (1 + (𝐴 · 𝑥)) ∈ ℂ)
91	88, 89, 90	sylancr 695	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ ℂ)
92	91	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ∈ ℂ)
93		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
94	93	dvlog2lem 24398	. . . . . . . . . . . . . . . . . 18 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
95		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
96	95	logdmss 24388	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
97	94, 96	sstri 3612	. . . . . . . . . . . . . . . . 17 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})
98		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs ∘ − ) = (abs ∘ − )
99	98	cnmetdval 22574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1 + (𝐴 · 𝑥)) ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) = (abs‘((1 + (𝐴 · 𝑥)) − 1)))
100	91, 88, 99	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) = (abs‘((1 + (𝐴 · 𝑥)) − 1)))
101		pncan2 10288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ (𝐴 · 𝑥) ∈ ℂ) → ((1 + (𝐴 · 𝑥)) − 1) = (𝐴 · 𝑥))
102	88, 89, 101	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) − 1) = (𝐴 · 𝑥))
103	102	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘((1 + (𝐴 · 𝑥)) − 1)) = (abs‘(𝐴 · 𝑥)))
104	100, 103	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) = (abs‘(𝐴 · 𝑥)))
105	89	abscld 14175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ∈ ℝ)
106	36	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ)
107	47	abscld 14175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) ∈ ℝ)
108	106, 107	remulcld 10070	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) ∈ ℝ)
109		1red 10055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℝ)
110		absmul 14034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (abs‘(𝐴 · 𝑥)) = ((abs‘𝐴) · (abs‘𝑥)))
111	47, 110	syldan 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) = ((abs‘𝐴) · (abs‘𝑥)))
112	34	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ∈ ℝ)
113	112, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ)
114	47	absge0d 14183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ≤ (abs‘𝑥))
115	112	lep1d 10955	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1))
116	112, 113, 107, 114, 115	lemul1ad 10963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) · (abs‘𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥)))
117	111, 116	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥)))
118		0cn 10032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℂ
119	98	cnmetdval 22574	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0)))
120	47, 118, 119	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0)))
121	47	subid1d 10381	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 − 0) = 𝑥)
122	121	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝑥 − 0)) = (abs‘𝑥))
123	120, 122	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘𝑥))
124		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
125	124, 30	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))))
126	31	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs ∘ − ) ∈ (∞Met‘ℂ))
127	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 / ((abs‘𝐴) + 1)) ∈ ℝ^*)
128		0cnd 10033	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ∈ ℂ)
129		elbl3 22197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (1 / ((abs‘𝐴) + 1)) ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ↔ (𝑥(abs ∘ − )0) < (1 / ((abs‘𝐴) + 1))))
130	126, 127, 128, 47, 129	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ↔ (𝑥(abs ∘ − )0) < (1 / ((abs‘𝐴) + 1))))
131	125, 130	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) < (1 / ((abs‘𝐴) + 1)))
132	123, 131	eqbrtrrd 4677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) < (1 / ((abs‘𝐴) + 1)))
133	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 < ((abs‘𝐴) + 1))
134		ltmuldiv2 10897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ (((abs‘𝐴) + 1) ∈ ℝ ∧ 0 < ((abs‘𝐴) + 1))) → ((((abs‘𝐴) + 1) · (abs‘𝑥)) < 1 ↔ (abs‘𝑥) < (1 / ((abs‘𝐴) + 1))))
135	107, 109, 113, 133, 134	syl112anc 1330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((((abs‘𝐴) + 1) · (abs‘𝑥)) < 1 ↔ (abs‘𝑥) < (1 / ((abs‘𝐴) + 1))))
136	132, 135	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) < 1)
137	105, 108, 109, 117, 136	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) < 1)
138	104, 137	eqbrtrd 4675	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) < 1)
139		1rp 11836	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ⁺
140		rpxr 11840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
141	139, 140	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℝ^*)
142		1cnd 10056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
143		elbl3 22197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (1 ∈ ℂ ∧ (1 + (𝐴 · 𝑥)) ∈ ℂ)) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 + (𝐴 · 𝑥))(abs ∘ − )1) < 1))
144	126, 141, 142, 91, 143	syl22anc 1327	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ − ))1) ↔ ((1 + (𝐴 · 𝑥))(abs ∘ − )1) < 1))
145	138, 144	mpbird 247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ − ))1))
146	97, 145	sseldi 3601	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (ℂ ∖ {0}))
147		eldifsni 4320	. . . . . . . . . . . . . . . 16 ⊢ ((1 + (𝐴 · 𝑥)) ∈ (ℂ ∖ {0}) → (1 + (𝐴 · 𝑥)) ≠ 0)
148	146, 147	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ≠ 0)
149	148	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ≠ 0)
150	47	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ∈ ℂ)
151	150, 85	reccld 10794	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ ℂ)
152	92, 149, 151	cxpefd 24458	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)) = (exp‘((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥))))))
153	91, 148	logcld 24317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ)
154	153	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ)
155	151, 154	mulcomd 10061	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥)))
156		simpll 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ∈ ℂ)
157		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ≠ 0)
158	156, 157	dividd 10799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 / 𝐴) = 1)
159	158	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (1 / 𝑥))
160	156, 156, 150, 157, 85	divdiv1d 10832	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (𝐴 / (𝐴 · 𝑥)))
161	159, 160	eqtr3d 2658	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) = (𝐴 / (𝐴 · 𝑥)))
162	161	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥)) = ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥))))
163	89	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ∈ ℂ)
164	82	biimpa 501	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ≠ 0)
165	154, 156, 163, 164	div12d 10837	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))
166	155, 162, 165	3eqtrd 2660	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))
167	166	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (exp‘((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
168	87, 152, 167	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
169	168	ex 450	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
170	84, 169	sylbird 250	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (¬ (𝐴 · 𝑥) = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
171	170	imp 445	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
172	28, 29, 80, 171	ifbothda 4123	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
173	172	mpteq2dva 4744	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))))
174	46	resmptd 5452	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))))
175		1cnd 10056	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → 1 ∈ ℂ)
176	153	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ)
177	89	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ∈ ℂ)
178		simpr 477	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ¬ (𝐴 · 𝑥) = 0)
179	178	neqned 2801	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ≠ 0)
180	176, 177, 179	divcld 10801	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) ∈ ℂ)
181	175, 180	ifclda 4120	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) ∈ ℂ)
182		eqidd 2623	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
183		eqidd 2623	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))))
184		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (𝐴 · 𝑦) = (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
185	184	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
186		oveq2 6658	. . . . . . . . . . 11 ⊢ (if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · 1))
187	186	fveq2d 6195	. . . . . . . . . 10 ⊢ (if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · 1)))
188		oveq2 6658	. . . . . . . . . . 11 ⊢ (if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))
189	188	fveq2d 6195	. . . . . . . . . 10 ⊢ (if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
190	187, 189	ifsb 4099	. . . . . . . . 9 ⊢ (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
191	185, 190	syl6eq 2672	. . . . . . . 8 ⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
192	181, 182, 183, 191	fmptco 6396	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))))
193	173, 174, 192	3eqtr4d 2666	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ 𝑆) = ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))
194		eqidd 2623	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))))
195		eqidd 2623	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) = (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))))
196		eqeq1 2626	. . . . . . . . . . 11 ⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 = 1 ↔ (1 + (𝐴 · 𝑥)) = 1))
197		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (log‘𝑦) = (log‘(1 + (𝐴 · 𝑥))))
198		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 − 1) = ((1 + (𝐴 · 𝑥)) − 1))
199	197, 198	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → ((log‘𝑦) / (𝑦 − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))
200	196, 199	ifbieq2d 4111	. . . . . . . . . 10 ⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1))) = if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))))
201	145, 194, 195, 200	fmptco 6396	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))))
202	63	eqeq2i 2634	. . . . . . . . . . . 12 ⊢ ((1 + (𝐴 · 𝑥)) = (1 + 0) ↔ (1 + (𝐴 · 𝑥)) = 1)
203	142, 89, 128	addcand 10239	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = (1 + 0) ↔ (𝐴 · 𝑥) = 0))
204	202, 203	syl5bbr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = 1 ↔ (𝐴 · 𝑥) = 0))
205	102	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))
206	204, 205	ifbieq2d 4111	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))) = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))
207	206	mpteq2dva 4744	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
208	201, 207	eqtrd 2656	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))
209		eqid 2622	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
210		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
211	210	cnfldtopon 22586	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
212	211	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
213		1cnd 10056	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℂ)
214	212, 212, 213	cnmptc 21465	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 1) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
215		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
216	212, 212, 215	cnmptc 21465	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝐴) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
217	212	cnmptid 21464	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝑥) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
218	210	mulcn 22670	. . . . . . . . . . . . . . 15 ⊢ · ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
219	218	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → · ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
220	212, 216, 217, 219	cnmpt12f 21469	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
221	210	addcn 22668	. . . . . . . . . . . . . 14 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
222	221	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
223	212, 214, 220, 222	cnmpt12f 21469	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (1 + (𝐴 · 𝑥))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
224	209, 212, 46, 223	cnmpt1res 21479	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld)))
225		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))
226	145, 225	fmptd 6385	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))):𝑆⟶(1(ball‘(abs ∘ − ))1))
227		frn 6053	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))):𝑆⟶(1(ball‘(abs ∘ − ))1) → ran (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘ − ))1))
228	226, 227	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ran (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘ − ))1))
229		difss 3737	. . . . . . . . . . . . . 14 ⊢ (ℂ ∖ {0}) ⊆ ℂ
230	97, 229	sstri 3612	. . . . . . . . . . . . 13 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ ℂ
231	230	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (1(ball‘(abs ∘ − ))1) ⊆ ℂ)
232		cnrest2 21090	. . . . . . . . . . . 12 ⊢ (((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)))))
233	212, 228, 231, 232	syl3anc 1326	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld)) ↔ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn ((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)))))
234	224, 233	mpbid 222	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn ((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1))))
235		blcntr 22218	. . . . . . . . . . . . 13 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (1 / ((abs‘𝐴) + 1)) ∈ ℝ⁺) → 0 ∈ (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))))
236	32, 33, 42, 235	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 0 ∈ (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))))
237	236, 30	syl6eleqr 2712	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → 0 ∈ 𝑆)
238		resttopon 20965	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
239	211, 46, 238	sylancr 695	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
240		toponuni 20719	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
241	239, 240	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
242	237, 241	eleqtrd 2703	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 0 ∈ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
243		eqid 2622	. . . . . . . . . . 11 ⊢ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
244	243	cncnpi 21082	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝑆 ↦ (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))
245	234, 242, 244	syl2anc 693	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP ((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)))‘0))
246		cnelprrecn 10029	. . . . . . . . . . 11 ⊢ ℂ ∈ {ℝ, ℂ}
247		logf1o 24311	. . . . . . . . . . . . . 14 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
248		f1of 6137	. . . . . . . . . . . . . 14 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
249	247, 248	ax-mp 5	. . . . . . . . . . . . 13 ⊢ log:(ℂ ∖ {0})⟶ran log
250		logrncn 24309	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ran log → 𝑥 ∈ ℂ)
251	250	ssriv 3607	. . . . . . . . . . . . 13 ⊢ ran log ⊆ ℂ
252		fss 6056	. . . . . . . . . . . . 13 ⊢ ((log:(ℂ ∖ {0})⟶ran log ∧ ran log ⊆ ℂ) → log:(ℂ ∖ {0})⟶ℂ)
253	249, 251, 252	mp2an 708	. . . . . . . . . . . 12 ⊢ log:(ℂ ∖ {0})⟶ℂ
254		fssres 6070	. . . . . . . . . . . 12 ⊢ ((log:(ℂ ∖ {0})⟶ℂ ∧ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ℂ)
255	253, 97, 254	mp2an 708	. . . . . . . . . . 11 ⊢ (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ − ))1)⟶ℂ
256		blcntr 22218	. . . . . . . . . . . . . 14 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ⁺) → 1 ∈ (1(ball‘(abs ∘ − ))1))
257	31, 88, 139, 256	mp3an 1424	. . . . . . . . . . . . 13 ⊢ 1 ∈ (1(ball‘(abs ∘ − ))1)
258		ovex 6678	. . . . . . . . . . . . . 14 ⊢ (1 / 𝑦) ∈ V
259	93	dvlog2 24399	. . . . . . . . . . . . . 14 ⊢ (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦))
260	258, 259	dmmpti 6023	. . . . . . . . . . . . 13 ⊢ dom (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) = (1(ball‘(abs ∘ − ))1)
261	257, 260	eleqtrri 2700	. . . . . . . . . . . 12 ⊢ 1 ∈ dom (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1)))
262		eqid 2622	. . . . . . . . . . . . 13 ⊢ ((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)) = ((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1))
263	259	fveq1i 6192	. . . . . . . . . . . . . . . . 17 ⊢ ((ℂ D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1) = ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦))‘1)
264		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 1 → (1 / 𝑦) = (1 / 1))
265		1div1e1 10717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 1) = 1
266	264, 265	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 1 → (1 / 𝑦) = 1)
267		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦)) = (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦))
268		1ex 10035	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ V
269	266, 267, 268	fvmpt 6282	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ (1(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦))‘1) = 1)
270	257, 269	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ (1 / 𝑦))‘1) = 1
271	263, 270	eqtr2i 2645	. . . . . . . . . . . . . . . 16 ⊢ 1 = ((ℂ D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1)
272	271	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → 1 = ((ℂ D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1))
273		fvres 6207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑦) = (log‘𝑦))
274		fvres 6207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘1) = (log‘1))
275	257, 274	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘1) = (log‘1))
276		log1 24332	. . . . . . . . . . . . . . . . . . 19 ⊢ (log‘1) = 0
277	275, 276	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ − ))1))‘1) = 0)
278	273, 277	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → (((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs ∘ − ))1))‘1)) = ((log‘𝑦) − 0))
279	97	sseli 3599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → 𝑦 ∈ (ℂ ∖ {0}))
280		eldifsn 4317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (ℂ ∖ {0}) ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
281	279, 280	sylib 208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
282		logcl 24315	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (log‘𝑦) ∈ ℂ)
283	281, 282	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑦) ∈ ℂ)
284	283	subid1d 10381	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → ((log‘𝑦) − 0) = (log‘𝑦))
285	278, 284	eqtr2d 2657	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → (log‘𝑦) = (((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs ∘ − ))1))‘1)))
286	285	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) → ((log‘𝑦) / (𝑦 − 1)) = ((((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs ∘ − ))1))‘1)) / (𝑦 − 1)))
287	272, 286	ifeq12d 4106	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (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))))
288	287	mpteq2ia 4740	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (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))))
289	262, 210, 288	dvcnp 23682	. . . . . . . . . . . 12 ⊢ (((ℂ ∈ {ℝ, ℂ} ∧ (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))
290	261, 289	mpan2 707	. . . . . . . . . . 11 ⊢ ((ℂ ∈ {ℝ, ℂ} ∧ (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))
291	246, 255, 230, 290	mp3an 1424	. . . . . . . . . 10 ⊢ (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)) CnP (TopOpen‘ℂ_fld))‘1)
292		oveq2 6658	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (𝐴 · 𝑥) = (𝐴 · 0))
293	292	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (1 + (𝐴 · 𝑥)) = (1 + (𝐴 · 0)))
294		ovex 6678	. . . . . . . . . . . . . 14 ⊢ (1 + (𝐴 · 0)) ∈ V
295	293, 225, 294	fvmpt 6282	. . . . . . . . . . . . 13 ⊢ (0 ∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0)))
296	237, 295	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0)))
297		mul01 10215	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
298	297	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (1 + (𝐴 · 0)) = (1 + 0))
299	298, 63	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (1 + (𝐴 · 0)) = 1)
300	296, 299	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = 1)
301	300	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)) CnP (TopOpen‘ℂ_fld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0)) = ((((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)) CnP (TopOpen‘ℂ_fld))‘1))
302	291, 301	syl5eleqr 2708	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (1(ball‘(abs ∘ − ))1)) CnP (TopOpen‘ℂ_fld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0)))
303		cnpco 21071	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝑆 ↦ (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))
304	245, 302, 303	syl2anc 693	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘0))
305	208, 304	eqeltrrd 2702	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘0))
306	212, 212, 215	cnmptc 21465	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝐴) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
307	212	cnmptid 21464	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
308	212, 306, 307, 219	cnmpt12f 21469	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
309		efcn 24197	. . . . . . . . . . 11 ⊢ exp ∈ (ℂ–cn→ℂ)
310	210	cncfcn1 22713	. . . . . . . . . . 11 ⊢ (ℂ–cn→ℂ) = ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld))
311	309, 310	eleqtri 2699	. . . . . . . . . 10 ⊢ exp ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld))
312	311	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → exp ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
313	212, 308, 312	cnmpt11f 21467	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
314		eqid 2622	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))
315	181, 314	fmptd 6385	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))):𝑆⟶ℂ)
316	315, 237	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0) ∈ ℂ)
317	211	toponunii 20721	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
318	317	cncnpi 21082	. . . . . . . 8 ⊢ (((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)) ∧ ((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0) ∈ ℂ) → (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∈ (((TopOpen‘ℂ_fld) CnP (TopOpen‘ℂ_fld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0)))
319	313, 316, 318	syl2anc 693	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∈ (((TopOpen‘ℂ_fld) CnP (TopOpen‘ℂ_fld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0)))
320		cnpco 21071	. . . . . . 7 ⊢ (((𝑥 ∈ 𝑆 ↦ 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))
321	305, 319, 320	syl2anc 693	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘0))
322	193, 321	eqeltrd 2701	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ 𝑆) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘0))
323	210	cnfldtop 22587	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) ∈ Top
324	323	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (TopOpen‘ℂ_fld) ∈ Top)
325	210	cnfldtopn 22585	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
326	325	blopn 22305	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (1 / ((abs‘𝐴) + 1)) ∈ ℝ^*) → (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ∈ (TopOpen‘ℂ_fld))
327	32, 33, 43, 326	syl3anc 1326	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ∈ (TopOpen‘ℂ_fld))
328	30, 327	syl5eqel 2705	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → 𝑆 ∈ (TopOpen‘ℂ_fld))
329		isopn3i 20886	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝑆 ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘𝑆) = 𝑆)
330	323, 328, 329	sylancr 695	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((int‘(TopOpen‘ℂ_fld))‘𝑆) = 𝑆)
331	237, 330	eleqtrrd 2704	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 0 ∈ ((int‘(TopOpen‘ℂ_fld))‘𝑆))
332		efcl 14813	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
333	332	ad2antrr 762	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑥 = 0) → (exp‘𝐴) ∈ ℂ)
334	88, 14, 90	sylancr 695	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) ∈ ℂ)
335	334, 53	cxpcld 24454	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)) ∈ ℂ)
336	333, 335	ifclda 4120	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))) ∈ ℂ)
337		eqid 2622	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) = (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥))))
338	336, 337	fmptd 6385	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))):ℂ⟶ℂ)
339	317, 317	cnprest 21093	. . . . . 6 ⊢ ((((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)))
340	324, 46, 331, 338, 339	syl22anc 1327	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ∈ (((TopOpen‘ℂ_fld) CnP (TopOpen‘ℂ_fld))‘0) ↔ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ 𝑆) ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘0)))
341	322, 340	mpbird 247	. . . 4 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ∈ (((TopOpen‘ℂ_fld) CnP (TopOpen‘ℂ_fld))‘0))
342	317	cnpresti 21092	. . . 4 ⊢ (((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))
343	25, 27, 341, 342	syl3anc 1326	. . 3 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑_𝑐(1 / 𝑥)))) ↾ (0[,)+∞)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) CnP (TopOpen‘ℂ_fld))‘0))
344	24, 343	eqeltrd 2701	. 2 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) CnP (TopOpen‘ℂ_fld))‘0))
345		simpl 473	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → 𝐴 ∈ ℂ)
346		rpcn 11841	. . . . . . 7 ⊢ (𝑘 ∈ ℝ⁺ → 𝑘 ∈ ℂ)
347	346	adantl 482	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → 𝑘 ∈ ℂ)
348		rpne0 11848	. . . . . . 7 ⊢ (𝑘 ∈ ℝ⁺ → 𝑘 ≠ 0)
349	348	adantl 482	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → 𝑘 ≠ 0)
350	345, 347, 349	divcld 10801	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → (𝐴 / 𝑘) ∈ ℂ)
351		addcl 10018	. . . . 5 ⊢ ((1 ∈ ℂ ∧ (𝐴 / 𝑘) ∈ ℂ) → (1 + (𝐴 / 𝑘)) ∈ ℂ)
352	88, 350, 351	sylancr 695	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → (1 + (𝐴 / 𝑘)) ∈ ℂ)
353	352, 347	cxpcld 24454	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ⁺) → ((1 + (𝐴 / 𝑘))↑_𝑐𝑘) ∈ ℂ)
354		oveq2 6658	. . . . 5 ⊢ (𝑘 = (1 / 𝑥) → (𝐴 / 𝑘) = (𝐴 / (1 / 𝑥)))
355	354	oveq2d 6666	. . . 4 ⊢ (𝑘 = (1 / 𝑥) → (1 + (𝐴 / 𝑘)) = (1 + (𝐴 / (1 / 𝑥))))
356		id 22	. . . 4 ⊢ (𝑘 = (1 / 𝑥) → 𝑘 = (1 / 𝑥))
357	355, 356	oveq12d 6668	. . 3 ⊢ (𝑘 = (1 / 𝑥) → ((1 + (𝐴 / 𝑘))↑_𝑐𝑘) = ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)))
358		eqid 2622	. . 3 ⊢ ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) = ((TopOpen‘ℂ_fld) ↾_t (0[,)+∞))
359	332, 353, 357, 210, 358	rlimcnp3 24694	. 2 ⊢ (𝐴 ∈ ℂ → ((𝑘 ∈ ℝ⁺ ↦ ((1 + (𝐴 / 𝑘))↑_𝑐𝑘)) ⇝_𝑟 (exp‘𝐴) ↔ (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑_𝑐(1 / 𝑥)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (0[,)+∞)) CnP (TopOpen‘ℂ_fld))‘0)))
360	344, 359	mpbird 247	1 ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ⁺ ↦ ((1 + (𝐴 / 𝑘))↑_𝑐𝑘)) ⇝_𝑟 (exp‘𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∖ cdif 3571 ⊆ wss 3574 ifcif 4086 {csn 4177 {cpr 4179 ∪ cuni 4436 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ran crn 5115 ↾ cres 5116 ∘ ccom 5118 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 -∞cmnf 10072 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℝ⁺crp 11832 (,]cioc 12176 [,)cico 12177 abscabs 13974 ⇝_𝑟 crli 14216 expce 14792 ↾_t crest 16081 TopOpenctopn 16082 ∞Metcxmt 19731 ballcbl 19733 ℂ_fldccnfld 19746 Topctop 20698 TopOnctopon 20715 intcnt 20821 Cn ccn 21028 CnP ccnp 21029 ×_t ctx 21363 –cn→ccncf 22679 D cdv 23627 logclog 24301 ↑_𝑐ccxp 24302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-tan 14802 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304

This theorem is referenced by: dfef2 24697

W3C validator