| Step | Hyp | Ref
| Expression |
| 1 | | 0cn 11253 |
. . 3
⊢ 0 ∈
ℂ |
| 2 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 3 | 2 | cnfldtop 24804 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈ Top |
| 4 | | unicntop 24806 |
. . . . 5
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 5 | 4 | ntrtop 23078 |
. . . 4
⊢
((TopOpen‘ℂfld) ∈ Top →
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ) |
| 6 | 3, 5 | ax-mp 5 |
. . 3
⊢
((int‘(TopOpen‘ℂfld))‘ℂ) =
ℂ |
| 7 | 1, 6 | eleqtrri 2840 |
. 2
⊢ 0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) |
| 8 | | ax-1cn 11213 |
. . 3
⊢ 1 ∈
ℂ |
| 9 | | 1rp 13038 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
| 10 | | ifcl 4571 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
| 11 | 9, 10 | mpan2 691 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ if(𝑥 ≤ 1, 𝑥, 1) ∈
ℝ+) |
| 12 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝑤 ∈ (ℂ ∖ {0})
↔ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
| 13 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑤 ∈
ℂ) |
| 14 | 13 | subid1d 11609 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(𝑤 − 0) = 𝑤) |
| 15 | 14 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘(𝑤 − 0)) =
(abs‘𝑤)) |
| 16 | 15 | breq1d 5153 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ (abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1))) |
| 17 | 13 | abscld 15475 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(abs‘𝑤) ∈
ℝ) |
| 18 | | rpre 13043 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
𝑥 ∈
ℝ) |
| 20 | | 1red 11262 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) → 1
∈ ℝ) |
| 21 | | ltmin 13236 |
. . . . . . . . . . 11
⊢
(((abs‘𝑤)
∈ ℝ ∧ 𝑥
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑤) < if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
| 22 | 17, 19, 20, 21 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘𝑤) <
if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
| 23 | 16, 22 | bitrd 279 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) ↔ ((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1))) |
| 24 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0)) |
| 25 | 24, 12 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈ (ℂ ∖
{0})) |
| 26 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (exp‘𝑧) = (exp‘𝑤)) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((exp‘𝑧) − 1) = ((exp‘𝑤) − 1)) |
| 28 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
| 29 | 27, 28 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (((exp‘𝑧) − 1) / 𝑧) = (((exp‘𝑤) − 1) / 𝑤)) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) |
| 31 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
(((exp‘𝑤)
− 1) / 𝑤) ∈
V |
| 32 | 29, 30, 31 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
| 33 | 25, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → ((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) = (((exp‘𝑤) − 1) / 𝑤)) |
| 34 | 33 | fvoveq1d 7453 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) =
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) |
| 35 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ∈
ℂ) |
| 36 | | efcl 16118 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) ∈
ℂ) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(exp‘𝑤) ∈
ℂ) |
| 38 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 1 ∈
ℂ) |
| 39 | 37, 38 | subcld 11620 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((exp‘𝑤) − 1)
∈ ℂ) |
| 40 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑤 ≠ 0) |
| 41 | 39, 35, 40 | divcld 12043 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
| 42 | 41, 38 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
| 43 | 42 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
| 44 | 35 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) ∈
ℝ) |
| 45 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ+) |
| 46 | 45 | rpred 13077 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) → 𝑥 ∈
ℝ) |
| 47 | | abscl 15317 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ →
(abs‘𝑤) ∈
ℝ) |
| 48 | 47 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ) |
| 49 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) ∈
ℂ) |
| 50 | | subcl 11507 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((exp‘𝑤)
∈ ℂ ∧ 1 ∈ ℂ) → ((exp‘𝑤) − 1) ∈ ℂ) |
| 51 | 49, 8, 50 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − 1)
∈ ℂ) |
| 52 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ∈
ℂ) |
| 53 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 𝑤 ≠ 0) |
| 54 | 51, 52, 53 | divcld 12043 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
/ 𝑤) ∈
ℂ) |
| 55 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℂ) |
| 56 | 54, 55 | subcld 11620 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − 1) ∈
ℂ) |
| 57 | 56 | abscld 15475 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
∈ ℝ) |
| 58 | 48, 57 | remulcld 11291 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ∈ ℝ) |
| 59 | 48 | resqcld 14165 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℝ) |
| 60 | | 3re 12346 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
| 61 | | 4nn 12349 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
| 62 | | nndivre 12307 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℝ ∧ 4 ∈ ℕ) → (3 / 4) ∈
ℝ) |
| 63 | 60, 61, 62 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (3 / 4)
∈ ℝ |
| 64 | | remulcl 11240 |
. . . . . . . . . . . . . . . . 17
⊢
((((abs‘𝑤)↑2) ∈ ℝ ∧ (3 / 4) ∈
ℝ) → (((abs‘𝑤)↑2) · (3 / 4)) ∈
ℝ) |
| 65 | 59, 63, 64 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ∈ ℝ) |
| 66 | 51, 52 | subcld 11620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) ∈
ℂ) |
| 67 | 66, 52, 53 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (((exp‘𝑤) − 1) − 𝑤)) |
| 68 | 51, 52, 52, 53 | divsubdird 12082 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − (𝑤 / 𝑤))) |
| 69 | 52, 53 | dividd 12041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 𝑤) = 1) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
/ 𝑤) − (𝑤 / 𝑤)) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
| 71 | 68, 70 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((((exp‘𝑤) − 1)
− 𝑤) / 𝑤) = ((((exp‘𝑤) − 1) / 𝑤) − 1)) |
| 72 | 71 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) − 𝑤) / 𝑤)) = (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1))) |
| 73 | 49, 55, 52 | subsub4d 11651 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) =
((exp‘𝑤) − (1 +
𝑤))) |
| 74 | | addcl 11237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ 𝑤
∈ ℂ) → (1 + 𝑤) ∈ ℂ) |
| 75 | 8, 52, 74 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + 𝑤) ∈
ℂ) |
| 76 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℕ0 |
| 77 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ0
↦ ((𝑤↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛))) |
| 78 | 77 | eftlcl 16143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 ∈ ℂ ∧ 2 ∈
ℕ0) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
| 79 | 52, 76, 78 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) ∈ ℂ) |
| 80 | | df-2 12329 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 = (1 +
1) |
| 81 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℕ0 |
| 82 | | 1e0p1 12775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 = (0 +
1) |
| 83 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℕ0 |
| 84 | | 0cnd 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ∈
ℂ) |
| 85 | 77 | efval2 16120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
| 86 | 85 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) =
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
| 87 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
ℕ0 = (ℤ≥‘0) |
| 88 | 87 | sumeq1i 15733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
Σ𝑘 ∈
ℕ0 ((𝑛
∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) |
| 89 | 86, 88 | eqtr2di 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘) = (exp‘𝑤)) |
| 90 | 89 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = (0 + (exp‘𝑤))) |
| 91 | 49 | addlidd 11462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 +
(exp‘𝑤)) =
(exp‘𝑤)) |
| 92 | 90, 91 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (0 +
Σ𝑘 ∈
(ℤ≥‘0)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 93 | | eft0val 16148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ ℂ → ((𝑤↑0) / (!‘0)) =
1) |
| 94 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑0) / (!‘0)) =
1) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) = (0 +
1)) |
| 96 | 95, 82 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (0 + ((𝑤↑0) / (!‘0))) =
1) |
| 97 | 77, 82, 83, 52, 84, 92, 96 | efsep 16146 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = (1 +
Σ𝑘 ∈
(ℤ≥‘1)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 98 | | exp1 14108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ ℂ → (𝑤↑1) = 𝑤) |
| 99 | 98 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤↑1) = 𝑤) |
| 100 | 99 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 /
(!‘1))) |
| 101 | | fac1 14316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(!‘1) = 1 |
| 102 | 101 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 / (!‘1)) = (𝑤 / 1) |
| 103 | 100, 102 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = (𝑤 / 1)) |
| 104 | | div1 11957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℂ → (𝑤 / 1) = 𝑤) |
| 105 | 104 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 / 1) = 𝑤) |
| 106 | 103, 105 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → ((𝑤↑1) / (!‘1)) = 𝑤) |
| 107 | 106 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (1 + ((𝑤↑1) / (!‘1))) = (1 +
𝑤)) |
| 108 | 77, 80, 81, 52, 55, 97, 107 | efsep 16146 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(exp‘𝑤) = ((1 + 𝑤) + Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 109 | 75, 79, 108 | mvrladdd 11676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((exp‘𝑤) − (1 +
𝑤)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
| 110 | 73, 109 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((exp‘𝑤) − 1)
− 𝑤) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
| 111 | 67, 72, 110 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 · ((((exp‘𝑤) − 1) / 𝑤) − 1)) = Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) |
| 112 | 111 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘))) |
| 113 | 52, 56 | absmuld 15493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘(𝑤 ·
((((exp‘𝑤) − 1)
/ 𝑤) − 1))) =
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1)))) |
| 114 | 112, 113 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) = ((abs‘𝑤) · (abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)))) |
| 115 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝑤)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘𝑤)↑𝑛) / (!‘𝑛))) |
| 116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) = (𝑛 ∈ ℕ0
↦ ((((abs‘𝑤)↑2) / (!‘2)) · ((1 / (2 +
1))↑𝑛))) |
| 117 | | 2nn 12339 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℕ |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 2 ∈
ℕ) |
| 119 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 1 ∈
ℝ) |
| 120 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) <
1) |
| 121 | 48, 119, 120 | ltled 11409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ≤
1) |
| 122 | 77, 115, 116, 118, 52, 121 | eftlub 16145 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘2)((𝑛 ∈ ℕ0 ↦ ((𝑤↑𝑛) / (!‘𝑛)))‘𝑘)) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
| 123 | 114, 122 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · ((2 + 1) / ((!‘2)
· 2)))) |
| 124 | | df-3 12330 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 = (2 +
1) |
| 125 | | fac2 14318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(!‘2) = 2 |
| 126 | 125 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((!‘2) · 2) = (2 · 2) |
| 127 | | 2t2e4 12430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
| 128 | 126, 127 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 =
((!‘2) · 2) |
| 129 | 124, 128 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 / 4) =
((2 + 1) / ((!‘2) · 2)) |
| 130 | 129 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝑤)↑2) · (3 / 4)) =
(((abs‘𝑤)↑2)
· ((2 + 1) / ((!‘2) · 2))) |
| 131 | 123, 130 | breqtrrdi 5185 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ (((abs‘𝑤)↑2) · (3 / 4))) |
| 132 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ∈
ℝ) |
| 133 | 48 | sqge0d 14177 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 ≤
((abs‘𝑤)↑2)) |
| 134 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
| 135 | | 3lt4 12440 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 <
4 |
| 136 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℂ |
| 137 | 136 | mulridi 11265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4
· 1) = 4 |
| 138 | 135, 137 | breqtrri 5170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 < (4
· 1) |
| 139 | | 4re 12350 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 4 ∈
ℝ |
| 140 | | 4pos 12373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
4 |
| 141 | 139, 140 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (4 ∈
ℝ ∧ 0 < 4) |
| 142 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((3
∈ ℝ ∧ 1 ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4))
→ ((3 / 4) < 1 ↔ 3 < (4 · 1))) |
| 143 | 60, 134, 141, 142 | mp3an 1463 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3 / 4)
< 1 ↔ 3 < (4 · 1)) |
| 144 | 138, 143 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3 / 4)
< 1 |
| 145 | 63, 134, 144 | ltleii 11384 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 / 4)
≤ 1 |
| 146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (3 / 4) ≤
1) |
| 147 | 132, 119,
59, 133, 146 | lemul2ad 12208 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ (((abs‘𝑤)↑2) · 1)) |
| 148 | 48 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℂ) |
| 149 | 148 | sqcld 14184 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2)
∈ ℂ) |
| 150 | 149 | mulridd 11278 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· 1) = ((abs‘𝑤)↑2)) |
| 151 | 147, 150 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(((abs‘𝑤)↑2)
· (3 / 4)) ≤ ((abs‘𝑤)↑2)) |
| 152 | 58, 65, 59, 131, 151 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)↑2)) |
| 153 | 148 | sqvald 14183 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤)↑2) =
((abs‘𝑤) ·
(abs‘𝑤))) |
| 154 | 152, 153 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤))) |
| 155 | | absgt0 15363 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℂ → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
| 156 | 155 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → (𝑤 ≠ 0 ↔ 0 <
(abs‘𝑤))) |
| 157 | 53, 156 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) → 0 <
(abs‘𝑤)) |
| 158 | 48, 157 | elrpd 13074 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘𝑤) ∈
ℝ+) |
| 159 | 57, 48, 158 | lemul2d 13121 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
((abs‘((((exp‘𝑤) − 1) / 𝑤) − 1)) ≤ (abs‘𝑤) ↔ ((abs‘𝑤) ·
(abs‘((((exp‘𝑤)
− 1) / 𝑤) −
1))) ≤ ((abs‘𝑤)
· (abs‘𝑤)))) |
| 160 | 154, 159 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) ∧ (abs‘𝑤) < 1) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
| 161 | 160 | ad2ant2l 746 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
≤ (abs‘𝑤)) |
| 162 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘𝑤) < 𝑥) |
| 163 | 43, 44, 46, 161, 162 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘((((exp‘𝑤)
− 1) / 𝑤) − 1))
< 𝑥) |
| 164 | 34, 163 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) ∧
((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
| 165 | 164 | ex 412 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
(((abs‘𝑤) < 𝑥 ∧ (abs‘𝑤) < 1) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 166 | 23, 165 | sylbid 240 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 167 | 166 | adantld 490 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ (𝑤 ∈ ℂ
∧ 𝑤 ≠ 0)) →
((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< if(𝑥 ≤ 1, 𝑥, 1)) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 168 | 12, 167 | sylan2b 594 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 169 | 168 | ralrimiva 3146 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ∀𝑤 ∈
(ℂ ∖ {0})((𝑤
≠ 0 ∧ (abs‘(𝑤
− 0)) < if(𝑥 ≤
1, 𝑥, 1)) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 170 | | brimralrspcev 5204 |
. . . . 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)) < 𝑥)) |
| 171 | 11, 169, 170 | syl2anc 584 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ∃𝑦 ∈
ℝ+ ∀𝑤 ∈ (ℂ ∖ {0})((𝑤 ≠ 0 ∧ (abs‘(𝑤 − 0)) < 𝑦) → (abs‘(((𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧))‘𝑤) − 1)) < 𝑥)) |
| 172 | 171 | rgen 3063 |
. . 3
⊢
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥) |
| 173 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
| 174 | | efcl 16118 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ →
(exp‘𝑧) ∈
ℂ) |
| 175 | 173, 174 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (exp‘𝑧) ∈
ℂ) |
| 176 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 1 ∈ ℂ) |
| 177 | 175, 176 | subcld 11620 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((exp‘𝑧)
− 1) ∈ ℂ) |
| 178 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
| 179 | 177, 173,
178 | divcld 12043 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) ∈
ℂ) |
| 180 | 30, 179 | fmpti 7132 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)):(ℂ
∖ {0})⟶ℂ |
| 181 | 180 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)):(ℂ ∖
{0})⟶ℂ) |
| 182 | | difssd 4137 |
. . . . 5
⊢ (⊤
→ (ℂ ∖ {0}) ⊆ ℂ) |
| 183 | | 0cnd 11254 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℂ) |
| 184 | 181, 182,
183 | ellimc3 25914 |
. . . 4
⊢ (⊤
→ (1 ∈ ((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥)))) |
| 185 | 184 | mptru 1547 |
. . 3
⊢ (1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) ↔ (1 ∈
ℂ ∧ ∀𝑥
∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑤 ≠ 0 ∧
(abs‘(𝑤 − 0))
< 𝑦) →
(abs‘(((𝑧 ∈
(ℂ ∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧))‘𝑤) − 1)) < 𝑥))) |
| 186 | 8, 172, 185 | mpbir2an 711 |
. 2
⊢ 1 ∈
((𝑧 ∈ (ℂ ∖
{0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ 0) |
| 187 | 2 | cnfldtopon 24803 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 188 | 187 | toponrestid 22927 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 189 | 173 | subid1d 11609 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (𝑧 − 0) =
𝑧) |
| 190 | 189 | oveq2d 7447 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0)) = (((exp‘𝑧) − (exp‘0)) / 𝑧)) |
| 191 | | ef0 16127 |
. . . . . . . 8
⊢
(exp‘0) = 1 |
| 192 | 191 | oveq2i 7442 |
. . . . . . 7
⊢
((exp‘𝑧)
− (exp‘0)) = ((exp‘𝑧) − 1) |
| 193 | 192 | oveq1i 7441 |
. . . . . 6
⊢
(((exp‘𝑧)
− (exp‘0)) / 𝑧)
= (((exp‘𝑧) −
1) / 𝑧) |
| 194 | 190, 193 | eqtr2di 2794 |
. . . . 5
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (((exp‘𝑧)
− 1) / 𝑧) =
(((exp‘𝑧) −
(exp‘0)) / (𝑧 −
0))) |
| 195 | 194 | mpteq2ia 5245 |
. . . 4
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− 1) / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (((exp‘𝑧)
− (exp‘0)) / (𝑧
− 0))) |
| 196 | | ssidd 4007 |
. . . 4
⊢ (⊤
→ ℂ ⊆ ℂ) |
| 197 | | eff 16117 |
. . . . 5
⊢
exp:ℂ⟶ℂ |
| 198 | 197 | a1i 11 |
. . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) |
| 199 | 188, 2, 195, 196, 198, 196 | eldv 25933 |
. . 3
⊢ (⊤
→ (0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0)))) |
| 200 | 199 | mptru 1547 |
. 2
⊢
(0(ℂ D exp)1 ↔ (0 ∈
((int‘(TopOpen‘ℂfld))‘ℂ) ∧ 1
∈ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (((exp‘𝑧) − 1) / 𝑧)) limℂ
0))) |
| 201 | 7, 186, 200 | mpbir2an 711 |
1
⊢ 0(ℂ
D exp)1 |