Step | Hyp | Ref
| Expression |
1 | | 0cn 10349 |
. . 3
⊢ 0 ∈
ℂ |
2 | | eqid 2826 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
3 | 2 | cnfldtop 22958 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈ Top |
4 | 2 | cnfldtopon 22957 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
5 | 4 | toponunii 21092 |
. . . . 5
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
6 | 5 | ntrtop 21246 |
. . . 4
⊢
((TopOpen‘ℂfld) ∈ Top →
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ) |
7 | 3, 6 | ax-mp 5 |
. . 3
⊢
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ |
8 | 1, 7 | eleqtrri 2906 |
. 2
⊢ 0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) |
9 | | ax-1cn 10311 |
. . 3
⊢ 1 ∈
ℂ |
10 | | 1rp 12117 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
11 | | ifcl 4351 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
12 | 10, 11 | mpan2 684 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
13 | | eldifsn 4537 |
. . . . . . 7
⊢ (𝑤 ∈ (ℂ ∖ {0})
↔ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
14 | | simprl 789 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑤 ∈
ℂ) |
15 | 14 | subid1d 10703 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(𝑤 − 0) = 𝑤) |
16 | 15 | fveq2d 6438 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘(𝑤 − 0)) =
(abs‘𝑤)) |
17 | 16 | breq1d 4884 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ (abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1))) |
18 | 14 | abscld 14553 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘𝑤) ∈
ℝ) |
19 | | rpre 12121 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
20 | 19 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑥 ∈
ℝ) |
21 | | 1red 10358 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) → 1
∈ ℝ) |
22 | | ltmin 12314 |
. . . . . . . . . . 11
⊢
(((abs‘𝑤)
∈ ℝ ∧ 𝑥
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
23 | 18, 20, 21, 22 | syl3anc 1496 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘𝑤) <
if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
24 | 17, 23 | bitrd 271 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
25 | | simplr 787 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) |
26 | 25, 13 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈ (ℂ ∖
{0})) |
27 | | fveq2 6434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (exp‘𝑧) = (exp‘𝑤)) |
28 | 27 | oveq1d 6921 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((exp‘𝑧) − 1) = ((exp‘𝑤) − 1)) |
29 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
30 | 28, 29 | oveq12d 6924 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (((exp‘𝑧) − 1) / 𝑧) = (((exp‘𝑤) − 1) / 𝑤)) |
31 | | eqid 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) |
32 | | ovex 6938 |
. . . . . . . . . . . . . 14
⊢
(((exp‘𝑤)
− 1) / 𝑤) ∈
V |
33 | 30, 31, 32 | fvmpt 6530 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
35 | 34 | fvoveq1d 6928 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) =
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) |
36 | | simplrl 797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈
ℂ) |
37 | | efcl 15186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) ∈
ℂ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(exp‘𝑤) ∈
ℂ) |
39 | | 1cnd 10352 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 1 ∈
ℂ) |
40 | 38, 39 | subcld 10714 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((exp‘𝑤) − 1)
∈ ℂ) |
41 | | simplrr 798 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ≠ 0) |
42 | 40, 36, 41 | divcld 11128 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
43 | 42, 39 | subcld 10714 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
44 | 43 | abscld 14553 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
45 | 36 | abscld 14553 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) ∈
ℝ) |
46 | | simpll 785 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ+) |
47 | 46 | rpred 12157 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ) |
48 | | abscl 14396 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ →
(abs‘𝑤) ∈
ℝ) |
49 | 48 | ad2antrr 719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ) |
50 | 37 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) ∈
ℂ) |
51 | | subcl 10601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((exp‘𝑤)
∈ ℂ ∧ 1 ∈ ℂ) → ((exp‘𝑤) − 1) ∈ ℂ) |
52 | 50, 9, 51 | sylancl 582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − 1)
∈ ℂ) |
53 | | simpll 785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ∈
ℂ) |
54 | | simplr 787 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ≠ 0) |
55 | 52, 53, 54 | divcld 11128 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
56 | | 1cnd 10352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℂ) |
57 | 55, 56 | subcld 10714 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
58 | 57 | abscld 14553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
59 | 49, 58 | remulcld 10388 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ∈ ℝ) |
60 | 49 | resqcld 13332 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℝ) |
61 | | 3re 11432 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
62 | | 4nn 11436 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
63 | | nndivre 11393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℝ ∧ 4 ∈ ℕ) → (3 / 4) ∈
ℝ) |
64 | 61, 62, 63 | mp2an 685 |
. . . . . . . . . . . . . . . . 17
⊢ (3 / 4)
∈ ℝ |
65 | | remulcl 10338 |
. . . . . . . . . . . . . . . . 17
⊢
((((abs‘𝑤)↑2) ∈ ℝ ∧ (3 / 4) ∈
ℝ) → (((abs‘𝑤)↑2) · (3 / 4)) ∈
ℝ) |
66 | 60, 64, 65 | sylancl 582 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ∈ ℝ) |
67 | 52, 53 | subcld 10714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) ∈
ℂ) |
68 | 67, 53, 54 | divcan2d 11130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (((exp‘𝑤) − 1) − 𝑤)) |
69 | 52, 53, 53, 54 | divsubdird 11167 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − (𝑤 / 𝑤))) |
70 | 53, 54 | dividd 11126 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 𝑤) = 1) |
71 | 70 | oveq2d 6922 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − (𝑤 / 𝑤)) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
72 | 69, 71 | eqtrd 2862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
73 | 72 | oveq2d 6922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1))) |
74 | 50, 56, 53 | subsub4d 10745 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) =
((exp‘𝑤) − (1 +
𝑤))) |
75 | | eqid 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ0
↦ ((𝑤↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛))) |
76 | | df-2 11415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 = (1 +
1) |
77 | | 1nn0 11637 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℕ0 |
78 | | 1e0p1 11865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 = (0 +
1) |
79 | | 0nn0 11636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
ℕ0 |
80 | | 0cnd 10350 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ∈
ℂ) |
81 | 75 | efval2 15187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
82 | 81 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
83 | | nn0uz 12005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
ℕ0 = (ℤ≥‘0) |
84 | 83 | sumeq1i 14806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) |
85 | 82, 84 | syl6req 2879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = (exp‘𝑤)) |
86 | 85 | oveq2d 6922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (0 + (exp‘𝑤))) |
87 | 50 | addid2d 10557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
(exp‘𝑤)) =
(exp‘𝑤)) |
88 | 86, 87 | eqtr2d 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
89 | | eft0val 15215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ ℂ → ((𝑤↑0) / (!‘0)) =
1) |
90 | 89 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑0) / (!‘0)) =
1) |
91 | 90 | oveq2d 6922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) = (0 +
1)) |
92 | 91, 78 | syl6eqr 2880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) =
1) |
93 | 75, 78, 79, 53, 80, 88, 92 | efsep 15213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (1 +
Σ𝑘 ∈
(ℤ≥‘1)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
94 | | exp1 13161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 ∈ ℂ → (𝑤↑1) = 𝑤) |
95 | 94 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤↑1) = 𝑤) |
96 | 95 | oveq1d 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 /
(!‘1))) |
97 | | fac1 13358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(!‘1) = 1 |
98 | 97 | oveq2i 6917 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 / (!‘1)) = (𝑤 / 1) |
99 | 96, 98 | syl6eq 2878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 / 1)) |
100 | | div1 11042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ ℂ → (𝑤 / 1) = 𝑤) |
101 | 100 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 1) = 𝑤) |
102 | 99, 101 | eqtrd 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = 𝑤) |
103 | 102 | oveq2d 6922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + ((𝑤↑1) / (!‘1))) = (1 +
𝑤)) |
104 | 75, 76, 77, 53, 56, 93, 103 | efsep 15213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
105 | 104 | eqcomd 2832 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤)) |
106 | | addcl 10335 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℂ ∧ 𝑤
∈ ℂ) → (1 + 𝑤) ∈ ℂ) |
107 | 9, 53, 106 | sylancr 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + 𝑤) ∈
ℂ) |
108 | | 2nn0 11638 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ0 |
109 | 75 | eftlcl 15210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑤 ∈ ℂ ∧ 2 ∈
ℕ0) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
110 | 53, 108, 109 | sylancl 582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
111 | 50, 107, 110 | subaddd 10732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − (1
+ 𝑤)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ↔ ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤))) |
112 | 105, 111 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − (1 +
𝑤)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
113 | 74, 112 | eqtrd 2862 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
114 | 68, 73, 113 | 3eqtr3d 2870 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
115 | 114 | fveq2d 6438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
116 | 53, 57 | absmuld 14571 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1)))) |
117 | 115, 116 | eqtr3d 2864 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)))) |
118 | | eqid 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝑤)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘𝑤)↑𝑛) / (!‘𝑛))) |
119 | | eqid 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) = (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) |
120 | | 2nn 11425 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 2 ∈
ℕ) |
122 | | 1red 10358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℝ) |
123 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) <
1) |
124 | 49, 122, 123 | ltled 10505 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ≤
1) |
125 | 75, 118, 119, 121, 53, 124 | eftlub 15212 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
126 | 117, 125 | eqbrtrrd 4898 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
127 | | df-3 11416 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
128 | | fac2 13360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(!‘2) = 2 |
129 | 128 | oveq1i 6916 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((!‘2) · 2) = (2 · 2) |
130 | | 2t2e4 11523 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
131 | 129, 130 | eqtr2i 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 =
((!‘2) · 2) |
132 | 127, 131 | oveq12i 6918 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 / 4) =
((2 + 1) / ((!‘2) · 2)) |
133 | 132 | oveq2i 6917 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝑤)↑2) · (3 / 4)) =
(((abs‘𝑤)↑2)
· ((2 + 1) / ((!‘2) · 2))) |
134 | 126, 133 | syl6breqr 4916 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · (3 / 4))) |
135 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ∈
ℝ) |
136 | 49 | sqge0d 13333 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ≤
((abs‘𝑤)↑2)) |
137 | | 1re 10357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
138 | | 3lt4 11533 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 <
4 |
139 | | 4cn 11438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℂ |
140 | 139 | mulid1i 10362 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4
· 1) = 4 |
141 | 138, 140 | breqtrri 4901 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 < (4
· 1) |
142 | | 4re 11437 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℝ |
143 | | 4pos 11466 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
4 |
144 | 142, 143 | pm3.2i 464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4 ∈
ℝ ∧ 0 < 4) |
145 | | ltdivmul 11229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℝ ∧ 1 ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4))
→ ((3 / 4) < 1 ↔ 3 < (4 · 1))) |
146 | 61, 137, 144, 145 | mp3an 1591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3 / 4)
< 1 ↔ 3 < (4 · 1)) |
147 | 141, 146 | mpbir 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3 / 4)
< 1 |
148 | 64, 137, 147 | ltleii 10480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 / 4)
≤ 1 |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ≤
1) |
150 | 135, 122,
60, 136, 149 | lemul2ad 11295 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ (((abs‘𝑤)↑2) · 1)) |
151 | 49 | recnd 10386 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℂ) |
152 | 151 | sqcld 13301 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℂ) |
153 | 152 | mulid1d 10375 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· 1) = ((abs‘𝑤)↑2)) |
154 | 150, 153 | breqtrd 4900 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ ((abs‘𝑤)↑2)) |
155 | 59, 66, 60, 134, 154 | letrd 10514 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)↑2)) |
156 | 151 | sqvald 13300 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2) =
((abs‘𝑤) ·
(abs‘𝑤))) |
157 | 155, 156 | breqtrd 4900 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤))) |
158 | | absgt0 14442 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
159 | 158 | ad2antrr 719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
160 | 54, 159 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 <
(abs‘𝑤)) |
161 | 49, 160 | elrpd 12154 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ+) |
162 | 58, 49, 161 | lemul2d 12201 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤) ↔ ((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤)))) |
163 | 157, 162 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
164 | 163 | ad2ant2l 754 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
165 | | simprl 789 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) < 𝑥) |
166 | 44, 45, 47, 164, 165 | lelttrd 10515 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
< 𝑥) |
167 | 35, 166 | eqbrtrd 4896 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
168 | 167 | ex 403 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
169 | 24, 168 | sylbid 232 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
170 | 169 | adantld 486 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
171 | 13, 170 | sylan2b 589 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
172 | 171 | ralrimiva 3176 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ∀𝑤 ∈
(ℂ ∖ {0})((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
173 | | brimralrspcev 4935 |
. . . . 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)) < 𝑥)) |
174 | 12, 172, 173 | syl2anc 581 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ∃𝑦 ∈
ℝ+ ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
175 | 174 | rgen 3132 |
. . 3
⊢
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
176 | | eldifi 3960 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
177 | | efcl 15186 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ →
(exp‘𝑧) ∈
ℂ) |
178 | 176, 177 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (exp‘𝑧) ∈
ℂ) |
179 | | 1cnd 10352 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 1 ∈ ℂ) |
180 | 178, 179 | subcld 10714 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((exp‘𝑧)
− 1) ∈ ℂ) |
181 | | eldifsni 4541 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
182 | 180, 176,
181 | divcld 11128 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) ∈
ℂ) |
183 | 31, 182 | fmpti 6632 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)):(ℂ
∖ {0})⟶ℂ |
184 | 183 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
185 | | difssd 3966 |
. . . . 5
⊢ (⊤
→ (ℂ ∖ {0}) ⊆ ℂ) |
186 | | 0cnd 10350 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℂ) |
187 | 184, 185,
186 | ellimc3 24043 |
. . . 4
⊢ (⊤
→ (1 ∈ ((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))) |
188 | 187 | mptru 1666 |
. . 3
⊢ (1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))) |
189 | 9, 175, 188 | mpbir2an 704 |
. 2
⊢ 1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) |
190 | 4 | toponrestid 21097 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
191 | 176 | subid1d 10703 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (𝑧 − 0) =
𝑧) |
192 | 191 | oveq2d 6922 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0)) = (((exp‘𝑧) − (exp‘0)) / 𝑧)) |
193 | | ef0 15194 |
. . . . . . . 8
⊢
(exp‘0) = 1 |
194 | 193 | oveq2i 6917 |
. . . . . . 7
⊢
((exp‘𝑧)
− (exp‘0)) = ((exp‘𝑧) − 1) |
195 | 194 | oveq1i 6916 |
. . . . . 6
⊢
(((exp‘𝑧)
− (exp‘0)) / 𝑧)
= (((exp‘𝑧) −
1) / 𝑧) |
196 | 192, 195 | syl6req 2879 |
. . . . 5
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) =
(((exp‘𝑧) −
(exp‘0)) / (𝑧 −
0))) |
197 | 196 | mpteq2ia 4964 |
. . . 4
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0))) |
198 | | ssidd 3850 |
. . . 4
⊢ (⊤
→ ℂ ⊆ ℂ) |
199 | | eff 15185 |
. . . . 5
⊢
exp:ℂ⟶ℂ |
200 | 199 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
201 | 190, 2, 197, 198, 200, 198 | eldv 24062 |
. . 3
⊢ (⊤
→ (0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0)))) |
202 | 201 | mptru 1666 |
. 2
⊢
(0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0))) |
203 | 8, 189, 202 | mpbir2an 704 |
1
⊢ 0(ℂ
D exp)1 |