Step | Hyp | Ref
| Expression |
1 | | carg 36119 |
. 2
class
Arg |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cccbar 36091 |
. . . 4
class
ℂ̅ |
4 | | cc0 11109 |
. . . . 5
class
0 |
5 | 4 | csn 4628 |
. . . 4
class
{0} |
6 | 3, 5 | cdif 3945 |
. . 3
class
(ℂ̅ ∖ {0}) |
7 | 2 | cv 1540 |
. . . . 5
class 𝑥 |
8 | | cc 11107 |
. . . . 5
class
ℂ |
9 | 7, 8 | wcel 2106 |
. . . 4
wff 𝑥 ∈ ℂ |
10 | | clog 26062 |
. . . . . 6
class
log |
11 | 7, 10 | cfv 6543 |
. . . . 5
class
(log‘𝑥) |
12 | | cim 15044 |
. . . . 5
class
ℑ |
13 | 11, 12 | cfv 6543 |
. . . 4
class
(ℑ‘(log‘𝑥)) |
14 | | cltxr 36117 |
. . . . . 6
class
<ℝ̅ |
15 | 7, 4, 14 | wbr 5148 |
. . . . 5
wff 𝑥<ℝ̅0 |
16 | | cpi 16009 |
. . . . 5
class
π |
17 | | c1st 7972 |
. . . . . . . 8
class
1st |
18 | 7, 17 | cfv 6543 |
. . . . . . 7
class
(1st ‘𝑥) |
19 | | c2 12266 |
. . . . . . . 8
class
2 |
20 | | cmul 11114 |
. . . . . . . 8
class
· |
21 | 19, 16, 20 | co 7408 |
. . . . . . 7
class (2
· π) |
22 | | cdiv 11870 |
. . . . . . 7
class
/ |
23 | 18, 21, 22 | co 7408 |
. . . . . 6
class
((1st ‘𝑥) / (2 · π)) |
24 | | cmin 11443 |
. . . . . 6
class
− |
25 | 23, 16, 24 | co 7408 |
. . . . 5
class
(((1st ‘𝑥) / (2 · π)) −
π) |
26 | 15, 16, 25 | cif 4528 |
. . . 4
class if(𝑥<ℝ̅0,
π, (((1st ‘𝑥) / (2 · π)) −
π)) |
27 | 9, 13, 26 | cif 4528 |
. . 3
class if(𝑥 ∈ ℂ,
(ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π))) |
28 | 2, 6, 27 | cmpt 5231 |
. 2
class (𝑥 ∈ (ℂ̅ ∖
{0}) ↦ if(𝑥 ∈
ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π)))) |
29 | 1, 28 | wceq 1541 |
1
wff Arg =
(𝑥 ∈ (ℂ̅
∖ {0}) ↦ if(𝑥
∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π)))) |