Step | Hyp | Ref
| Expression |
1 | | 0cn 9911 |
. . 3
⊢ 0 ∈
ℂ |
2 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
3 | 2 | cnfldtop 22397 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈ Top |
4 | 2 | cnfldtopon 22396 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
5 | 4 | toponunii 20547 |
. . . . 5
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
6 | 5 | ntrtop 20684 |
. . . 4
⊢
((TopOpen‘ℂfld) ∈ Top →
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ) |
7 | 3, 6 | ax-mp 5 |
. . 3
⊢
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ |
8 | 1, 7 | eleqtrri 2687 |
. 2
⊢ 0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) |
9 | | ax-1cn 9873 |
. . 3
⊢ 1 ∈
ℂ |
10 | | 1rp 11712 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
11 | | ifcl 4080 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
12 | 10, 11 | mpan2 703 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
13 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝑤 ∈ (ℂ ∖ {0})
↔ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
14 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑤 ∈
ℂ) |
15 | 14 | subid1d 10260 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(𝑤 − 0) = 𝑤) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘(𝑤 − 0)) =
(abs‘𝑤)) |
17 | 16 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ (abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1))) |
18 | 14 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘𝑤) ∈
ℝ) |
19 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑥 ∈
ℝ) |
21 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) → 1
∈ ℝ) |
22 | | ltmin 11899 |
. . . . . . . . . . 11
⊢
(((abs‘𝑤)
∈ ℝ ∧ 𝑥
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
23 | 18, 20, 21, 22 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘𝑤) <
if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
24 | 17, 23 | bitrd 267 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
25 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) |
26 | 25, 13 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈ (ℂ ∖
{0})) |
27 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → (exp‘𝑧) = (exp‘𝑤)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → ((exp‘𝑧) − 1) = ((exp‘𝑤) − 1)) |
29 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
30 | 28, 29 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (((exp‘𝑧) − 1) / 𝑧) = (((exp‘𝑤) − 1) / 𝑤)) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) |
32 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(((exp‘𝑤)
− 1) / 𝑤) ∈
V |
33 | 30, 31, 32 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
35 | 34 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) =
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) |
37 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈
ℂ) |
38 | | efcl 14652 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) ∈
ℂ) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(exp‘𝑤) ∈
ℂ) |
40 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 1 ∈
ℂ) |
41 | 39, 40 | subcld 10271 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((exp‘𝑤) − 1)
∈ ℂ) |
42 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ≠ 0) |
43 | 41, 37, 42 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
44 | 43, 40 | subcld 10271 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
45 | 44 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
46 | 37 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) ∈
ℝ) |
47 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ+) |
48 | 47 | rpred 11748 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ) |
49 | | abscl 13866 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ →
(abs‘𝑤) ∈
ℝ) |
50 | 49 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ) |
51 | 38 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) ∈
ℂ) |
52 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((exp‘𝑤)
∈ ℂ ∧ 1 ∈ ℂ) → ((exp‘𝑤) − 1) ∈ ℂ) |
53 | 51, 9, 52 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − 1)
∈ ℂ) |
54 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ∈
ℂ) |
55 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ≠ 0) |
56 | 53, 54, 55 | divcld 10680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
57 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℂ) |
58 | 56, 57 | subcld 10271 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
59 | 58 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
60 | 50, 59 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ∈ ℝ) |
61 | 50 | resqcld 12897 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℝ) |
62 | | 3re 10971 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
63 | | 4nn 11064 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
64 | | nndivre 10933 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℝ ∧ 4 ∈ ℕ) → (3 / 4) ∈
ℝ) |
65 | 62, 63, 64 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢ (3 / 4)
∈ ℝ |
66 | | remulcl 9900 |
. . . . . . . . . . . . . . . . 17
⊢
((((abs‘𝑤)↑2) ∈ ℝ ∧ (3 / 4) ∈
ℝ) → (((abs‘𝑤)↑2) · (3 / 4)) ∈
ℝ) |
67 | 61, 65, 66 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ∈ ℝ) |
68 | 53, 54 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) ∈
ℂ) |
69 | 68, 54, 55 | divcan2d 10682 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (((exp‘𝑤) − 1) − 𝑤)) |
70 | 53, 54, 54, 55 | divsubdird 10719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − (𝑤 / 𝑤))) |
71 | 54, 55 | dividd 10678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 𝑤) = 1) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − (𝑤 / 𝑤)) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
73 | 70, 72 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
74 | 73 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1))) |
75 | 51, 57, 54 | subsub4d 10302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) =
((exp‘𝑤) − (1 +
𝑤))) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ0
↦ ((𝑤↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛))) |
77 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 = (1 +
1) |
78 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℕ0 |
79 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 = (0 +
1) |
80 | | 0nn0 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
ℕ0 |
81 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ∈
ℂ) |
82 | 76 | efval2 14653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
83 | 82 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
84 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
ℕ0 = (ℤ≥‘0) |
85 | 84 | sumeq1i 14276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) |
86 | 83, 85 | syl6req 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = (exp‘𝑤)) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (0 + (exp‘𝑤))) |
88 | 51 | addid2d 10116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
(exp‘𝑤)) =
(exp‘𝑤)) |
89 | 87, 88 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
90 | | eft0val 14681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ ℂ → ((𝑤↑0) / (!‘0)) =
1) |
91 | 90 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑0) / (!‘0)) =
1) |
92 | 91 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) = (0 +
1)) |
93 | 92, 79 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) =
1) |
94 | 76, 79, 80, 54, 81, 89, 93 | efsep 14679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (1 +
Σ𝑘 ∈
(ℤ≥‘1)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
95 | | exp1 12728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 ∈ ℂ → (𝑤↑1) = 𝑤) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤↑1) = 𝑤) |
97 | 96 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 /
(!‘1))) |
98 | | fac1 12926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(!‘1) = 1 |
99 | 98 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 / (!‘1)) = (𝑤 / 1) |
100 | 97, 99 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 / 1)) |
101 | | div1 10595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ ℂ → (𝑤 / 1) = 𝑤) |
102 | 101 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 1) = 𝑤) |
103 | 100, 102 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = 𝑤) |
104 | 103 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + ((𝑤↑1) / (!‘1))) = (1 +
𝑤)) |
105 | 76, 77, 78, 54, 57, 94, 104 | efsep 14679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
106 | 105 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤)) |
107 | | addcl 9897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℂ ∧ 𝑤
∈ ℂ) → (1 + 𝑤) ∈ ℂ) |
108 | 9, 54, 107 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + 𝑤) ∈
ℂ) |
109 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ0 |
110 | 76 | eftlcl 14676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑤 ∈ ℂ ∧ 2 ∈
ℕ0) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
111 | 54, 109, 110 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
112 | 51, 108, 111 | subaddd 10289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − (1
+ 𝑤)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ↔ ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (exp‘𝑤))) |
113 | 106, 112 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − (1 +
𝑤)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
114 | 75, 113 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
115 | 69, 74, 114 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
116 | 115 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
117 | 54, 58 | absmuld 14041 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1)))) |
118 | 116, 117 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)))) |
119 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝑤)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘𝑤)↑𝑛) / (!‘𝑛))) |
120 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) = (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) |
121 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 2 ∈
ℕ) |
123 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℝ) |
124 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) <
1) |
125 | 50, 123, 124 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ≤
1) |
126 | 76, 119, 120, 122, 54, 125 | eftlub 14678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
127 | 118, 126 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
128 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
129 | | fac2 12928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(!‘2) = 2 |
130 | 129 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((!‘2) · 2) = (2 · 2) |
131 | | 2t2e4 11054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
132 | 130, 131 | eqtr2i 2633 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 =
((!‘2) · 2) |
133 | 128, 132 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 / 4) =
((2 + 1) / ((!‘2) · 2)) |
134 | 133 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝑤)↑2) · (3 / 4)) =
(((abs‘𝑤)↑2)
· ((2 + 1) / ((!‘2) · 2))) |
135 | 127, 134 | syl6breqr 4625 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · (3 / 4))) |
136 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ∈
ℝ) |
137 | 50 | sqge0d 12898 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ≤
((abs‘𝑤)↑2)) |
138 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
139 | | 3lt4 11074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 <
4 |
140 | | 4cn 10975 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℂ |
141 | 140 | mulid1i 9921 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4
· 1) = 4 |
142 | 139, 141 | breqtrri 4610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 < (4
· 1) |
143 | | 4re 10974 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℝ |
144 | | 4pos 10993 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
4 |
145 | 143, 144 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4 ∈
ℝ ∧ 0 < 4) |
146 | | ltdivmul 10777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℝ ∧ 1 ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4))
→ ((3 / 4) < 1 ↔ 3 < (4 · 1))) |
147 | 62, 138, 145, 146 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3 / 4)
< 1 ↔ 3 < (4 · 1)) |
148 | 142, 147 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3 / 4)
< 1 |
149 | 65, 138, 148 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 / 4)
≤ 1 |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ≤
1) |
151 | 136, 123,
61, 137, 150 | lemul2ad 10843 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ (((abs‘𝑤)↑2) · 1)) |
152 | 50 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℂ) |
153 | 152 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℂ) |
154 | 153 | mulid1d 9936 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· 1) = ((abs‘𝑤)↑2)) |
155 | 151, 154 | breqtrd 4609 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ ((abs‘𝑤)↑2)) |
156 | 60, 67, 61, 135, 155 | letrd 10073 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)↑2)) |
157 | 152 | sqvald 12867 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2) =
((abs‘𝑤) ·
(abs‘𝑤))) |
158 | 156, 157 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤))) |
159 | | absgt0 13912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
160 | 159 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
161 | 55, 160 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 <
(abs‘𝑤)) |
162 | 50, 161 | elrpd 11745 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ+) |
163 | 59, 50, 162 | lemul2d 11792 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤) ↔ ((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤)))) |
164 | 158, 163 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
165 | 164 | ad2ant2l 778 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
166 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) < 𝑥) |
167 | 45, 46, 48, 165, 166 | lelttrd 10074 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
< 𝑥) |
168 | 36, 167 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
169 | 168 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
170 | 24, 169 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
171 | 170 | adantld 482 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
172 | 13, 171 | sylan2b 491 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
173 | 172 | ralrimiva 2949 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ∀𝑤 ∈
(ℂ ∖ {0})((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
174 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → ((abs‘(𝑤 − 0)) < 𝑦 ↔ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1))) |
175 | 174 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) ↔ (𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)))) |
176 | 175 | imbi1d 330 |
. . . . . . 7
⊢ (𝑦 = if(𝑥 ≤ 1, 𝑥, 1) → (((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦
(((exp‘𝑧) − 1)
/ 𝑧))‘𝑤) − 1)) < 𝑥) ↔ ((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0}) ↦
(((exp‘𝑧) − 1)
/ 𝑧))‘𝑤) − 1)) < 𝑥))) |
177 | 176 | ralbidv 2969 |
. . . . . 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)) < 𝑥))) |
178 | 177 | rspcev 3282 |
. . . . 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)) < 𝑥)) |
179 | 12, 173, 178 | syl2anc 691 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ∃𝑦 ∈
ℝ+ ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
180 | 179 | rgen 2906 |
. . 3
⊢
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
181 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
182 | | efcl 14652 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ →
(exp‘𝑧) ∈
ℂ) |
183 | 181, 182 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (exp‘𝑧) ∈
ℂ) |
184 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 1 ∈ ℂ) |
185 | 183, 184 | subcld 10271 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((exp‘𝑧)
− 1) ∈ ℂ) |
186 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
187 | 185, 181,
186 | divcld 10680 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) ∈
ℂ) |
188 | 31, 187 | fmpti 6291 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)):(ℂ
∖ {0})⟶ℂ |
189 | 188 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
190 | | difssd 3700 |
. . . . 5
⊢ (⊤
→ (ℂ ∖ {0}) ⊆ ℂ) |
191 | | 0cnd 9912 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℂ) |
192 | 189, 190,
191 | ellimc3 23449 |
. . . 4
⊢ (⊤
→ (1 ∈ ((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))) |
193 | 192 | trud 1484 |
. . 3
⊢ (1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))) |
194 | 9, 180, 193 | mpbir2an 957 |
. 2
⊢ 1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) |
195 | 5 | restid 15917 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
196 | 3, 195 | ax-mp 5 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
197 | 196 | eqcomi 2619 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
198 | 181 | subid1d 10260 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (𝑧 − 0) =
𝑧) |
199 | 198 | oveq2d 6565 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0)) = (((exp‘𝑧) − (exp‘0)) / 𝑧)) |
200 | | ef0 14660 |
. . . . . . . 8
⊢
(exp‘0) = 1 |
201 | 200 | oveq2i 6560 |
. . . . . . 7
⊢
((exp‘𝑧)
− (exp‘0)) = ((exp‘𝑧) − 1) |
202 | 201 | oveq1i 6559 |
. . . . . 6
⊢
(((exp‘𝑧)
− (exp‘0)) / 𝑧)
= (((exp‘𝑧) −
1) / 𝑧) |
203 | 199, 202 | syl6req 2661 |
. . . . 5
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) =
(((exp‘𝑧) −
(exp‘0)) / (𝑧 −
0))) |
204 | 203 | mpteq2ia 4668 |
. . . 4
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0))) |
205 | | ssid 3587 |
. . . . 5
⊢ ℂ
⊆ ℂ |
206 | 205 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ⊆ ℂ) |
207 | | eff 14651 |
. . . . 5
⊢
exp:ℂ⟶ℂ |
208 | 207 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
209 | 197, 2, 204, 206, 208, 206 | eldv 23468 |
. . 3
⊢ (⊤
→ (0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0)))) |
210 | 209 | trud 1484 |
. 2
⊢
(0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0))) |
211 | 8, 194, 210 | mpbir2an 957 |
1
⊢ 0(ℂ
D exp)1 |