MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dveflem Structured version   Visualization version   GIF version

Theorem dveflem 23723
Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 14820, to show that abs(exp(𝑥) − 1 − 𝑥) ≤ abs(𝑥)↑2 · (3 / 4). (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
Assertion
Ref Expression
dveflem 0(ℂ D exp)1

Proof of Theorem dveflem
Dummy variables 𝑘 𝑛 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 10017 . . 3 0 ∈ ℂ
2 eqid 2620 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
32cnfldtop 22568 . . . 4 (TopOpen‘ℂfld) ∈ Top
42cnfldtopon 22567 . . . . . 6 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
54toponunii 20702 . . . . 5 ℂ = (TopOpen‘ℂfld)
65ntrtop 20855 . . . 4 ((TopOpen‘ℂfld) ∈ Top → ((int‘(TopOpen‘ℂfld))‘ℂ) = ℂ)
73, 6ax-mp 5 . . 3 ((int‘(TopOpen‘ℂfld))‘ℂ) = ℂ
81, 7eleqtrri 2698 . 2 0 ∈ ((int‘(TopOpen‘ℂfld))‘ℂ)
9 ax-1cn 9979 . . 3 1 ∈ ℂ
10 1rp 11821 . . . . . 6 1 ∈ ℝ+
11 ifcl 4121 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ 1 ∈ ℝ+) → if(𝑥 ≤ 1, 𝑥, 1) ∈ ℝ+)
1210, 11mpan2 706 . . . . 5 (𝑥 ∈ ℝ+ → if(𝑥 ≤ 1, 𝑥, 1) ∈ ℝ+)
13 eldifsn 4308 . . . . . . 7 (𝑤 ∈ (ℂ ∖ {0}) ↔ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
14 simprl 793 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → 𝑤 ∈ ℂ)
1514subid1d 10366 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → (𝑤 − 0) = 𝑤)
1615fveq2d 6182 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → (abs‘(𝑤 − 0)) = (abs‘𝑤))
1716breq1d 4654 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → ((abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1) ↔ (abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1)))
1814abscld 14156 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → (abs‘𝑤) ∈ ℝ)
19 rpre 11824 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
2019adantr 481 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → 𝑥 ∈ ℝ)
21 1red 10040 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → 1 ∈ ℝ)
22 ltmin 12010 . . . . . . . . . . 11 (((abs‘𝑤) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)))
2318, 20, 21, 22syl3anc 1324 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → ((abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)))
2417, 23bitrd 268 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → ((abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)))
25 simplr 791 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
2625, 13sylibr 224 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈ (ℂ ∖ {0}))
27 fveq2 6178 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (exp‘𝑧) = (exp‘𝑤))
2827oveq1d 6650 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((exp‘𝑧) − 1) = ((exp‘𝑤) − 1))
29 id 22 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤𝑧 = 𝑤)
3028, 29oveq12d 6653 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (((exp‘𝑧) − 1) / 𝑧) = (((exp‘𝑤) − 1) / 𝑤))
31 eqid 2620 . . . . . . . . . . . . . . 15 (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))
32 ovex 6663 . . . . . . . . . . . . . . 15 (((exp‘𝑤) − 1) / 𝑤) ∈ V
3330, 31, 32fvmpt 6269 . . . . . . . . . . . . . 14 (𝑤 ∈ (ℂ ∖ {0}) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤))
3426, 33syl 17 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤))
3534oveq1d 6650 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1) = ((((exp‘𝑤) − 1) / 𝑤) − 1))
3635fveq2d 6182 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) = (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)))
37 simplrl 799 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈ ℂ)
38 efcl 14794 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → (exp‘𝑤) ∈ ℂ)
3937, 38syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (exp‘𝑤) ∈ ℂ)
40 1cnd 10041 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 1 ∈ ℂ)
4139, 40subcld 10377 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((exp‘𝑤) − 1) ∈ ℂ)
42 simplrr 800 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ≠ 0)
4341, 37, 42divcld 10786 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (((exp‘𝑤) − 1) / 𝑤) ∈ ℂ)
4443, 40subcld 10377 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((((exp‘𝑤) − 1) / 𝑤) − 1) ∈ ℂ)
4544abscld 14156 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ∈ ℝ)
4637abscld 14156 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘𝑤) ∈ ℝ)
47 simpll 789 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈ ℝ+)
4847rpred 11857 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈ ℝ)
49 abscl 13999 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℂ → (abs‘𝑤) ∈ ℝ)
5049ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘𝑤) ∈ ℝ)
5138ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (exp‘𝑤) ∈ ℂ)
52 subcl 10265 . . . . . . . . . . . . . . . . . . . . 21 (((exp‘𝑤) ∈ ℂ ∧ 1 ∈ ℂ) → ((exp‘𝑤) − 1) ∈ ℂ)
5351, 9, 52sylancl 693 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((exp‘𝑤) − 1) ∈ ℂ)
54 simpll 789 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ∈ ℂ)
55 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ≠ 0)
5653, 54, 55divcld 10786 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((exp‘𝑤) − 1) / 𝑤) ∈ ℂ)
57 1cnd 10041 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈ ℂ)
5856, 57subcld 10377 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((((exp‘𝑤) − 1) / 𝑤) − 1) ∈ ℂ)
5958abscld 14156 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ∈ ℝ)
6050, 59remulcld 10055 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ∈ ℝ)
6150resqcld 13018 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤)↑2) ∈ ℝ)
62 3re 11079 . . . . . . . . . . . . . . . . . 18 3 ∈ ℝ
63 4nn 11172 . . . . . . . . . . . . . . . . . 18 4 ∈ ℕ
64 nndivre 11041 . . . . . . . . . . . . . . . . . 18 ((3 ∈ ℝ ∧ 4 ∈ ℕ) → (3 / 4) ∈ ℝ)
6562, 63, 64mp2an 707 . . . . . . . . . . . . . . . . 17 (3 / 4) ∈ ℝ
66 remulcl 10006 . . . . . . . . . . . . . . . . 17 ((((abs‘𝑤)↑2) ∈ ℝ ∧ (3 / 4) ∈ ℝ) → (((abs‘𝑤)↑2) · (3 / 4)) ∈ ℝ)
6761, 65, 66sylancl 693 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((abs‘𝑤)↑2) · (3 / 4)) ∈ ℝ)
6853, 54subcld 10377 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((exp‘𝑤) − 1) − 𝑤) ∈ ℂ)
6968, 54, 55divcan2d 10788 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (((exp‘𝑤) − 1) − 𝑤))
7053, 54, 54, 55divsubdird 10825 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((((exp‘𝑤) − 1) − 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − (𝑤 / 𝑤)))
7154, 55dividd 10784 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 𝑤) = 1)
7271oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((((exp‘𝑤) − 1) / 𝑤) − (𝑤 / 𝑤)) = ((((exp‘𝑤) − 1) / 𝑤) − 1))
7370, 72eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((((exp‘𝑤) − 1) − 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − 1))
7473oveq2d 6651 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1)))
7551, 57, 54subsub4d 10408 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((exp‘𝑤) − 1) − 𝑤) = ((exp‘𝑤) − (1 + 𝑤)))
76 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))
77 df-2 11064 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 = (1 + 1)
78 1nn0 11293 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℕ0
79 1e0p1 11537 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 = (0 + 1)
80 0nn0 11292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℕ0
81 0cnd 10018 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ∈ ℂ)
8276efval2 14795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ ℂ → (exp‘𝑤) = Σ𝑘 ∈ ℕ0 ((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘))
8382ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (exp‘𝑤) = Σ𝑘 ∈ ℕ0 ((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘))
84 nn0uz 11707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 = (ℤ‘0)
8584sumeq1i 14409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Σ𝑘 ∈ ℕ0 ((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘) = Σ𝑘 ∈ (ℤ‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)
8683, 85syl6req 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈ (ℤ‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘) = (exp‘𝑤))
8786oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + Σ𝑘 ∈ (ℤ‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)) = (0 + (exp‘𝑤)))
8851addid2d 10222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + (exp‘𝑤)) = (exp‘𝑤))
8987, 88eqtr2d 2655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (exp‘𝑤) = (0 + Σ𝑘 ∈ (ℤ‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)))
90 eft0val 14823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ ℂ → ((𝑤↑0) / (!‘0)) = 1)
9190ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑0) / (!‘0)) = 1)
9291oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) = (0 + 1))
9392, 79syl6eqr 2672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) = 1)
9476, 79, 80, 54, 81, 89, 93efsep 14821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (exp‘𝑤) = (1 + Σ𝑘 ∈ (ℤ‘1)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)))
95 exp1 12849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ ℂ → (𝑤↑1) = 𝑤)
9695ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤↑1) = 𝑤)
9796oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 / (!‘1)))
98 fac1 13047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (!‘1) = 1
9998oveq2i 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 / (!‘1)) = (𝑤 / 1)
10097, 99syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 / 1))
101 div1 10701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ ℂ → (𝑤 / 1) = 𝑤)
102101ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 1) = 𝑤)
103100, 102eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = 𝑤)
104103oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + ((𝑤↑1) / (!‘1))) = (1 + 𝑤))
10576, 77, 78, 54, 57, 94, 104efsep 14821 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (exp‘𝑤) = ((1 + 𝑤) + Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)))
106105eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((1 + 𝑤) + Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤))
107 addcl 10003 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (1 + 𝑤) ∈ ℂ)
1089, 54, 107sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + 𝑤) ∈ ℂ)
109 2nn0 11294 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ0
11076eftlcl 14818 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑤 ∈ ℂ ∧ 2 ∈ ℕ0) → Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ)
11154, 109, 110sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ)
11251, 108, 111subaddd 10395 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((exp‘𝑤) − (1 + 𝑤)) = Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘) ↔ ((1 + 𝑤) + Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤)))
113106, 112mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((exp‘𝑤) − (1 + 𝑤)) = Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘))
11475, 113eqtrd 2654 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((exp‘𝑤) − 1) − 𝑤) = Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘))
11569, 74, 1143eqtr3d 2662 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1)) = Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘))
116115fveq2d 6182 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘(𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1))) = (abs‘Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)))
11754, 58absmuld 14174 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘(𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1))) = ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))))
118116, 117eqtr3d 2656 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)) = ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))))
119 eqid 2620 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 ↦ (((abs‘𝑤)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((abs‘𝑤)↑𝑛) / (!‘𝑛)))
120 eqid 2620 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 ↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 + 1))↑𝑛))) = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 + 1))↑𝑛)))
121 2nn 11170 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℕ
122121a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 2 ∈ ℕ)
123 1red 10040 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈ ℝ)
124 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘𝑤) < 1)
12550, 123, 124ltled 10170 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘𝑤) ≤ 1)
12676, 119, 120, 122, 54, 125eftlub 14820 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘Σ𝑘 ∈ (ℤ‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤𝑛) / (!‘𝑛)))‘𝑘)) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2) · 2))))
127118, 126eqbrtrrd 4668 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2) · 2))))
128 df-3 11065 . . . . . . . . . . . . . . . . . . 19 3 = (2 + 1)
129 fac2 13049 . . . . . . . . . . . . . . . . . . . . 21 (!‘2) = 2
130129oveq1i 6645 . . . . . . . . . . . . . . . . . . . 20 ((!‘2) · 2) = (2 · 2)
131 2t2e4 11162 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
132130, 131eqtr2i 2643 . . . . . . . . . . . . . . . . . . 19 4 = ((!‘2) · 2)
133128, 132oveq12i 6647 . . . . . . . . . . . . . . . . . 18 (3 / 4) = ((2 + 1) / ((!‘2) · 2))
134133oveq2i 6646 . . . . . . . . . . . . . . . . 17 (((abs‘𝑤)↑2) · (3 / 4)) = (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2) · 2)))
135127, 134syl6breqr 4686 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ≤ (((abs‘𝑤)↑2) · (3 / 4)))
13665a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ∈ ℝ)
13750sqge0d 13019 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ≤ ((abs‘𝑤)↑2))
138 1re 10024 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ
139 3lt4 11182 . . . . . . . . . . . . . . . . . . . . . 22 3 < 4
140 4cn 11083 . . . . . . . . . . . . . . . . . . . . . . 23 4 ∈ ℂ
141140mulid1i 10027 . . . . . . . . . . . . . . . . . . . . . 22 (4 · 1) = 4
142139, 141breqtrri 4671 . . . . . . . . . . . . . . . . . . . . 21 3 < (4 · 1)
143 4re 11082 . . . . . . . . . . . . . . . . . . . . . . 23 4 ∈ ℝ
144 4pos 11101 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 4
145143, 144pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℝ ∧ 0 < 4)
146 ltdivmul 10883 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℝ ∧ 1 ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → ((3 / 4) < 1 ↔ 3 < (4 · 1)))
14762, 138, 145, 146mp3an 1422 . . . . . . . . . . . . . . . . . . . . 21 ((3 / 4) < 1 ↔ 3 < (4 · 1))
148142, 147mpbir 221 . . . . . . . . . . . . . . . . . . . 20 (3 / 4) < 1
14965, 138, 148ltleii 10145 . . . . . . . . . . . . . . . . . . 19 (3 / 4) ≤ 1
150149a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ≤ 1)
151136, 123, 61, 137, 150lemul2ad 10949 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((abs‘𝑤)↑2) · (3 / 4)) ≤ (((abs‘𝑤)↑2) · 1))
15250recnd 10053 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘𝑤) ∈ ℂ)
153152sqcld 12989 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤)↑2) ∈ ℂ)
154153mulid1d 10042 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((abs‘𝑤)↑2) · 1) = ((abs‘𝑤)↑2))
155151, 154breqtrd 4670 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (((abs‘𝑤)↑2) · (3 / 4)) ≤ ((abs‘𝑤)↑2))
15660, 67, 61, 135, 155letrd 10179 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ≤ ((abs‘𝑤)↑2))
157152sqvald 12988 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤)↑2) = ((abs‘𝑤) · (abs‘𝑤)))
158156, 157breqtrd 4670 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ≤ ((abs‘𝑤) · (abs‘𝑤)))
159 absgt0 14045 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ℂ → (𝑤 ≠ 0 ↔ 0 < (abs‘𝑤)))
160159ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 ≠ 0 ↔ 0 < (abs‘𝑤)))
16155, 160mpbid 222 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 < (abs‘𝑤))
16250, 161elrpd 11854 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘𝑤) ∈ ℝ+)
16359, 50, 162lemul2d 11901 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤) ↔ ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1))) ≤ ((abs‘𝑤) · (abs‘𝑤))))
164158, 163mpbird 247 . . . . . . . . . . . . 13 (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤))
165164ad2ant2l 781 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤))
166 simprl 793 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘𝑤) < 𝑥)
16745, 46, 48, 165, 166lelttrd 10180 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) < 𝑥)
16836, 167eqbrtrd 4666 . . . . . . . . . 10 (((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) ∧ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)
169168ex 450 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → (((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
17024, 169sylbid 230 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → ((abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
171170adantld 483 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) → ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
17213, 171sylan2b 492 . . . . . 6 ((𝑥 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})) → ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
173172ralrimiva 2963 . . . . 5 (𝑥 ∈ ℝ+ → ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
174 breq2 4648 . . . . . . . . 9 (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → ((abs‘(𝑤 − 0)) < 𝑦 ↔ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)))
175174anbi2d 739 . . . . . . . 8 (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) ↔ (𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1))))
176175imbi1d 331 . . . . . . 7 (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → (((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) ↔ ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))
177176ralbidv 2983 . . . . . 6 (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → (∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) ↔ ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))
178177rspcev 3304 . . . . 5 ((if(𝑥 ≤ 1, 𝑥, 1) ∈ ℝ+ ∧ ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
17912, 173, 178syl2anc 692 . . . 4 (𝑥 ∈ ℝ+ → ∃𝑦 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))
180179rgen 2919 . . 3 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)
181 eldifi 3724 . . . . . . . . . 10 (𝑧 ∈ (ℂ ∖ {0}) → 𝑧 ∈ ℂ)
182 efcl 14794 . . . . . . . . . 10 (𝑧 ∈ ℂ → (exp‘𝑧) ∈ ℂ)
183181, 182syl 17 . . . . . . . . 9 (𝑧 ∈ (ℂ ∖ {0}) → (exp‘𝑧) ∈ ℂ)
184 1cnd 10041 . . . . . . . . 9 (𝑧 ∈ (ℂ ∖ {0}) → 1 ∈ ℂ)
185183, 184subcld 10377 . . . . . . . 8 (𝑧 ∈ (ℂ ∖ {0}) → ((exp‘𝑧) − 1) ∈ ℂ)
186 eldifsni 4311 . . . . . . . 8 (𝑧 ∈ (ℂ ∖ {0}) → 𝑧 ≠ 0)
187185, 181, 186divcld 10786 . . . . . . 7 (𝑧 ∈ (ℂ ∖ {0}) → (((exp‘𝑧) − 1) / 𝑧) ∈ ℂ)
18831, 187fmpti 6369 . . . . . 6 (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)):(ℂ ∖ {0})⟶ℂ
189188a1i 11 . . . . 5 (⊤ → (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)):(ℂ ∖ {0})⟶ℂ)
190 difssd 3730 . . . . 5 (⊤ → (ℂ ∖ {0}) ⊆ ℂ)
191 0cnd 10018 . . . . 5 (⊤ → 0 ∈ ℂ)
192189, 190, 191ellimc3 23624 . . . 4 (⊤ → (1 ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) lim 0) ↔ (1 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))))
193192trud 1491 . . 3 (1 ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) lim 0) ↔ (1 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))
1949, 180, 193mpbir2an 954 . 2 1 ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) lim 0)
1955restid 16075 . . . . . 6 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
1963, 195ax-mp 5 . . . . 5 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
197196eqcomi 2629 . . . 4 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
198181subid1d 10366 . . . . . . 7 (𝑧 ∈ (ℂ ∖ {0}) → (𝑧 − 0) = 𝑧)
199198oveq2d 6651 . . . . . 6 (𝑧 ∈ (ℂ ∖ {0}) → (((exp‘𝑧) − (exp‘0)) / (𝑧 − 0)) = (((exp‘𝑧) − (exp‘0)) / 𝑧))
200 ef0 14802 . . . . . . . 8 (exp‘0) = 1
201200oveq2i 6646 . . . . . . 7 ((exp‘𝑧) − (exp‘0)) = ((exp‘𝑧) − 1)
202201oveq1i 6645 . . . . . 6 (((exp‘𝑧) − (exp‘0)) / 𝑧) = (((exp‘𝑧) − 1) / 𝑧)
203199, 202syl6req 2671 . . . . 5 (𝑧 ∈ (ℂ ∖ {0}) → (((exp‘𝑧) − 1) / 𝑧) = (((exp‘𝑧) − (exp‘0)) / (𝑧 − 0)))
204203mpteq2ia 4731 . . . 4 (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − (exp‘0)) / (𝑧 − 0)))
205 ssid 3616 . . . . 5 ℂ ⊆ ℂ
206205a1i 11 . . . 4 (⊤ → ℂ ⊆ ℂ)
207 eff 14793 . . . . 5 exp:ℂ⟶ℂ
208207a1i 11 . . . 4 (⊤ → exp:ℂ⟶ℂ)
209197, 2, 204, 206, 208, 206eldv 23643 . . 3 (⊤ → (0(ℂ D exp)1 ↔ (0 ∈ ((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1 ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) lim 0))))
210209trud 1491 . 2 (0(ℂ D exp)1 ↔ (0 ∈ ((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1 ∈ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) lim 0)))
2118, 194, 210mpbir2an 954 1 0(ℂ D exp)1
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wtru 1482  wcel 1988  wne 2791  wral 2909  wrex 2910  cdif 3564  wss 3567  ifcif 4077  {csn 4168   class class class wbr 4644  cmpt 4720  wf 5872  cfv 5876  (class class class)co 6635  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  cn 11005  2c2 11055  3c3 11056  4c4 11057  0cn0 11277  cuz 11672  +crp 11817  cexp 12843  !cfa 13043  abscabs 13955  Σcsu 14397  expce 14773  t crest 16062  TopOpenctopn 16063  fldccnfld 19727  Topctop 20679  intcnt 20802   lim climc 23607   D cdv 23608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ico 12166  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-fac 13044  df-hash 13101  df-shft 13788  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-limsup 14183  df-clim 14200  df-rlim 14201  df-sum 14398  df-ef 14779  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-plusg 15935  df-mulr 15936  df-starv 15937  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-rest 16064  df-topn 16065  df-topgen 16085  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-ntr 20805  df-cnp 21013  df-xms 22106  df-ms 22107  df-limc 23611  df-dv 23612
This theorem is referenced by:  dvef  23724
  Copyright terms: Public domain W3C validator