Metamath Proof Explorer

Theorem 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 ∈ ℕ0
77 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
78 77 eftlcl ⊢ ( ( 𝑤 ∈ ℂ ∧ 2 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
79 52 76 78 sylancl ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℂ )
80 df-2 ⊢ 2 = ( 1 + 1 )
81 1nn0 ⊢ 1 ∈ ℕ0
82 1e0p1 ⊢ 1 = ( 0 + 1 )
83 0nn0 ⊢ 0 ∈ ℕ0
84 0cnd ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → 0 ∈ ℂ )
85 77 efval2 ⊢ ( 𝑤 ∈ ℂ → ( exp ‘ 𝑤 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
86 85 ad2antrr ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( exp ‘ 𝑤 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
87 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
88 87 sumeq1i ⊢ Σ 𝑘 ∈ ℕ0 ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 )
89 86 88 eqtr2di ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( exp ‘ 𝑤 ) )
90 89 oveq2d ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( 0 + Σ 𝑘 ∈ ( ℤ≥ ‘ 0 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( 0 + ( exp ‘ 𝑤 ) ) )
91 49 addlidd ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( 0 + ( exp ‘ 𝑤 ) ) = ( exp ‘ 𝑤 ) )
92 90 91 eqtr2d ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( exp ‘ 𝑤 ) = ( 0 + Σ 𝑘 ∈ ( ℤ≥ ‘ 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 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
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 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
109 75 79 108 mvrladdd ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( ( exp ‘ 𝑤 ) − ( 1 + 𝑤 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
110 73 109 eqtrd ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( ( ( exp ‘ 𝑤 ) − 1 ) − 𝑤 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
111 67 72 110 3eqtr3d ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( 𝑤 · ( ( ( ( exp ‘ 𝑤 ) − 1 ) / 𝑤 ) − 1 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
112 111 fveq2d ⊢ ( ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ∧ ( abs ‘ 𝑤 ) < 1 ) → ( abs ‘ ( 𝑤 · ( ( ( ( exp ‘ 𝑤 ) − 1 ) / 𝑤 ) − 1 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) )
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 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) = ( ( abs ‘ 𝑤 ) · ( abs ‘ ( ( ( ( exp ‘ 𝑤 ) − 1 ) / 𝑤 ) − 1 ) ) ) )
115 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝑤 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝑤 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
116 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝑤 ) ↑ 2 ) / ( ! ‘ 2 ) ) · ( ( 1 / ( 2 + 1 ) ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( 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 ) ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑤 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) ) ≤ ( ( ( 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