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	$⊢ 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	47	biimpa	$⊢ ((A \in ℂ \land x \in S) \land A x = 0) \to (A = 0 \lor x = 0)$
49	8 12	reccld	$⊢ ((A \in ℂ \land x \in ℂ) \land \neg x = 0) \to \frac{1}{x} \in ℂ$
50	45 49	syldanl	$⊢ ((A \in ℂ \land x \in S) \land \neg x = 0) \to \frac{1}{x} \in ℂ$
51	50	adantlr	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to \frac{1}{x} \in ℂ$
52	51	1cxpd	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to 1^{\frac{1}{x}} = 1$
53		simplr	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to A = 0$
54	53	oveq1d	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to A x = 0 \cdot x$
55	45	ad2antrr	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to x \in ℂ$
56	55	mul02d	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to 0 \cdot x = 0$
57	54 56	eqtrd	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to A x = 0$
58	57	oveq2d	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to 1 + A x = 1 + 0$
59		1p0e1	$⊢ 1 + 0 = 1$
60	58 59	eqtrdi	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to 1 + A x = 1$
61	60	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}}$
62	53	fveq2d	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to e^{A} = e^{0}$
63		ef0	$⊢ e^{0} = 1$
64	62 63	eqtrdi	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to e^{A} = 1$
65	52 61 64	3eqtr4d	$⊢ (((A \in ℂ \land x \in S) \land A = 0) \land \neg x = 0) \to {(1 + A x)}^{\frac{1}{x}} = e^{A}$
66	65	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})$
67		ifid	$⊢ if (x = 0, e^{A}, e^{A}) = e^{A}$
68	66 67	eqtrdi	$⊢ ((A \in ℂ \land x \in S) \land A = 0) \to if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}}) = e^{A}$
69		iftrue	$⊢ x = 0 \to if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}}) = e^{A}$
70	69	adantl	$⊢ ((A \in ℂ \land x \in S) \land x = 0) \to if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}}) = e^{A}$
71	68 70	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}$
72		mulid1	$⊢ A \in ℂ \to A \cdot 1 = A$
73	72	ad2antrr	$⊢ ((A \in ℂ \land x \in S) \land (A = 0 \lor x = 0)) \to A \cdot 1 = A$
74	73	fveq2d	$⊢ ((A \in ℂ \land x \in S) \land (A = 0 \lor x = 0)) \to e^{A \cdot 1} = e^{A}$
75	71 74	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}$
76	48 75	syldan	$⊢ ((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}$
77		mulne0b	$⊢ (A \in ℂ \land x \in ℂ) \to ((A \neq 0 \land x \neq 0) \leftrightarrow A x \neq 0)$
78	45 77	syldan	$⊢ (A \in ℂ \land x \in S) \to ((A \neq 0 \land x \neq 0) \leftrightarrow A x \neq 0)$
79		df-ne	$⊢ A x \neq 0 \leftrightarrow \neg A x = 0$
80	78 79	bitrdi	$⊢ (A \in ℂ \land x \in S) \to ((A \neq 0 \land x \neq 0) \leftrightarrow \neg A x = 0)$
81		simprr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to x \neq 0$
82	81	neneqd	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \neg x = 0$
83	82	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}}$
84		ax-1cn	$⊢ 1 \in ℂ$
85	45 14	syldan	$⊢ (A \in ℂ \land x \in S) \to A x \in ℂ$
86		addcl	$⊢ (1 \in ℂ \land A x \in ℂ) \to 1 + A x \in ℂ$
87	84 85 86	sylancr	$⊢ (A \in ℂ \land x \in S) \to 1 + A x \in ℂ$
88	87	adantr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to 1 + A x \in ℂ$
89		eqid	$⊢ 1 ball (abs \circ -) 1 = 1 ball (abs \circ -) 1$
90	89	dvlog2lem	$⊢ 1 ball (abs \circ -) 1 \subseteq ℂ ∖ (−∞, 0]$
91		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
92	91	logdmss	$⊢ ℂ ∖ (−∞, 0] \subseteq ℂ ∖ \{0\}$
93	90 92	sstri	$⊢ 1 ball (abs \circ -) 1 \subseteq ℂ ∖ \{0\}$
94		eqid	$⊢ abs \circ - = abs \circ -$
95	94	cnmetdval	$⊢ (1 + A x \in ℂ \land 1 \in ℂ) \to (1 + A x) (abs \circ -) 1 = \|1 + A x - 1\|$
96	87 84 95	sylancl	$⊢ (A \in ℂ \land x \in S) \to (1 + A x) (abs \circ -) 1 = \|1 + A x - 1\|$
97		pncan2	$⊢ (1 \in ℂ \land A x \in ℂ) \to 1 + A x - 1 = A x$
98	84 85 97	sylancr	$⊢ (A \in ℂ \land x \in S) \to 1 + A x - 1 = A x$
99	98	fveq2d	$⊢ (A \in ℂ \land x \in S) \to \|1 + A x - 1\| = \|A x\|$
100	96 99	eqtrd	$⊢ (A \in ℂ \land x \in S) \to (1 + A x) (abs \circ -) 1 = \|A x\|$
101	85	abscld	$⊢ (A \in ℂ \land x \in S) \to \|A x\| \in ℝ$
102	34	adantr	$⊢ (A \in ℂ \land x \in S) \to \|A\| + 1 \in ℝ$
103	45	abscld	$⊢ (A \in ℂ \land x \in S) \to \|x\| \in ℝ$
104	102 103	remulcld	$⊢ (A \in ℂ \land x \in S) \to (\|A\| + 1) \|x\| \in ℝ$
105		1red	$⊢ (A \in ℂ \land x \in S) \to 1 \in ℝ$
106		absmul	$⊢ (A \in ℂ \land x \in ℂ) \to \|A x\| = \|A\| \|x\|$
107	45 106	syldan	$⊢ (A \in ℂ \land x \in S) \to \|A x\| = \|A\| \|x\|$
108	32	adantr	$⊢ (A \in ℂ \land x \in S) \to \|A\| \in ℝ$
109	108 33	syl	$⊢ (A \in ℂ \land x \in S) \to \|A\| + 1 \in ℝ$
110	45	absge0d	$⊢ (A \in ℂ \land x \in S) \to 0 \leq \|x\|$
111	108	lep1d	$⊢ (A \in ℂ \land x \in S) \to \|A\| \leq \|A\| + 1$
112	108 109 103 110 111	lemul1ad	$⊢ (A \in ℂ \land x \in S) \to \|A\| \|x\| \leq (\|A\| + 1) \|x\|$
113	107 112	eqbrtrd	$⊢ (A \in ℂ \land x \in S) \to \|A x\| \leq (\|A\| + 1) \|x\|$
114		0cn	$⊢ 0 \in ℂ$
115	94	cnmetdval	$⊢ (x \in ℂ \land 0 \in ℂ) \to x (abs \circ -) 0 = \|x - 0\|$
116	45 114 115	sylancl	$⊢ (A \in ℂ \land x \in S) \to x (abs \circ -) 0 = \|x - 0\|$
117	45	subid1d	$⊢ (A \in ℂ \land x \in S) \to x - 0 = x$
118	117	fveq2d	$⊢ (A \in ℂ \land x \in S) \to \|x - 0\| = \|x\|$
119	116 118	eqtrd	$⊢ (A \in ℂ \land x \in S) \to x (abs \circ -) 0 = \|x\|$
120		simpr	$⊢ (A \in ℂ \land x \in S) \to x \in S$
121	120 1	eleqtrdi	$⊢ (A \in ℂ \land x \in S) \to x \in (0 ball (abs \circ -) (\frac{1}{\|A\| + 1}))$
122	30	a1i	$⊢ (A \in ℂ \land x \in S) \to abs \circ - \in ∞Met (ℂ)$
123	41	adantr	$⊢ (A \in ℂ \land x \in S) \to \frac{1}{\|A\| + 1} \in ℝ^{*}$
124		0cnd	$⊢ (A \in ℂ \land x \in S) \to 0 \in ℂ$
125		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})$
126	122 123 124 45 125	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})$
127	121 126	mpbid	$⊢ (A \in ℂ \land x \in S) \to x (abs \circ -) 0 < \frac{1}{\|A\| + 1}$
128	119 127	eqbrtrrd	$⊢ (A \in ℂ \land x \in S) \to \|x\| < \frac{1}{\|A\| + 1}$
129	38	adantr	$⊢ (A \in ℂ \land x \in S) \to 0 < \|A\| + 1$
130		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})$
131	103 105 109 129 130	syl112anc	$⊢ (A \in ℂ \land x \in S) \to ((\|A\| + 1) \|x\| < 1 \leftrightarrow \|x\| < \frac{1}{\|A\| + 1})$
132	128 131	mpbird	$⊢ (A \in ℂ \land x \in S) \to (\|A\| + 1) \|x\| < 1$
133	101 104 105 113 132	lelttrd	$⊢ (A \in ℂ \land x \in S) \to \|A x\| < 1$
134	100 133	eqbrtrd	$⊢ (A \in ℂ \land x \in S) \to (1 + A x) (abs \circ -) 1 < 1$
135		1rp	$⊢ 1 \in ℝ^{+}$
136		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
137	135 136	mp1i	$⊢ (A \in ℂ \land x \in S) \to 1 \in ℝ^{*}$
138		1cnd	$⊢ (A \in ℂ \land x \in S) \to 1 \in ℂ$
139		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)$
140	122 137 138 87 139	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)$
141	134 140	mpbird	$⊢ (A \in ℂ \land x \in S) \to 1 + A x \in (1 ball (abs \circ -) 1)$
142	93 141	sseldi	$⊢ (A \in ℂ \land x \in S) \to 1 + A x \in (ℂ ∖ \{0\})$
143		eldifsni	$⊢ 1 + A x \in (ℂ ∖ \{0\}) \to 1 + A x \neq 0$
144	142 143	syl	$⊢ (A \in ℂ \land x \in S) \to 1 + A x \neq 0$
145	144	adantr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to 1 + A x \neq 0$
146	45	adantr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to x \in ℂ$
147	146 81	reccld	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \frac{1}{x} \in ℂ$
148	88 145 147	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)}$
149	87 144	logcld	$⊢ (A \in ℂ \land x \in S) \to \log (1 + A x) \in ℂ$
150	149	adantr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \log (1 + A x) \in ℂ$
151	147 150	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})$
152		simpll	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to A \in ℂ$
153		simprl	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to A \neq 0$
154	152 153	dividd	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \frac{A}{A} = 1$
155	154	oveq1d	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \frac{\frac{A}{A}}{x} = \frac{1}{x}$
156	152 152 146 153 81	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}$
157	155 156	eqtr3d	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to \frac{1}{x} = \frac{A}{A x}$
158	157	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})$
159	85	adantr	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to A x \in ℂ$
160	78	biimpa	$⊢ ((A \in ℂ \land x \in S) \land (A \neq 0 \land x \neq 0)) \to A x \neq 0$
161	150 152 159 160	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})$
162	151 158 161	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})$
163	162	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})}$
164	83 148 163	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})}$
165	164	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})})$
166	80 165	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})})$
167	166	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})}$
168	28 29 76 167	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})})$
169	168	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})}))$
170	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}}))$
171		1cnd	$⊢ ((A \in ℂ \land x \in S) \land A x = 0) \to 1 \in ℂ$
172	149	adantr	$⊢ ((A \in ℂ \land x \in S) \land \neg A x = 0) \to \log (1 + A x) \in ℂ$
173	85	adantr	$⊢ ((A \in ℂ \land x \in S) \land \neg A x = 0) \to A x \in ℂ$
174		simpr	$⊢ ((A \in ℂ \land x \in S) \land \neg A x = 0) \to \neg A x = 0$
175	174	neqned	$⊢ ((A \in ℂ \land x \in S) \land \neg A x = 0) \to A x \neq 0$
176	172 173 175	divcld	$⊢ ((A \in ℂ \land x \in S) \land \neg A x = 0) \to \frac{\log (1 + A x)}{A x} \in ℂ$
177	171 176	ifclda	$⊢ (A \in ℂ \land x \in S) \to if (A x = 0, 1, \frac{\log (1 + A x)}{A x}) \in ℂ$
178		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}))$
179		eqidd	$⊢ A \in ℂ \to (y \in ℂ ⟼ e^{A y}) = (y \in ℂ ⟼ e^{A y})$
180		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})$
181	180	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})}$
182		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$
183	182	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}$
184		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})$
185	184	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})}$
186	183 185	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})})$
187	181 186	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})})$
188	177 178 179 187	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})}))$
189	169 170 188	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}))$
190		eqidd	$⊢ A \in ℂ \to (x \in S ⟼ 1 + A x) = (x \in S ⟼ 1 + A x)$
191		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}))$
192		eqeq1	$⊢ y = 1 + A x \to (y = 1 \leftrightarrow 1 + A x = 1)$
193		fveq2	$⊢ y = 1 + A x \to \log y = \log (1 + A x)$
194		oveq1	$⊢ y = 1 + A x \to y - 1 = 1 + A x - 1$
195	193 194	oveq12d	$⊢ y = 1 + A x \to \frac{\log y}{y - 1} = \frac{\log (1 + A x)}{1 + A x - 1}$
196	192 195	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})$
197	141 190 191 196	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}))$
198	59	eqeq2i	$⊢ 1 + A x = 1 + 0 \leftrightarrow 1 + A x = 1$
199	138 85 124	addcand	$⊢ (A \in ℂ \land x \in S) \to (1 + A x = 1 + 0 \leftrightarrow A x = 0)$
200	198 199	bitr3id	$⊢ (A \in ℂ \land x \in S) \to (1 + A x = 1 \leftrightarrow A x = 0)$
201	98	oveq2d	$⊢ (A \in ℂ \land x \in S) \to \frac{\log (1 + A x)}{1 + A x - 1} = \frac{\log (1 + A x)}{A x}$
202	200 201	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})$
203	202	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}))$
204	197 203	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}))$
205		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
206		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
207	206	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
208	207	a1i	$⊢ A \in ℂ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
209		1cnd	$⊢ A \in ℂ \to 1 \in ℂ$
210	208 208 209	cnmptc	$⊢ A \in ℂ \to (x \in ℂ ⟼ 1) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
211		id	$⊢ A \in ℂ \to A \in ℂ$
212	208 208 211	cnmptc	$⊢ A \in ℂ \to (x \in ℂ ⟼ A) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
213	208	cnmptid	$⊢ A \in ℂ \to (x \in ℂ ⟼ x) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
214	206	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
215	214	a1i	$⊢ A \in ℂ \to \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
216	208 212 213 215	cnmpt12f	$⊢ A \in ℂ \to (x \in ℂ ⟼ A x) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
217	206	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	208 210 216 218	cnmpt12f	$⊢ A \in ℂ \to (x \in ℂ ⟼ 1 + A x) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
220	205 208 44 219	cnmpt1res	$⊢ A \in ℂ \to (x \in S ⟼ 1 + A x) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn TopOpen (ℂ_{fld}))$
221	141	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	93 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	207 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	207 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 93 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 84 135 250	mp3an	$⊢ 1 \in (1 ball (abs \circ -) 1)$
252		ovex	$⊢ \frac{1}{y} \in V$
253	89	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	93	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 206 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 59	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	204 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	208 208 211	cnmptc	$⊢ A \in ℂ \to (y \in ℂ ⟼ A) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
302	208	cnmptid	$⊢ A \in ℂ \to (y \in ℂ ⟼ y) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
303	208 301 302 215	cnmpt12f	$⊢ A \in ℂ \to (y \in ℂ ⟼ A y) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
304		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
305	206	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})$
306	304 305	eleqtri	$⊢ \exp \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
307	306	a1i	$⊢ A \in ℂ \to \exp \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
308	208 303 307	cnmpt11f	$⊢ A \in ℂ \to (y \in ℂ ⟼ e^{A y}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
309	177	fmpttd	$⊢ A \in ℂ \to (x \in S ⟼ if (A x = 0, 1, \frac{\log (1 + A x)}{A x})) : S ⟶ ℂ$
310	309 231	ffvelrnd	$⊢ A \in ℂ \to (x \in S ⟼ if (A x = 0, 1, \frac{\log (1 + A x)}{A x})) (0) \in ℂ$
311		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
312	311	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))$
313	308 310 312	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))$
314		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)$
315	300 313 314	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)$
316	189 315	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)$
317	206	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
318	317	a1i	$⊢ A \in ℂ \to TopOpen (ℂ_{fld}) \in Top$
319	206	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
320	319	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})$
321	30 31 41 320	mp3an2i	$⊢ A \in ℂ \to 0 ball (abs \circ -) (\frac{1}{\|A\| + 1}) \in TopOpen (ℂ_{fld})$
322	1 321	eqeltrid	$⊢ A \in ℂ \to S \in TopOpen (ℂ_{fld})$
323		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (S) = S$
324	317 322 323	sylancr	$⊢ A \in ℂ \to int (TopOpen (ℂ_{fld})) (S) = S$
325	231 324	eleqtrrd	$⊢ A \in ℂ \to 0 \in int (TopOpen (ℂ_{fld})) (S)$
326		efcl	$⊢ A \in ℂ \to e^{A} \in ℂ$
327	326	ad2antrr	$⊢ ((A \in ℂ \land x \in ℂ) \land x = 0) \to e^{A} \in ℂ$
328	84 15 86	sylancr	$⊢ ((A \in ℂ \land x \in ℂ) \land \neg x = 0) \to 1 + A x \in ℂ$
329	328 49	cxpcld	$⊢ ((A \in ℂ \land x \in ℂ) \land \neg x = 0) \to {(1 + A x)}^{\frac{1}{x}} \in ℂ$
330	327 329	ifclda	$⊢ (A \in ℂ \land x \in ℂ) \to if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}}) \in ℂ$
331	330	fmpttd	$⊢ A \in ℂ \to (x \in ℂ ⟼ if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}})) : ℂ ⟶ ℂ$
332	311 311	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))$
333	318 44 325 331 332	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))$
334	316 333	mpbird	$⊢ A \in ℂ \to (x \in ℂ ⟼ if (x = 0, e^{A}, {(1 + A x)}^{\frac{1}{x}})) \in (TopOpen (ℂ_{fld}) CnP TopOpen (ℂ_{fld})) (0)$
335	311	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)$
336	4 27 334 335	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)$
337	25 336	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)$
338		simpl	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to A \in ℂ$
339		rpcn	$⊢ k \in ℝ^{+} \to k \in ℂ$
340	339	adantl	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to k \in ℂ$
341		rpne0	$⊢ k \in ℝ^{+} \to k \neq 0$
342	341	adantl	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to k \neq 0$
343	338 340 342	divcld	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to \frac{A}{k} \in ℂ$
344		addcl	$⊢ (1 \in ℂ \land \frac{A}{k} \in ℂ) \to 1 + (\frac{A}{k}) \in ℂ$
345	84 343 344	sylancr	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to 1 + (\frac{A}{k}) \in ℂ$
346	345 340	cxpcld	$⊢ (A \in ℂ \land k \in ℝ^{+}) \to {(1 + (\frac{A}{k}))}^{k} \in ℂ$
347		oveq2	$⊢ k = \frac{1}{x} \to \frac{A}{k} = \frac{A}{\frac{1}{x}}$
348	347	oveq2d	$⊢ k = \frac{1}{x} \to 1 + (\frac{A}{k}) = 1 + (\frac{A}{\frac{1}{x}})$
349		id	$⊢ k = \frac{1}{x} \to k = \frac{1}{x}$
350	348 349	oveq12d	$⊢ k = \frac{1}{x} \to {(1 + (\frac{A}{k}))}^{k} = {(1 + (\frac{A}{\frac{1}{x}}))}^{\frac{1}{x}}$
351		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)$
352	326 346 350 206 351	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))$
353	337 352	mpbird	$⊢ A \in ℂ \to (k \in ℝ^{+} ⟼ {(1 + (\frac{A}{k}))}^{k}) \underset{ℝ}{⇝} e^{A}$

Metamath Proof Explorer

Theorem efrlim

Proof