Step | Hyp | Ref
| Expression |
1 | | reelprrecn 11244 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
3 | | redvabs.d |
. . . . . . . . . . 11
⊢ 𝐷 = (ℝ ∖
{0}) |
4 | 3 | eleq2i 2830 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖
{0})) |
5 | | eldifsn 4790 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℝ ∖ {0})
↔ (𝑥 ∈ ℝ
∧ 𝑥 ≠
0)) |
6 | 4, 5 | bitri 275 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0)) |
7 | 6 | simplbi 497 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ) |
8 | 7 | recnd 11286 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
9 | 8 | sqcld 14180 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
10 | 6 | simprbi 496 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
11 | | sqne0 14159 |
. . . . . . . 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 26626 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘(𝑥↑2)) ∈ ℂ) |
15 | 14 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘(𝑥↑2))
∈ ℂ) |
16 | | ovexd 7465 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((1 /
(𝑥↑2)) · (2
· 𝑥)) ∈
V) |
17 | | cnelprrecn 11245 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
18 | 17 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
19 | | incom 4216 |
. . . . . . . . 9
⊢
(ℝ+ ∩ (-∞(,]0)) = ((-∞(,]0) ∩
ℝ+) |
20 | | dfrp2 13432 |
. . . . . . . . . 10
⊢
ℝ+ = (0(,)+∞) |
21 | 20 | ineq2i 4224 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ ℝ+) = ((-∞(,]0) ∩
(0(,)+∞)) |
22 | | mnfxr 11315 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ -∞ ∈ ℝ*) |
24 | | 0xr 11305 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 0 ∈ ℝ*) |
26 | | pnfxr 11312 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ +∞ ∈ ℝ*) |
28 | 23, 25, 27 | iocioodisjd 42333 |
. . . . . . . . . 10
⊢ (⊤
→ ((-∞(,]0) ∩ (0(,)+∞)) = ∅) |
29 | 28 | mptru 1543 |
. . . . . . . . 9
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
30 | 19, 21, 29 | 3eqtri 2766 |
. . . . . . . 8
⊢
(ℝ+ ∩ (-∞(,]0)) = ∅ |
31 | | disjdif2 4485 |
. . . . . . . 8
⊢
((ℝ+ ∩ (-∞(,]0)) = ∅ →
(ℝ+ ∖ (-∞(,]0)) =
ℝ+) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢
(ℝ+ ∖ (-∞(,]0)) =
ℝ+ |
33 | | rpsscn 42311 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℂ |
34 | | ssdif 4153 |
. . . . . . . 8
⊢
(ℝ+ ⊆ ℂ → (ℝ+ ∖
(-∞(,]0)) ⊆ (ℂ ∖ (-∞(,]0))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . 7
⊢
(ℝ+ ∖ (-∞(,]0)) ⊆ (ℂ ∖
(-∞(,]0)) |
36 | 32, 35 | eqsstrri 4030 |
. . . . . 6
⊢
ℝ+ ⊆ (ℂ ∖
(-∞(,]0)) |
37 | 10 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ≠ 0) |
38 | | sqn0rp 14163 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → (𝑥↑2) ∈
ℝ+) |
39 | 7, 37, 38 | syl2an2 686 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (𝑥↑2) ∈
ℝ+) |
40 | 36, 39 | sselid 3992 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (𝑥↑2) ∈ (ℂ ∖
(-∞(,]0))) |
41 | | ovexd 7465 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (2
· 𝑥) ∈
V) |
42 | | eldifi 4140 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
43 | | eldifn 4141 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
44 | | mnflt0 13164 |
. . . . . . . . . . 11
⊢ -∞
< 0 |
45 | | 0le0 12364 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
46 | | elioc1 13425 |
. . . . . . . . . . . 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 1340 |
. . . . . . . . . 10
⊢ 0 ∈
(-∞(,]0) |
49 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
50 | 48, 49 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
51 | 50 | necon3bi 2964 |
. . . . . . . 8
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
52 | 43, 51 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
53 | 42, 52 | logcld 26626 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) |
54 | 53 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
55 | | ovexd 7465 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
56 | | recn 11242 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
57 | 56 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ) → 𝑥
∈ ℂ) |
58 | 57 | sqcld 14180 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (𝑥↑2) ∈ ℂ) |
59 | | ovexd 7465 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (2 · (𝑥↑(2 − 1))) ∈
V) |
60 | | eqid 2734 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
61 | | cnopn 24822 |
. . . . . . . . 9
⊢ ℂ
∈ (TopOpen‘ℂfld) |
62 | 61 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℂ ∈ (TopOpen‘ℂfld)) |
63 | | ax-resscn 11209 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
64 | | dfss2 3980 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
65 | 63, 64 | mpbi 230 |
. . . . . . . . 9
⊢ (ℝ
∩ ℂ) = ℝ |
66 | 65 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (ℝ ∩ ℂ) = ℝ) |
67 | | sqcl 14154 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
68 | 67 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
69 | | ovexd 7465 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · (𝑥↑(2 − 1))) ∈
V) |
70 | | 2nn 12336 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
71 | | dvexp 26005 |
. . . . . . . . 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 26008 |
. . . . . . 7
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (𝑥↑2))) = (𝑥 ∈ ℝ ↦ (2 · (𝑥↑(2 −
1))))) |
74 | 7 | ssriv 3998 |
. . . . . . . 8
⊢ 𝐷 ⊆
ℝ |
75 | 74 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 𝐷 ⊆
ℝ) |
76 | 60 | tgioo2 24838 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
77 | | rehaus 24834 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Haus |
78 | | 0re 11260 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
79 | | uniretop 24798 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
80 | 79 | sncld 23394 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Haus ∧ 0 ∈ ℝ) → {0}
∈ (Clsd‘(topGen‘ran (,)))) |
81 | 77, 78, 80 | mp2an 692 |
. . . . . . . . . 10
⊢ {0}
∈ (Clsd‘(topGen‘ran (,))) |
82 | 79 | cldopn 23054 |
. . . . . . . . . 10
⊢ ({0}
∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈
(topGen‘ran (,))) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
∖ {0}) ∈ (topGen‘ran (,)) |
84 | 3, 83 | eqeltri 2834 |
. . . . . . . 8
⊢ 𝐷 ∈ (topGen‘ran
(,)) |
85 | 84 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 𝐷 ∈
(topGen‘ran (,))) |
86 | 2, 58, 59, 73, 75, 76, 60, 85 | dvmptres 26015 |
. . . . . 6
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (𝑥↑2))) = (𝑥 ∈ 𝐷 ↦ (2 · (𝑥↑(2 − 1))))) |
87 | | 2m1e1 12389 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
88 | 87 | oveq2i 7441 |
. . . . . . . . 9
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
89 | 8 | exp1d 14177 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (𝑥↑1) = 𝑥) |
90 | 88, 89 | eqtrid 2786 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (𝑥↑(2 − 1)) = 𝑥) |
91 | 90 | oveq2d 7446 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥)) |
92 | 91 | mpteq2ia 5250 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ 𝐷 ↦ (2 · 𝑥)) |
93 | 86, 92 | eqtrdi 2790 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (𝑥↑2))) = (𝑥 ∈ 𝐷 ↦ (2 · 𝑥))) |
94 | | logf1o 26620 |
. . . . . . . . 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 4812 |
. . . . . . . . . 10
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) |
98 | 48, 97 | ax-mp 5 |
. . . . . . . . 9
⊢ {0}
⊆ (-∞(,]0) |
99 | | sscon 4152 |
. . . . . . . . 9
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
100 | 98, 99 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
101 | 96, 100 | feqresmpt 6977 |
. . . . . . 7
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
102 | 101 | oveq2d 7446 |
. . . . . 6
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) |
103 | | eqid 2734 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
104 | 103 | dvlog 26707 |
. . . . . 6
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
105 | 102, 104 | eqtr3di 2789 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
106 | | fveq2 6906 |
. . . . 5
⊢ (𝑦 = (𝑥↑2) → (log‘𝑦) = (log‘(𝑥↑2))) |
107 | | oveq2 7438 |
. . . . 5
⊢ (𝑦 = (𝑥↑2) → (1 / 𝑦) = (1 / (𝑥↑2))) |
108 | 2, 18, 40, 41, 54, 55, 93, 105, 106, 107 | dvmptco 26024 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦ (log‘(𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ ((1 / (𝑥↑2)) · (2 · 𝑥)))) |
109 | | 2cnd 12341 |
. . . 4
⊢ (⊤
→ 2 ∈ ℂ) |
110 | | 2ne0 12367 |
. . . . 5
⊢ 2 ≠
0 |
111 | 110 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ≠ 0) |
112 | 2, 15, 16, 108, 109, 111 | dvmptdivc 26017 |
. . 3
⊢ (⊤
→ (ℝ D (𝑥 ∈
𝐷 ↦
((log‘(𝑥↑2)) /
2))) = (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 ·
𝑥)) / 2))) |
113 | 112 | mptru 1543 |
. 2
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2)) |
114 | 7 | resqcld 14161 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℝ) |
115 | 114, 13 | rereccld 12091 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) ∈ ℝ) |
116 | 115 | recnd 11286 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) ∈ ℂ) |
117 | | 2cnd 12341 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → 2 ∈ ℂ) |
118 | 116, 117,
8 | mul12d 11467 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · (2 · 𝑥)) = (2 · ((1 / (𝑥↑2)) · 𝑥))) |
119 | 118 | oveq1d 7445 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2) = ((2 · ((1 /
(𝑥↑2)) · 𝑥)) / 2)) |
120 | 116, 8 | mulcld 11278 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) ∈ ℂ) |
121 | 110 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 2 ≠ 0) |
122 | 120, 117,
121 | divcan3d 12045 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((2 · ((1 / (𝑥↑2)) · 𝑥)) / 2) = ((1 / (𝑥↑2)) · 𝑥)) |
123 | 8 | sqvald 14179 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) = (𝑥 · 𝑥)) |
124 | 123 | oveq2d 7446 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / (𝑥↑2)) = (1 / (𝑥 · 𝑥))) |
125 | 124 | oveq1d 7445 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) = ((1 / (𝑥 · 𝑥)) · 𝑥)) |
126 | 8, 8, 10, 10 | recdiv2d 12058 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / 𝑥) / 𝑥) = (1 / (𝑥 · 𝑥))) |
127 | 126 | oveq1d 7445 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((1 / 𝑥) / 𝑥) · 𝑥) = ((1 / (𝑥 · 𝑥)) · 𝑥)) |
128 | 8, 10 | reccld 12033 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (1 / 𝑥) ∈ ℂ) |
129 | 128, 8, 10 | divcan1d 12041 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (((1 / 𝑥) / 𝑥) · 𝑥) = (1 / 𝑥)) |
130 | 125, 127,
129 | 3eqtr2d 2780 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((1 / (𝑥↑2)) · 𝑥) = (1 / 𝑥)) |
131 | 119, 122,
130 | 3eqtrd 2778 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2) = (1 / 𝑥)) |
132 | 131 | mpteq2ia 5250 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (((1 / (𝑥↑2)) · (2 · 𝑥)) / 2)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
133 | 113, 132 | eqtri 2762 |
1
⊢ (ℝ
D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |