Definition df-bj-arg 33131

Description: Define the argument of a nonzero extended complex number. By convention, it has values in ( -u pi , pi ]. Another convention chooses [ 0 , 2 pi ) but the present one simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.)

Assertion

Ref	Expression
df-bj-arg	|- Arg = ( x e. (CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) ) )

Detailed syntax breakdown of Definition df-bj-arg

Step	Hyp	Ref	Expression
1		carg 33130	. 2 class Arg
2		vx	. . 3 setvar x
3		cccbar 33102	. . . 4 class CCbar
4		cc0 9936	. . . . 5 class 0
5	4	csn 4177	. . . 4 class { 0 }
6	3, 5	cdif 3571	. . 3 class (CCbar \ { 0 } )
7	2	cv 1482	. . . . 5 class x
8		cc 9934	. . . . 5 class CC
9	7, 8	wcel 1990	. . . 4 wff x e. CC
10		clog 24301	. . . . . 6 class log
11	7, 10	cfv 5888	. . . . 5 class ( log ` x )
12		cim 13838	. . . . 5 class Im
13	11, 12	cfv 5888	. . . 4 class ( Im ` ( log ` x ) )
14		c1st 7166	. . . . 5 class 1st
15	7, 14	cfv 5888	. . . 4 class ( 1st ` x )
16	9, 13, 15	cif 4086	. . 3 class if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) )
17	2, 6, 16	cmpt 4729	. 2 class ( x e. (CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) ) )
18	1, 17	wceq 1483	1 wff Arg = ( x e. (CCbar \ { 0 } ) |-> if ( x e. CC , ( Im ` ( log ` x ) ) , ( 1st ` x ) ) )

This definition is referenced by: (None)