| Step | Hyp | Ref
| Expression |
| 1 | | reelprrecn 11247 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
| 3 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 5 | | dfrp2 13436 |
. . . . . . 7
⊢
ℝ+ = (0(,)+∞) |
| 6 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ -∞ ∈ ℝ*) |
| 8 | | 0xr 11308 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
| 9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 0 ∈ ℝ*) |
| 10 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ +∞ ∈ ℝ*) |
| 12 | 7, 9, 11 | iocioodisjd 42355 |
. . . . . . . . . 10
⊢ (⊤
→ ((-∞(,]0) ∩ (0(,)+∞)) = ∅) |
| 13 | 12 | mptru 1547 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
| 14 | 13 | ineqcomi 4211 |
. . . . . . . 8
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ |
| 15 | | disjdif2 4480 |
. . . . . . . 8
⊢
(((0(,)+∞) ∩ (-∞(,]0)) = ∅ → ((0(,)+∞)
∖ (-∞(,]0)) = (0(,)+∞)) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . . 7
⊢
((0(,)+∞) ∖ (-∞(,]0)) =
(0(,)+∞) |
| 17 | 5, 16 | eqtr4i 2768 |
. . . . . 6
⊢
ℝ+ = ((0(,)+∞) ∖
(-∞(,]0)) |
| 18 | | ioosscn 13449 |
. . . . . . 7
⊢
(0(,)+∞) ⊆ ℂ |
| 19 | | ssdif 4144 |
. . . . . . 7
⊢
((0(,)+∞) ⊆ ℂ → ((0(,)+∞) ∖
(-∞(,]0)) ⊆ (ℂ ∖ (-∞(,]0))) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢
((0(,)+∞) ∖ (-∞(,]0)) ⊆ (ℂ ∖
(-∞(,]0)) |
| 21 | 17, 20 | eqsstri 4030 |
. . . . 5
⊢
ℝ+ ⊆ (ℂ ∖
(-∞(,]0)) |
| 22 | | redvabs.d |
. . . . . . . . . . 11
⊢ 𝐷 = (ℝ ∖
{0}) |
| 23 | 22 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖
{0})) |
| 24 | | eldifsn 4786 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ {0})
↔ (𝑥 ∈ ℝ
∧ 𝑥 ≠
0)) |
| 25 | 23, 24 | bitri 275 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0)) |
| 26 | 25 | simplbi 497 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ) |
| 27 | 26 | recnd 11289 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
| 28 | 27 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) |
| 29 | 25 | simprbi 496 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
| 30 | 29 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ≠ 0) |
| 31 | 28, 30 | absrpcld 15487 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(abs‘𝑥) ∈
ℝ+) |
| 32 | 21, 31 | sselid 3981 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(abs‘𝑥) ∈
(ℂ ∖ (-∞(,]0))) |
| 33 | | negex 11506 |
. . . . . 6
⊢ -1 ∈
V |
| 34 | | 1ex 11257 |
. . . . . 6
⊢ 1 ∈
V |
| 35 | 33, 34 | ifex 4576 |
. . . . 5
⊢ if(𝑥 < 0, -1, 1) ∈
V |
| 36 | 35 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → if(𝑥 < 0, -1, 1) ∈
V) |
| 37 | | eldifi 4131 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
| 38 | 37 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ∈ ℂ) |
| 39 | | eldifn 4132 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
| 40 | | mnflt0 13167 |
. . . . . . . . . 10
⊢ -∞
< 0 |
| 41 | | ubioc1 13440 |
. . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) |
| 42 | 6, 8, 40, 41 | mp3an 1463 |
. . . . . . . . 9
⊢ 0 ∈
(-∞(,]0) |
| 43 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
| 44 | 42, 43 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
| 45 | 44 | necon3bi 2967 |
. . . . . . 7
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
| 46 | 39, 45 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
| 47 | 46 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → 𝑦 ≠ 0) |
| 48 | 38, 47 | logcld 26612 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
| 49 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
| 50 | 22 | redvmptabs 42390 |
. . . . 5
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1)) |
| 51 | 50 | a1i 11 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))) |
| 52 | | logf1o 26606 |
. . . . . . . . . 10
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 53 | | f1of 6848 |
. . . . . . . . . 10
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
| 54 | 52, 53 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
| 55 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
| 56 | 55 | logdmss 26684 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
| 57 | 56 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
| 58 | 54, 57 | feqresmpt 6978 |
. . . . . . . 8
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
| 59 | 58 | mptru 1547 |
. . . . . . 7
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦)) |
| 60 | 59 | oveq2i 7442 |
. . . . . 6
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦))) |
| 61 | 55 | dvlog 26693 |
. . . . . 6
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
| 62 | 60, 61 | eqtr3i 2767 |
. . . . 5
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
| 63 | 62 | a1i 11 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
| 64 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = (abs‘𝑥) → (log‘𝑦) = (log‘(abs‘𝑥))) |
| 65 | | oveq2 7439 |
. . . 4
⊢ (𝑦 = (abs‘𝑥) → (1 / 𝑦) = (1 / (abs‘𝑥))) |
| 66 | 2, 4, 32, 36, 48, 49, 51, 63, 64, 65 | dvmptco 26010 |
. . 3
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1,
1)))) |
| 67 | 66 | mptru 1547 |
. 2
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1,
1))) |
| 68 | | ovif2 7532 |
. . . 4
⊢ ((1 /
(abs‘𝑥)) ·
if(𝑥 < 0, -1, 1)) =
if(𝑥 < 0, ((1 /
(abs‘𝑥)) ·
-1), ((1 / (abs‘𝑥))
· 1)) |
| 69 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ∈
ℝ) |
| 70 | 69 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ∈
ℂ) |
| 71 | 70 | abscld 15475 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ∈
ℝ) |
| 72 | 71 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ∈
ℂ) |
| 73 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ≠ 0) |
| 74 | 70, 73 | absne0d 15486 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) ≠ 0) |
| 75 | 72, 74 | reccld 12036 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℂ) |
| 76 | | neg1cn 12380 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
| 77 | 76 | a1i 11 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -1 ∈
ℂ) |
| 78 | 75, 77 | mulcomd 11282 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · -1)
= (-1 · (1 / (abs‘𝑥)))) |
| 79 | 75 | mulm1d 11715 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (-1 · (1
/ (abs‘𝑥))) = -(1 /
(abs‘𝑥))) |
| 80 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 1 ∈
ℂ) |
| 81 | 80, 72, 74 | divneg2d 12057 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -(1 /
(abs‘𝑥)) = (1 /
-(abs‘𝑥))) |
| 82 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 0 ∈
ℝ) |
| 83 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 < 0) |
| 84 | 69, 82, 83 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → 𝑥 ≤ 0) |
| 85 | 69, 84 | absnidd 15452 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (abs‘𝑥) = -𝑥) |
| 86 | 85 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -𝑥 = (abs‘𝑥)) |
| 87 | 70, 86 | negcon1ad 11615 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) →
-(abs‘𝑥) = 𝑥) |
| 88 | 87 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → (1 /
-(abs‘𝑥)) = (1 /
𝑥)) |
| 89 | 81, 88 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → -(1 /
(abs‘𝑥)) = (1 / 𝑥)) |
| 90 | 78, 79, 89 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · -1)
= (1 / 𝑥)) |
| 91 | 25, 90 | sylanb 581 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 < 0) → ((1 / (abs‘𝑥)) · -1) = (1 / 𝑥)) |
| 92 | | recn 11245 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 93 | 92 | abscld 15475 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
| 94 | 93 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) ∈
ℝ) |
| 95 | 92 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ∈
ℂ) |
| 96 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ≠ 0) |
| 97 | 95, 96 | absne0d 15486 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) ≠ 0) |
| 98 | 94, 97 | rereccld 12094 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℝ) |
| 99 | 98 | recnd 11289 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) ∈
ℂ) |
| 100 | 99 | mulridd 11278 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · 1)
= (1 / (abs‘𝑥))) |
| 101 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 𝑥 ∈
ℝ) |
| 102 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → 0 ∈
ℝ) |
| 103 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℝ) |
| 104 | 102, 103 | lenltd 11407 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → (0 ≤ 𝑥 ↔ ¬ 𝑥 < 0)) |
| 105 | 104 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → 0 ≤ 𝑥) |
| 106 | 101, 105 | absidd 15461 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (abs‘𝑥) = 𝑥) |
| 107 | 106 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → (1 /
(abs‘𝑥)) = (1 / 𝑥)) |
| 108 | 100, 107 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) → ((1 /
(abs‘𝑥)) · 1)
= (1 / 𝑥)) |
| 109 | 25, 108 | sylanb 581 |
. . . . 5
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 < 0) → ((1 / (abs‘𝑥)) · 1) = (1 / 𝑥)) |
| 110 | 91, 109 | ifeqda 4562 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → if(𝑥 < 0, ((1 / (abs‘𝑥)) · -1), ((1 / (abs‘𝑥)) · 1)) = (1 / 𝑥)) |
| 111 | 68, 110 | eqtrid 2789 |
. . 3
⊢ (𝑥 ∈ 𝐷 → ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1, 1)) = (1 / 𝑥)) |
| 112 | 111 | mpteq2ia 5245 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (abs‘𝑥)) · if(𝑥 < 0, -1, 1))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
| 113 | 67, 112 | eqtri 2765 |
1
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦
(log‘(abs‘𝑥))))
= (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |