dveflem

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub , to show that abs ( exp ( x ) - 1 - x ) <_ abs ( x ) ^ 2 x. ( 3 / 4 ) . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

		Ref	Expression
	Assertion	dveflem	$⊢ 0 \exp_{ℂ}^{'} 1$

Proof

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
3	2	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
4		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
5	4	ntrtop	$⊢ TopOpen (ℂ_{fld}) \in Top \to int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
6	3 5	ax-mp	$⊢ int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
7	1 6	eleqtrri	$⊢ 0 \in int (TopOpen (ℂ_{fld})) (ℂ)$
8		ax-1cn	$⊢ 1 \in ℂ$
9		1rp	$⊢ 1 \in ℝ^{+}$
10		ifcl	$⊢ (x \in ℝ^{+} \land 1 \in ℝ^{+}) \to if (x \leq 1, x, 1) \in ℝ^{+}$
11	9 10	mpan2	$⊢ x \in ℝ^{+} \to if (x \leq 1, x, 1) \in ℝ^{+}$
12		eldifsn	$⊢ w \in (ℂ ∖ \{0\}) \leftrightarrow (w \in ℂ \land w \neq 0)$
13		simprl	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to w \in ℂ$
14	13	subid1d	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to w - 0 = w$
15	14	fveq2d	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to \|w - 0\| = \|w\|$
16	15	breq1d	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to (\|w - 0\| < if (x \leq 1, x, 1) \leftrightarrow \|w\| < if (x \leq 1, x, 1))$
17	13	abscld	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to \|w\| \in ℝ$
18		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
19	18	adantr	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to x \in ℝ$
20		1red	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to 1 \in ℝ$
21		ltmin	$⊢ (\|w\| \in ℝ \land x \in ℝ \land 1 \in ℝ) \to (\|w\| < if (x \leq 1, x, 1) \leftrightarrow (\|w\| < x \land \|w\| < 1))$
22	17 19 20 21	syl3anc	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to (\|w\| < if (x \leq 1, x, 1) \leftrightarrow (\|w\| < x \land \|w\| < 1))$
23	16 22	bitrd	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to (\|w - 0\| < if (x \leq 1, x, 1) \leftrightarrow (\|w\| < x \land \|w\| < 1))$
24		simplr	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to (w \in ℂ \land w \neq 0)$
25	24 12	sylibr	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to w \in (ℂ ∖ \{0\})$
26		fveq2	$⊢ z = w \to e^{z} = e^{w}$
27	26	oveq1d	$⊢ z = w \to e^{z} - 1 = e^{w} - 1$
28		id	$⊢ z = w \to z = w$
29	27 28	oveq12d	$⊢ z = w \to \frac{e^{z} - 1}{z} = \frac{e^{w} - 1}{w}$
30		eqid	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) = (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z})$
31		ovex	$⊢ \frac{e^{w} - 1}{w} \in V$
32	29 30 31	fvmpt	$⊢ w \in (ℂ ∖ \{0\}) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) = \frac{e^{w} - 1}{w}$
33	25 32	syl	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) = \frac{e^{w} - 1}{w}$
34	33	fvoveq1d	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| = \|(\frac{e^{w} - 1}{w}) - 1\|$
35		simplrl	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to w \in ℂ$
36		efcl	$⊢ w \in ℂ \to e^{w} \in ℂ$
37	35 36	syl	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to e^{w} \in ℂ$
38		1cnd	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to 1 \in ℂ$
39	37 38	subcld	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to e^{w} - 1 \in ℂ$
40		simplrr	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to w \neq 0$
41	39 35 40	divcld	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \frac{e^{w} - 1}{w} \in ℂ$
42	41 38	subcld	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to (\frac{e^{w} - 1}{w}) - 1 \in ℂ$
43	42	abscld	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|(\frac{e^{w} - 1}{w}) - 1\| \in ℝ$
44	35	abscld	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|w\| \in ℝ$
45		simpll	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to x \in ℝ^{+}$
46	45	rpred	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to x \in ℝ$
47		abscl	$⊢ w \in ℂ \to \|w\| \in ℝ$
48	47	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \in ℝ$
49	36	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} \in ℂ$
50		subcl	$⊢ (e^{w} \in ℂ \land 1 \in ℂ) \to e^{w} - 1 \in ℂ$
51	49 8 50	sylancl	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} - 1 \in ℂ$
52		simpll	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w \in ℂ$
53		simplr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w \neq 0$
54	51 52 53	divcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{e^{w} - 1}{w} \in ℂ$
55		1cnd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 1 \in ℂ$
56	54 55	subcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to (\frac{e^{w} - 1}{w}) - 1 \in ℂ$
57	56	abscld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|(\frac{e^{w} - 1}{w}) - 1\| \in ℝ$
58	48 57	remulcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \in ℝ$
59	48	resqcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} \in ℝ$
60		3re	$⊢ 3 \in ℝ$
61		4nn	$⊢ 4 \in ℕ$
62		nndivre	$⊢ (3 \in ℝ \land 4 \in ℕ) \to \frac{3}{4} \in ℝ$
63	60 61 62	mp2an	$⊢ \frac{3}{4} \in ℝ$
64		remulcl	$⊢ ({\|w\|}^{2} \in ℝ \land \frac{3}{4} \in ℝ) \to {\|w\|}^{2} (\frac{3}{4}) \in ℝ$
65	59 63 64	sylancl	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} (\frac{3}{4}) \in ℝ$
66	51 52	subcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} - 1 - w \in ℂ$
67	66 52 53	divcan2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w (\frac{e^{w} - 1 - w}{w}) = e^{w} - 1 - w$
68	51 52 52 53	divsubdird	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{e^{w} - 1 - w}{w} = (\frac{e^{w} - 1}{w}) - (\frac{w}{w})$
69	52 53	dividd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w}{w} = 1$
70	69	oveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to (\frac{e^{w} - 1}{w}) - (\frac{w}{w}) = (\frac{e^{w} - 1}{w}) - 1$
71	68 70	eqtrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{e^{w} - 1 - w}{w} = (\frac{e^{w} - 1}{w}) - 1$
72	71	oveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w (\frac{e^{w} - 1 - w}{w}) = w ((\frac{e^{w} - 1}{w}) - 1)$
73	49 55 52	subsub4d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} - 1 - w = e^{w} - (1 + w)$
74		addcl	$⊢ (1 \in ℂ \land w \in ℂ) \to 1 + w \in ℂ$
75	8 52 74	sylancr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 1 + w \in ℂ$
76		2nn0	$⊢ 2 \in ℕ_{0}$
77		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!})$
78	77	eftlcl	$⊢ (w \in ℂ \land 2 \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k) \in ℂ$
79	52 76 78	sylancl	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k) \in ℂ$
80		df-2	$⊢ 2 = 1 + 1$
81		1nn0	$⊢ 1 \in ℕ_{0}$
82		1e0p1	$⊢ 1 = 0 + 1$
83		0nn0	$⊢ 0 \in ℕ_{0}$
84		0cnd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 \in ℂ$
85	77	efval2	$⊢ w \in ℂ \to e^{w} = \sum_{k \in ℕ_{0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
86	85	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} = \sum_{k \in ℕ_{0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
87		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
88	87	sumeq1i	$⊢ \sum_{k \in ℕ_{0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k) = \sum_{k \in ℤ_{\geq 0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
89	86 88	eqtr2di	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \sum_{k \in ℤ_{\geq 0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k) = e^{w}$
90	89	oveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 + \sum_{k \in ℤ_{\geq 0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k) = 0 + e^{w}$
91	49	addid2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 + e^{w} = e^{w}$
92	90 91	eqtr2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} = 0 + \sum_{k \in ℤ_{\geq 0}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
93		eft0val	$⊢ w \in ℂ \to \frac{w^{0}}{0!} = 1$
94	93	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w^{0}}{0!} = 1$
95	94	oveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 + (\frac{w^{0}}{0!}) = 0 + 1$
96	95 82	eqtr4di	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 + (\frac{w^{0}}{0!}) = 1$
97	77 82 83 52 84 92 96	efsep	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} = 1 + \sum_{k \in ℤ_{\geq 1}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
98		exp1	$⊢ w \in ℂ \to w^{1} = w$
99	98	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w^{1} = w$
100	99	oveq1d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w^{1}}{1!} = \frac{w}{1!}$
101		fac1	$⊢ 1! = 1$
102	101	oveq2i	$⊢ \frac{w}{1!} = \frac{w}{1}$
103	100 102	eqtrdi	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w^{1}}{1!} = \frac{w}{1}$
104		div1	$⊢ w \in ℂ \to \frac{w}{1} = w$
105	104	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w}{1} = w$
106	103 105	eqtrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{w^{1}}{1!} = w$
107	106	oveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 1 + (\frac{w^{1}}{1!}) = 1 + w$
108	77 80 81 52 55 97 107	efsep	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} = 1 + w + \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
109	75 79 108	mvrladdd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} - (1 + w) = \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
110	73 109	eqtrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to e^{w} - 1 - w = \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
111	67 72 110	3eqtr3d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to w ((\frac{e^{w} - 1}{w}) - 1) = \sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)$
112	111	fveq2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w ((\frac{e^{w} - 1}{w}) - 1)\| = \|\sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)\|$
113	52 56	absmuld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w ((\frac{e^{w} - 1}{w}) - 1)\| = \|w\| \|(\frac{e^{w} - 1}{w}) - 1\|$
114	112 113	eqtr3d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|\sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)\| = \|w\| \|(\frac{e^{w} - 1}{w}) - 1\|$
115		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{\|w\|}^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{{\|w\|}^{n}}{n!})$
116		eqid	$⊢ (n \in ℕ_{0} ⟼ (\frac{{\|w\|}^{2}}{2!}) {(\frac{1}{2 + 1})}^{n}) = (n \in ℕ_{0} ⟼ (\frac{{\|w\|}^{2}}{2!}) {(\frac{1}{2 + 1})}^{n})$
117		2nn	$⊢ 2 \in ℕ$
118	117	a1i	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 2 \in ℕ$
119		1red	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 1 \in ℝ$
120		simpr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| < 1$
121	48 119 120	ltled	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \leq 1$
122	77 115 116 118 52 121	eftlub	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|\sum_{k \in ℤ_{\geq 2}} (n \in ℕ_{0} ⟼ \frac{w^{n}}{n!}) (k)\| \leq {\|w\|}^{2} (\frac{2 + 1}{2! \cdot 2})$
123	114 122	eqbrtrrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \leq {\|w\|}^{2} (\frac{2 + 1}{2! \cdot 2})$
124		df-3	$⊢ 3 = 2 + 1$
125		fac2	$⊢ 2! = 2$
126	125	oveq1i	$⊢ 2! \cdot 2 = 2 \cdot 2$
127		2t2e4	$⊢ 2 \cdot 2 = 4$
128	126 127	eqtr2i	$⊢ 4 = 2! \cdot 2$
129	124 128	oveq12i	$⊢ \frac{3}{4} = \frac{2 + 1}{2! \cdot 2}$
130	129	oveq2i	$⊢ {\|w\|}^{2} (\frac{3}{4}) = {\|w\|}^{2} (\frac{2 + 1}{2! \cdot 2})$
131	123 130	breqtrrdi	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \leq {\|w\|}^{2} (\frac{3}{4})$
132	63	a1i	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{3}{4} \in ℝ$
133	48	sqge0d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 \leq {\|w\|}^{2}$
134		1re	$⊢ 1 \in ℝ$
135		3lt4	$⊢ 3 < 4$
136		4cn	$⊢ 4 \in ℂ$
137	136	mulid1i	$⊢ 4 \cdot 1 = 4$
138	135 137	breqtrri	$⊢ 3 < 4 \cdot 1$
139		4re	$⊢ 4 \in ℝ$
140		4pos	$⊢ 0 < 4$
141	139 140	pm3.2i	$⊢ (4 \in ℝ \land 0 < 4)$
142		ltdivmul	$⊢ (3 \in ℝ \land 1 \in ℝ \land (4 \in ℝ \land 0 < 4)) \to (\frac{3}{4} < 1 \leftrightarrow 3 < 4 \cdot 1)$
143	60 134 141 142	mp3an	$⊢ \frac{3}{4} < 1 \leftrightarrow 3 < 4 \cdot 1$
144	138 143	mpbir	$⊢ \frac{3}{4} < 1$
145	63 134 144	ltleii	$⊢ \frac{3}{4} \leq 1$
146	145	a1i	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \frac{3}{4} \leq 1$
147	132 119 59 133 146	lemul2ad	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} (\frac{3}{4}) \leq {\|w\|}^{2} \cdot 1$
148	48	recnd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \in ℂ$
149	148	sqcld	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} \in ℂ$
150	149	mulid1d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} \cdot 1 = {\|w\|}^{2}$
151	147 150	breqtrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} (\frac{3}{4}) \leq {\|w\|}^{2}$
152	58 65 59 131 151	letrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \leq {\|w\|}^{2}$
153	148	sqvald	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to {\|w\|}^{2} = \|w\| \|w\|$
154	152 153	breqtrd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \leq \|w\| \|w\|$
155		absgt0	$⊢ w \in ℂ \to (w \neq 0 \leftrightarrow 0 < \|w\|)$
156	155	ad2antrr	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to (w \neq 0 \leftrightarrow 0 < \|w\|)$
157	53 156	mpbid	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to 0 < \|w\|$
158	48 157	elrpd	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|w\| \in ℝ^{+}$
159	57 48 158	lemul2d	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to (\|(\frac{e^{w} - 1}{w}) - 1\| \leq \|w\| \leftrightarrow \|w\| \|(\frac{e^{w} - 1}{w}) - 1\| \leq \|w\| \|w\|)$
160	154 159	mpbird	$⊢ ((w \in ℂ \land w \neq 0) \land \|w\| < 1) \to \|(\frac{e^{w} - 1}{w}) - 1\| \leq \|w\|$
161	160	ad2ant2l	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|(\frac{e^{w} - 1}{w}) - 1\| \leq \|w\|$
162		simprl	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|w\| < x$
163	43 44 46 161 162	lelttrd	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|(\frac{e^{w} - 1}{w}) - 1\| < x$
164	34 163	eqbrtrd	$⊢ ((x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \land (\|w\| < x \land \|w\| < 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x$
165	164	ex	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to ((\|w\| < x \land \|w\| < 1) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
166	23 165	sylbid	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to (\|w - 0\| < if (x \leq 1, x, 1) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
167	166	adantld	$⊢ (x \in ℝ^{+} \land (w \in ℂ \land w \neq 0)) \to ((w \neq 0 \land \|w - 0\| < if (x \leq 1, x, 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
168	12 167	sylan2b	$⊢ (x \in ℝ^{+} \land w \in (ℂ ∖ \{0\})) \to ((w \neq 0 \land \|w - 0\| < if (x \leq 1, x, 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
169	168	ralrimiva	$⊢ x \in ℝ^{+} \to \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < if (x \leq 1, x, 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
170		brimralrspcev	$⊢ (if (x \leq 1, x, 1) \in ℝ^{+} \land \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < if (x \leq 1, x, 1)) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)) \to \exists y \in ℝ^{+} \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < y) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
171	11 169 170	syl2anc	$⊢ x \in ℝ^{+} \to \exists y \in ℝ^{+} \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < y) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
172	171	rgen	$⊢ \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < y) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)$
173		eldifi	$⊢ z \in (ℂ ∖ \{0\}) \to z \in ℂ$
174		efcl	$⊢ z \in ℂ \to e^{z} \in ℂ$
175	173 174	syl	$⊢ z \in (ℂ ∖ \{0\}) \to e^{z} \in ℂ$
176		1cnd	$⊢ z \in (ℂ ∖ \{0\}) \to 1 \in ℂ$
177	175 176	subcld	$⊢ z \in (ℂ ∖ \{0\}) \to e^{z} - 1 \in ℂ$
178		eldifsni	$⊢ z \in (ℂ ∖ \{0\}) \to z \neq 0$
179	177 173 178	divcld	$⊢ z \in (ℂ ∖ \{0\}) \to \frac{e^{z} - 1}{z} \in ℂ$
180	30 179	fmpti	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
181	180	a1i	$⊢ ⊤ \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
182		difssd	$⊢ ⊤ \to ℂ ∖ \{0\} \subseteq ℂ$
183		0cnd	$⊢ ⊤ \to 0 \in ℂ$
184	181 182 183	ellimc3	$⊢ ⊤ \to (1 \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) {lim}_{ℂ} 0) \leftrightarrow (1 \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < y) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x)))$
185	184	mptru	$⊢ 1 \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) {lim}_{ℂ} 0) \leftrightarrow (1 \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall w \in (ℂ ∖ \{0\}) ((w \neq 0 \land \|w - 0\| < y) \to \|(z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) (w) - 1\| < x))$
186	8 172 185	mpbir2an	$⊢ 1 \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) {lim}_{ℂ} 0)$
187	2	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
188	187	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
189	173	subid1d	$⊢ z \in (ℂ ∖ \{0\}) \to z - 0 = z$
190	189	oveq2d	$⊢ z \in (ℂ ∖ \{0\}) \to \frac{e^{z} - e^{0}}{z - 0} = \frac{e^{z} - e^{0}}{z}$
191		ef0	$⊢ e^{0} = 1$
192	191	oveq2i	$⊢ e^{z} - e^{0} = e^{z} - 1$
193	192	oveq1i	$⊢ \frac{e^{z} - e^{0}}{z} = \frac{e^{z} - 1}{z}$
194	190 193	eqtr2di	$⊢ z \in (ℂ ∖ \{0\}) \to \frac{e^{z} - 1}{z} = \frac{e^{z} - e^{0}}{z - 0}$
195	194	mpteq2ia	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) = (z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - e^{0}}{z - 0})$
196		ssidd	$⊢ ⊤ \to ℂ \subseteq ℂ$
197		eff	$⊢ \exp : ℂ ⟶ ℂ$
198	197	a1i	$⊢ ⊤ \to \exp : ℂ ⟶ ℂ$
199	188 2 195 196 198 196	eldv	$⊢ ⊤ \to (0 \exp_{ℂ}^{'} 1 \leftrightarrow (0 \in int (TopOpen (ℂ_{fld})) (ℂ) \land 1 \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) {lim}_{ℂ} 0)))$
200	199	mptru	$⊢ 0 \exp_{ℂ}^{'} 1 \leftrightarrow (0 \in int (TopOpen (ℂ_{fld})) (ℂ) \land 1 \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{e^{z} - 1}{z}) {lim}_{ℂ} 0))$
201	7 186 200	mpbir2an	$⊢ 0 \exp_{ℂ}^{'} 1$

Metamath Proof Explorer

Theorem dveflem

Proof