Detailed syntax breakdown of Definition df-bj-arg
| Step | Hyp | Ref
| Expression |
| 1 | | carg 37222 |
. 2
class
Arg |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | cccbar 37194 |
. . . 4
class
ℂ̅ |
| 4 | | cc0 11151 |
. . . . 5
class
0 |
| 5 | 4 | csn 4624 |
. . . 4
class
{0} |
| 6 | 3, 5 | cdif 3947 |
. . 3
class
(ℂ̅ ∖ {0}) |
| 7 | 2 | cv 1539 |
. . . . 5
class 𝑥 |
| 8 | | cc 11149 |
. . . . 5
class
ℂ |
| 9 | 7, 8 | wcel 2108 |
. . . 4
wff 𝑥 ∈ ℂ |
| 10 | | clog 26586 |
. . . . . 6
class
log |
| 11 | 7, 10 | cfv 6559 |
. . . . 5
class
(log‘𝑥) |
| 12 | | cim 15133 |
. . . . 5
class
ℑ |
| 13 | 11, 12 | cfv 6559 |
. . . 4
class
(ℑ‘(log‘𝑥)) |
| 14 | | cltxr 37220 |
. . . . . 6
class
<ℝ̅ |
| 15 | 7, 4, 14 | wbr 5141 |
. . . . 5
wff 𝑥<ℝ̅0 |
| 16 | | cpi 16098 |
. . . . 5
class
π |
| 17 | | c1st 8008 |
. . . . . . . 8
class
1st |
| 18 | 7, 17 | cfv 6559 |
. . . . . . 7
class
(1st ‘𝑥) |
| 19 | | c2 12317 |
. . . . . . . 8
class
2 |
| 20 | | cmul 11156 |
. . . . . . . 8
class
· |
| 21 | 19, 16, 20 | co 7429 |
. . . . . . 7
class (2
· π) |
| 22 | | cdiv 11916 |
. . . . . . 7
class
/ |
| 23 | 18, 21, 22 | co 7429 |
. . . . . 6
class
((1st ‘𝑥) / (2 · π)) |
| 24 | | cmin 11488 |
. . . . . 6
class
− |
| 25 | 23, 16, 24 | co 7429 |
. . . . 5
class
(((1st ‘𝑥) / (2 · π)) −
π) |
| 26 | 15, 16, 25 | cif 4524 |
. . . 4
class if(𝑥<ℝ̅0,
π, (((1st ‘𝑥) / (2 · π)) −
π)) |
| 27 | 9, 13, 26 | cif 4524 |
. . 3
class if(𝑥 ∈ ℂ,
(ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π))) |
| 28 | 2, 6, 27 | cmpt 5223 |
. 2
class (𝑥 ∈ (ℂ̅ ∖
{0}) ↦ if(𝑥 ∈
ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π)))) |
| 29 | 1, 28 | wceq 1540 |
1
wff Arg =
(𝑥 ∈ (ℂ̅
∖ {0}) ↦ if(𝑥
∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π,
(((1st ‘𝑥)
/ (2 · π)) − π)))) |