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 ( ℂ D exp ) 1

Proof

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

Metamath Proof Explorer

Theorem dveflem

Proof