Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-arg Structured version   Visualization version   GIF version

Definition df-bj-arg 37187
Description: Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses values in [0, 2π) but the present convention simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) The "else" case of the second conditional operator, corresponding to infinite extended complex numbers other than -∞, gives a definition depending on the specific definition chosen for these numbers (df-bj-inftyexpitau 37142), and therefore should not be relied upon. (New usage is discouraged.)
Assertion
Ref Expression
df-bj-arg Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st𝑥) / (2 · π)) − π))))

Detailed syntax breakdown of Definition df-bj-arg
StepHypRef Expression
1 carg 37186 . 2 class Arg
2 vx . . 3 setvar 𝑥
3 cccbar 37158 . . . 4 class ℂ̅
4 cc0 11146 . . . . 5 class 0
54csn 4630 . . . 4 class {0}
63, 5cdif 3960 . . 3 class (ℂ̅ ∖ {0})
72cv 1534 . . . . 5 class 𝑥
8 cc 11144 . . . . 5 class
97, 8wcel 2104 . . . 4 wff 𝑥 ∈ ℂ
10 clog 26592 . . . . . 6 class log
117, 10cfv 6558 . . . . 5 class (log‘𝑥)
12 cim 15123 . . . . 5 class
1311, 12cfv 6558 . . . 4 class (ℑ‘(log‘𝑥))
14 cltxr 37184 . . . . . 6 class <ℝ̅
157, 4, 14wbr 5149 . . . . 5 wff 𝑥<ℝ̅0
16 cpi 16088 . . . . 5 class π
17 c1st 8005 . . . . . . . 8 class 1st
187, 17cfv 6558 . . . . . . 7 class (1st𝑥)
19 c2 12312 . . . . . . . 8 class 2
20 cmul 11151 . . . . . . . 8 class ·
2119, 16, 20co 7425 . . . . . . 7 class (2 · π)
22 cdiv 11911 . . . . . . 7 class /
2318, 21, 22co 7425 . . . . . 6 class ((1st𝑥) / (2 · π))
24 cmin 11483 . . . . . 6 class
2523, 16, 24co 7425 . . . . 5 class (((1st𝑥) / (2 · π)) − π)
2615, 16, 25cif 4530 . . . 4 class if(𝑥<ℝ̅0, π, (((1st𝑥) / (2 · π)) − π))
279, 13, 26cif 4530 . . 3 class if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st𝑥) / (2 · π)) − π)))
282, 6, 27cmpt 5232 . 2 class (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st𝑥) / (2 · π)) − π))))
291, 28wceq 1535 1 wff Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st𝑥) / (2 · π)) − π))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator