| Step | Hyp | Ref
| Expression |
| 1 | | reelprrecn 11247 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
| 3 | | redvabs.d |
. . . . . . . . . . 11
⊢ 𝐷 = (ℝ ∖
{0}) |
| 4 | 3 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖
{0})) |
| 5 | | eldifsn 4786 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ {0})
↔ (𝑥 ∈ ℝ
∧ 𝑥 ≠
0)) |
| 6 | 4, 5 | bitri 275 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0)) |
| 7 | 6 | simplbi 497 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ) |
| 8 | 7 | recnd 11289 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
| 9 | 8 | sqcld 14184 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
| 10 | 6 | simprbi 496 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
| 11 | | sqne0 14163 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) ≠ 0 ↔ 𝑥 ≠ 0)) |
| 12 | 8, 11 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((𝑥↑2) ≠ 0 ↔ 𝑥 ≠ 0)) |
| 13 | 10, 12 | mpbird 257 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ≠ 0) |
| 14 | 9, 13 | logcld 26612 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘(𝑥↑2)) ∈ ℂ) |
| 15 | 14 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘(𝑥↑2))
∈ ℂ) |
| 16 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((1 /
(𝑥↑2)) · (2
· 𝑥)) ∈
V) |
| 17 | | cnelprrecn 11248 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 19 | | incom 4209 |
. . . . . . . . 9
⊢
(ℝ+ ∩ (-∞(,]0)) = ((-∞(,]0) ∩
ℝ+) |
| 20 | | dfrp2 13436 |
. . . . . . . . . 10
⊢
ℝ+ = (0(,)+∞) |
| 21 | 20 | ineq2i 4217 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ ℝ+) = ((-∞(,]0) ∩
(0(,)+∞)) |
| 22 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ -∞ ∈ ℝ*) |
| 24 | | 0xr 11308 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
| 25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 0 ∈ ℝ*) |
| 26 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ +∞ ∈ ℝ*) |
| 28 | 23, 25, 27 | iocioodisjd 42355 |
. . . . . . . . . 10
⊢ (⊤
→ ((-∞(,]0) ∩ (0(,)+∞)) = ∅) |
| 29 | 28 | mptru 1547 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
| 30 | 19, 21, 29 | 3eqtri 2769 |
. . . . . . . 8
⊢
(ℝ+ ∩ (-∞(,]0)) = ∅ |
| 31 | | disjdif2 4480 |
. . . . . . . 8
⊢
((ℝ+ ∩ (-∞(,]0)) = ∅ →
(ℝ+ ∖ (-∞(,]0)) =
ℝ+) |
| 32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢
(ℝ+ ∖ (-∞(,]0)) =
ℝ+ |
| 33 | | rpsscn 42333 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℂ |
| 34 | | ssdif 4144 |
. . . . . . . 8
⊢
(ℝ+ ⊆ ℂ → (ℝ+ ∖
(-∞(,]0)) ⊆ (ℂ ∖ (-∞(,]0))) |
| 35 | 33, 34 | ax-mp 5 |
. . . . . . 7
⊢
(ℝ+ ∖ (-∞(,]0)) ⊆ (ℂ ∖
(-∞(,]0)) |
| 36 | 32, 35 | eqsstrri 4031 |
. . . . . 6
⊢
ℝ+ ⊆ (ℂ ∖
(-∞(,]0)) |
| 37 | 10 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ≠ 0) |
| 38 | | sqn0rp 14167 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → (𝑥↑2) ∈
ℝ+) |
| 39 | 7, 37, 38 | syl2an2 686 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (𝑥↑2) ∈
ℝ+) |
| 40 | 36, 39 | sselid 3981 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (𝑥↑2) ∈ (ℂ ∖
(-∞(,]0))) |
| 41 | | ovexd 7466 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (2
· 𝑥) ∈
V) |
| 42 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
| 43 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
| 44 | | mnflt0 13167 |
. . . . . . . . . . 11
⊢ -∞
< 0 |
| 45 | | 0le0 12367 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
| 46 | | elioc1 13429 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (0 ∈ (-∞(,]0) ↔ (0 ∈
ℝ* ∧ -∞ < 0 ∧ 0 ≤ 0))) |
| 47 | 22, 24, 46 | mp2an 692 |
. . . . . . . . . . 11
⊢ (0 ∈
(-∞(,]0) ↔ (0 ∈ ℝ* ∧ -∞ < 0 ∧
0 ≤ 0)) |
| 48 | 24, 44, 45, 47 | mpbir3an 1342 |
. . . . . . . . . 10
⊢ 0 ∈
(-∞(,]0) |
| 49 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
| 50 | 48, 49 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
| 51 | 50 | necon3bi 2967 |
. . . . . . . 8
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
| 52 | 43, 51 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
| 53 | 42, 52 | logcld 26612 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) |
| 54 | 53 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
| 55 | | ovexd 7466 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
| 56 | | recn 11245 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 57 | 56 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ) → 𝑥
∈ ℂ) |
| 58 | 57 | sqcld 14184 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (𝑥↑2) ∈ ℂ) |
| 59 | | ovexd 7466 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (2 · (𝑥↑(2 − 1))) ∈
V) |
| 60 | | eqid 2737 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 61 | | cnopn 24807 |
. . . . . . . . 9
⊢ ℂ
∈ (TopOpen‘ℂfld) |
| 62 | 61 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℂ ∈ (TopOpen‘ℂfld)) |
| 63 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 64 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
| 65 | 63, 64 | mpbi 230 |
. . . . . . . . 9
⊢ (ℝ
∩ ℂ) = ℝ |
| 66 | 65 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (ℝ ∩ ℂ) = ℝ) |
| 67 | | sqcl 14158 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
| 68 | 67 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
| 69 | | ovexd 7466 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · (𝑥↑(2 − 1))) ∈
V) |
| 70 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 71 | | dvexp 25991 |
. . . . . . . . 9
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
| 72 | 70, 71 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
| 73 | 60, 2, 62, 66, 68, 69, 72 | dvmptres3 25994 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (𝑥↑2))) = (𝑥 ∈ ℝ ↦ (2 · (𝑥↑(2 −
1))))) |
| 74 | 7 | ssriv 3987 |
. . . . . . . 8
⊢ 𝐷 ⊆
ℝ |
| 75 | 74 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 𝐷 ⊆
ℝ) |
| 76 | | tgioo4 24826 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 77 | | rehaus 24820 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Haus |
| 78 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 79 | | uniretop 24783 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 80 | 79 | sncld 23379 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Haus ∧ 0 ∈ ℝ) → {0}
∈ (Clsd‘(topGen‘ran (,)))) |
| 81 | 77, 78, 80 | mp2an 692 |
. . . . . . . . . 10
⊢ {0}
∈ (Clsd‘(topGen‘ran (,))) |
| 82 | 79 | cldopn 23039 |
. . . . . . . . . 10
⊢ ({0}
∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈
(topGen‘ran (,))) |
| 83 | 81, 82 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
∖ {0}) ∈ (topGen‘ran (,)) |
| 84 | 3, 83 | eqeltri 2837 |
. . . . . . . 8
⊢ 𝐷 ∈ (topGen‘ran
(,)) |
| 85 | 84 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 𝐷 ∈
(topGen‘ran (,))) |
| 86 | 2, 58, 59, 73, 75, 76, 60, 85 | dvmptres 26001 |
. . . . . 6
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (𝑥↑2))) = (𝑥 ∈ 𝐷 ↦ (2 · (𝑥↑(2 − 1))))) |
| 87 | | 2m1e1 12392 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
| 88 | 87 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
| 89 | 8 | exp1d 14181 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (𝑥↑1) = 𝑥) |
| 90 | 88, 89 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (𝑥↑(2 − 1)) = 𝑥) |
| 91 | 90 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥)) |
| 92 | 91 | mpteq2ia 5245 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ 𝐷 ↦ (2 · 𝑥)) |
| 93 | 86, 92 | eqtrdi 2793 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (𝑥↑2))) = (𝑥 ∈ 𝐷 ↦ (2 · 𝑥))) |
| 94 | | logf1o 26606 |
. . . . . . . . 9
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 95 | | f1of 6848 |
. . . . . . . . 9
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
| 96 | 94, 95 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
| 97 | | snssi 4808 |
. . . . . . . . . 10
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) |
| 98 | 48, 97 | ax-mp 5 |
. . . . . . . . 9
⊢ {0}
⊆ (-∞(,]0) |
| 99 | | sscon 4143 |
. . . . . . . . 9
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
| 100 | 98, 99 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
| 101 | 96, 100 | feqresmpt 6978 |
. . . . . . 7
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
| 102 | 101 | oveq2d 7447 |
. . . . . 6
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) |
| 103 | | eqid 2737 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
| 104 | 103 | dvlog 26693 |
. . . . . 6
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
| 105 | 102, 104 | eqtr3di 2792 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
| 106 | | fveq2 6906 |
. . . . 5
⊢ (𝑦 = (𝑥↑2) → (log‘𝑦) = (log‘(𝑥↑2))) |
| 107 | | oveq2 7439 |
. . . . 5
⊢ (𝑦 = (𝑥↑2) → (1 / 𝑦) = (1 / (𝑥↑2))) |
| 108 | 2, 18, 40, 41, 54, 55, 93, 105, 106, 107 | dvmptco 26010 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (log‘(𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ ((1 / (𝑥↑2)) · (2 · 𝑥)))) |
| 109 | | 2cnd 12344 |
. . . 4
⊢ (⊤
→ 2 ∈ ℂ) |
| 110 | | 2ne0 12370 |
. . . . 5
⊢ 2 ≠
0 |
| 111 | 110 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ≠ 0) |
| 112 | 2, 15, 16, 108, 109, 111 | dvmptdivc 26003 |
. . 3
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦
((log‘(𝑥↑2)) /
2))) = (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 ·
𝑥)) / 2))) |
| 113 | 112 | mptru 1547 |
. 2
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2)) |
| 114 | 7 | resqcld 14165 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℝ) |
| 115 | 114, 13 | rereccld 12094 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) ∈ ℝ) |
| 116 | 115 | recnd 11289 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) ∈ ℂ) |
| 117 | | 2cnd 12344 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 2 ∈ ℂ) |
| 118 | 116, 117,
8 | mul12d 11470 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · (2 · 𝑥)) = (2 · ((1 / (𝑥↑2)) · 𝑥))) |
| 119 | 118 | oveq1d 7446 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2) = ((2 · ((1 /
(𝑥↑2)) · 𝑥)) / 2)) |
| 120 | 116, 8 | mulcld 11281 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) ∈ ℂ) |
| 121 | 110 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 2 ≠ 0) |
| 122 | 120, 117,
121 | divcan3d 12048 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((2 · ((1 / (𝑥↑2)) · 𝑥)) / 2) = ((1 / (𝑥↑2)) · 𝑥)) |
| 123 | 8 | sqvald 14183 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) = (𝑥 · 𝑥)) |
| 124 | 123 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) = (1 / (𝑥 · 𝑥))) |
| 125 | 124 | oveq1d 7446 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) = ((1 / (𝑥 · 𝑥)) · 𝑥)) |
| 126 | 8, 8, 10, 10 | recdiv2d 12061 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / 𝑥) / 𝑥) = (1 / (𝑥 · 𝑥))) |
| 127 | 126 | oveq1d 7446 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((1 / 𝑥) / 𝑥) · 𝑥) = ((1 / (𝑥 · 𝑥)) · 𝑥)) |
| 128 | 8, 10 | reccld 12036 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / 𝑥) ∈ ℂ) |
| 129 | 128, 8, 10 | divcan1d 12044 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((1 / 𝑥) / 𝑥) · 𝑥) = (1 / 𝑥)) |
| 130 | 125, 127,
129 | 3eqtr2d 2783 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) = (1 / 𝑥)) |
| 131 | 119, 122,
130 | 3eqtrd 2781 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2) = (1 / 𝑥)) |
| 132 | 131 | mpteq2ia 5245 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
| 133 | 113, 132 | eqtri 2765 |
1
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |