efrlim

Description: The limit of the sequence ( 1 + A / k ) ^ k is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 ). (Contributed by Mario Carneiro, 1-Mar-2015) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

		Ref	Expression
	Hypothesis	efrlim.1	$⊢ S = 0 ball (abs \circ -) (\frac{1}{\|A\| + 1})$
	Assertion	efrlim	$⊢ A \in ℂ \to (k \in ℝ^{+} ⟼ {(1 + (\frac{A}{k}))}^{k}) \underset{ℝ}{⇝} e^{A}$

Proof

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

Metamath Proof Explorer

Theorem efrlim

Proof