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 e. ( CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , if ( x

Detailed syntax breakdown

Step Hyp Ref Expression
0 carg 
 |-  Arg
1 vx 
 |-  x
2 cccbar 
 |-  CCbar
3 cc0 
 |-  0
4 3 csn 
 |-  { 0 }
5 2 4 cdif 
 |-  ( CCbar \ { 0 } )
6 1 cv 
 |-  x
7 cc 
 |-  CC
8 6 7 wcel 
 |-  x e. CC
9 cim 
 |-  Im
10 clog 
 |-  log
11 6 10 cfv 
 |-  ( log ` x )
12 11 9 cfv 
 |-  ( Im ` ( log ` x ) )
13 cltxr 
 |-
14 6 3 13 wbr 
 |-  x
15 cpi 
 |-  _pi
16 c1st 
 |-  1st
17 6 16 cfv 
 |-  ( 1st ` x )
18 cdiv 
 |-  /
19 c2 
 |-  2
20 cmul 
 |-  x.
21 19 15 20 co 
 |-  ( 2 x. _pi )
22 17 21 18 co 
 |-  ( ( 1st ` x ) / ( 2 x. _pi ) )
23 cmin 
 |-  -
24 22 15 23 co 
 |-  ( ( ( 1st ` x ) / ( 2 x. _pi ) ) - _pi )
25 14 15 24 cif 
 |-  if ( x
26 8 12 25 cif 
 |-  if ( x e. CC , ( Im ` ( log ` x ) ) , if ( x
27 1 5 26 cmpt 
 |-  ( x e. ( CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , if ( x
28 0 27 wceq 
 |-  Arg = ( x e. ( CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , if ( x