Step | Hyp | Ref
| Expression |
1 | | reelprrecn 11244 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
3 | | cnelprrecn 11245 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
4 | 3 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
5 | | dfrp2 13432 |
. . . . . . 7
⊢
ℝ+ = (0(,)+∞) |
6 | | mnfxr 11315 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ -∞ ∈ ℝ*) |
8 | | 0xr 11305 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 0 ∈ ℝ*) |
10 | | pnfxr 11312 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ +∞ ∈ ℝ*) |
12 | 7, 9, 11 | iocioodisjd 42333 |
. . . . . . . . . 10
⊢ (⊤
→ ((-∞(,]0) ∩ (0(,)+∞)) = ∅) |
13 | 12 | mptru 1543 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
14 | 13 | ineqcomi 4218 |
. . . . . . . 8
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ |
15 | | disjdif2 4485 |
. . . . . . . 8
⊢
(((0(,)+∞) ∩ (-∞(,]0)) = ∅ → ((0(,)+∞)
∖ (-∞(,]0)) = (0(,)+∞)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . 7
⊢
((0(,)+∞) ∖ (-∞(,]0)) =
(0(,)+∞) |
17 | 5, 16 | eqtr4i 2765 |
. . . . . 6
⊢
ℝ+ = ((0(,)+∞) ∖
(-∞(,]0)) |
18 | | ioosscn 13445 |
. . . . . . 7
⊢
(0(,)+∞) ⊆ ℂ |
19 | | ssdif 4153 |
. . . . . . 7
⊢
((0(,)+∞) ⊆ ℂ → ((0(,)+∞) ∖
(-∞(,]0)) ⊆ (ℂ ∖ (-∞(,]0))) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢
((0(,)+∞) ∖ (-∞(,]0)) ⊆ (ℂ ∖
(-∞(,]0)) |
21 | 17, 20 | eqsstri 4029 |
. . . . 5
⊢
ℝ+ ⊆ (ℂ ∖
(-∞(,]0)) |
22 | | redvabs.d |
. . . . . . . . . . 11
⊢ 𝐷 = (ℝ ∖
{0}) |
23 | 22 | eleq2i 2830 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖
{0})) |
24 | | eldifsn 4790 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ {0})
↔ (𝑥 ∈ ℝ
∧ 𝑥 ≠
0)) |
25 | 23, 24 | bitri 275 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0)) |
26 | 25 | simplbi 497 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ) |
27 | 26 | recnd 11286 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
28 | 27 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) |
29 | 25 | simprbi 496 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
30 | 29 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ≠ 0) |
31 | 28, 30 | absrpcld 15483 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(abs‘𝑥) ∈
ℝ+) |
32 | 21, 31 | sselid 3992 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(abs‘𝑥) ∈
(ℂ ∖ (-∞(,]0))) |
33 | | negex 11503 |
. . . . . 6
⊢ -1 ∈
V |
34 | | 1ex 11254 |
. . . . . 6
⊢ 1 ∈
V |
35 | 33, 34 | ifex 4580 |
. . . . 5
⊢ if(𝑥 < 0, -1, 1) ∈
V |
36 | 35 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → if(𝑥 < 0, -1, 1) ∈
V) |
37 | | eldifi 4140 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
38 | 37 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ∈ ℂ) |
39 | | eldifn 4141 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
40 | | mnflt0 13164 |
. . . . . . . . . 10
⊢ -∞
< 0 |
41 | | ubioc1 13436 |
. . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) |
42 | 6, 8, 40, 41 | mp3an 1460 |
. . . . . . . . 9
⊢ 0 ∈
(-∞(,]0) |
43 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
44 | 42, 43 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
45 | 44 | necon3bi 2964 |
. . . . . . 7
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
46 | 39, 45 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
47 | 46 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ≠ 0) |
48 | 38, 47 | logcld 26626 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
49 | | ovexd 7465 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
50 | 22 | redvmptabs 42368 |
. . . . 5
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1)) |
51 | 50 | a1i 11 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))) |
52 | | logf1o 26620 |
. . . . . . . . . . . . 13
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
53 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
log:(ℂ ∖ {0})⟶ran log |
55 | 54 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
56 | 55 | feqmptd 6976 |
. . . . . . . . . 10
⊢ (⊤
→ log = (𝑦 ∈
(ℂ ∖ {0}) ↦ (log‘𝑦))) |
57 | 56 | mptru 1543 |
. . . . . . . . 9
⊢ log =
(𝑦 ∈ (ℂ ∖
{0}) ↦ (log‘𝑦)) |
58 | 57 | reseq1i 5995 |
. . . . . . . 8
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) = ((𝑦 ∈ (ℂ ∖ {0}) ↦
(log‘𝑦)) ↾
(ℂ ∖ (-∞(,]0))) |
59 | | c0ex 11252 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
60 | 59 | snss 4789 |
. . . . . . . . . 10
⊢ (0 ∈
(-∞(,]0) ↔ {0} ⊆ (-∞(,]0)) |
61 | 42, 60 | mpbi 230 |
. . . . . . . . 9
⊢ {0}
⊆ (-∞(,]0) |
62 | | sscon 4152 |
. . . . . . . . 9
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
63 | | resmpt 6056 |
. . . . . . . . 9
⊢ ((ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) → ((𝑦 ∈ (ℂ ∖ {0})
↦ (log‘𝑦))
↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
64 | 61, 62, 63 | mp2b 10 |
. . . . . . . 8
⊢ ((𝑦 ∈ (ℂ ∖ {0})
↦ (log‘𝑦))
↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦)) |
65 | 58, 64 | eqtr2i 2763 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)) = (log ↾ (ℂ ∖
(-∞(,]0))) |
66 | 65 | oveq2i 7441 |
. . . . . 6
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (log‘𝑦))) = (ℂ D (log ↾ (ℂ
∖ (-∞(,]0)))) |
67 | | eqid 2734 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
68 | 67 | dvlog 26707 |
. . . . . 6
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
69 | 66, 68 | eqtri 2762 |
. . . . 5
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
70 | 69 | a1i 11 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
71 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = (abs‘𝑥) → (log‘𝑦) = (log‘(abs‘𝑥))) |
72 | | oveq2 7438 |
. . . 4
⊢ (𝑦 = (abs‘𝑥) → (1 / 𝑦) = (1 / (abs‘𝑥))) |
73 | 2, 4, 32, 36, 48, 49, 51, 70, 71, 72 | dvmptco 26024 |
. . 3
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1,
1)))) |
74 | 73 | mptru 1543 |
. 2
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1,
1))) |
75 | | ovif2 7531 |
. . . 4
⊢ ((1 /
(abs‘𝑥)) ·
if(𝑥 < 0, -1, 1)) =
if(𝑥 < 0, ((1 /
(abs‘𝑥)) ·
-1), ((1 / (abs‘𝑥))
· 1)) |
76 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ∈
ℝ) |
77 | 76 | recnd 11286 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ∈
ℂ) |
78 | 77 | abscld 15471 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ∈
ℝ) |
79 | 78 | recnd 11286 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ∈
ℂ) |
80 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ≠ 0) |
81 | 77, 80 | absne0d 15482 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ≠ 0) |
82 | 79, 81 | reccld 12033 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℂ) |
83 | | neg1cn 12377 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
84 | 83 | a1i 11 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -1 ∈
ℂ) |
85 | 82, 84 | mulcomd 11279 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · -1)
= (-1 · (1 / (abs‘𝑥)))) |
86 | 82 | mulm1d 11712 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (-1 · (1
/ (abs‘𝑥))) = -(1 /
(abs‘𝑥))) |
87 | | 1cnd 11253 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 1 ∈
ℂ) |
88 | 87, 79, 81 | divneg2d 12054 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -(1 /
(abs‘𝑥)) = (1 /
-(abs‘𝑥))) |
89 | | 0red 11261 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 0 ∈
ℝ) |
90 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 < 0) |
91 | 76, 89, 90 | ltled 11406 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ≤ 0) |
92 | 76, 91 | absnidd 15448 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) = -𝑥) |
93 | 92 | eqcomd 2740 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -𝑥 = (abs‘𝑥)) |
94 | 77, 93 | negcon1ad 11612 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) →
-(abs‘𝑥) = 𝑥) |
95 | 94 | oveq2d 7446 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (1 /
-(abs‘𝑥)) = (1 /
𝑥)) |
96 | 88, 95 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -(1 /
(abs‘𝑥)) = (1 / 𝑥)) |
97 | 85, 86, 96 | 3eqtrd 2778 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · -1)
= (1 / 𝑥)) |
98 | 25, 97 | sylanb 581 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 < 0) → ((1 / (abs‘𝑥)) · -1) = (1 / 𝑥)) |
99 | | recn 11242 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
100 | 99 | abscld 15471 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
101 | 100 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) ∈
ℝ) |
102 | 99 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ∈
ℂ) |
103 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ≠ 0) |
104 | 102, 103 | absne0d 15482 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) ≠ 0) |
105 | 101, 104 | rereccld 12091 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℝ) |
106 | 105 | recnd 11286 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℂ) |
107 | 106 | mulridd 11275 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · 1)
= (1 / (abs‘𝑥))) |
108 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ∈
ℝ) |
109 | | 0red 11261 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → 0 ∈
ℝ) |
110 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℝ) |
111 | 109, 110 | lenltd 11404 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → (0 ≤ 𝑥 ↔ ¬ 𝑥 < 0)) |
112 | 111 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 0 ≤ 𝑥) |
113 | 108, 112 | absidd 15457 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) = 𝑥) |
114 | 113 | oveq2d 7446 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) = (1 / 𝑥)) |
115 | 107, 114 | eqtrd 2774 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · 1)
= (1 / 𝑥)) |
116 | 25, 115 | sylanb 581 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 < 0) → ((1 / (abs‘𝑥)) · 1) = (1 / 𝑥)) |
117 | 98, 116 | ifeqda 4566 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → if(𝑥 < 0, ((1 / (abs‘𝑥)) · -1), ((1 / (abs‘𝑥)) · 1)) = (1 / 𝑥)) |
118 | 75, 117 | eqtrid 2786 |
. . 3
⊢ (𝑥 ∈ 𝐷 → ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1, 1)) = (1 / 𝑥)) |
119 | 118 | mpteq2ia 5250 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1, 1))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
120 | 74, 119 | eqtri 2762 |
1
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |