Metamath Proof Explorer

Definition df-bj-arg

Description: Define the argument of a nonzero extended complex number. By convention, it has values in ( -upi , pi ] . Another convention chooses values in [ 0 , 2 _pi ) 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 minfty , gives a definition depending on the specific definition chosen for these numbers ( df-bj-inftyexpitau ), and therefore should not be relied upon. (New usage is discouraged.)

Ref Expression
Assertion df-bj-arg ⊢ Arg = x ∈ ℂ ‾ ∖ 0 ⟼ if x ∈ ℂ ℑ ⁡ log ⁡ x if x < R 0 π 1 st ⁡ x 2 ⁢ π − π

Detailed syntax breakdown

Step Hyp Ref Expression
0 carg class Arg
1 vx setvar x
2 cccbar class ℂ ‾
3 cc0 class 0
4 3 csn class 0
5 2 4 cdif class ℂ ‾ ∖ 0
6 1 cv setvar x
7 cc class ℂ
8 6 7 wcel wff x ∈ ℂ
9 cim class ℑ
10 clog class log
11 6 10 cfv class log ⁡ x
12 11 9 cfv class ℑ ⁡ log ⁡ x
13 cltxr class < R
14 6 3 13 wbr wff x < R 0
15 cpi class π
16 c1st class 1 st
17 6 16 cfv class 1 st ⁡ x
18 cdiv class ÷
19 c2 class 2
20 cmul class ×
21 19 15 20 co class 2 ⁢ π
22 17 21 18 co class 1 st ⁡ x 2 ⁢ π
23 cmin class −
24 22 15 23 co class 1 st ⁡ x 2 ⁢ π − π
25 14 15 24 cif class if x < R 0 π 1 st ⁡ x 2 ⁢ π − π
26 8 12 25 cif class if x ∈ ℂ ℑ ⁡ log ⁡ x if x < R 0 π 1 st ⁡ x 2 ⁢ π − π
27 1 5 26 cmpt class x ∈ ℂ ‾ ∖ 0 ⟼ if x ∈ ℂ ℑ ⁡ log ⁡ x if x < R 0 π 1 st ⁡ x 2 ⁢ π − π
28 0 27 wceq wff Arg = x ∈ ℂ ‾ ∖ 0 ⟼ if x ∈ ℂ ℑ ⁡ log ⁡ x if x < R 0 π 1 st ⁡ x 2 ⁢ π − π