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 = ( 𝑥 ∈ ( ℂ̅ ∖ { 0 } ) ↦ if ( 𝑥 ∈ ℂ , ( ℑ ‘ ( log ‘ 𝑥 ) ) , if ( 𝑥 <ℝ̅ 0 , π , ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carg	⊢ Arg
1		vx	⊢ 𝑥
2		cccbar	⊢ ℂ̅
3		cc0	⊢ 0
4	3	csn	⊢ { 0 }
5	2 4	cdif	⊢ ( ℂ̅ ∖ { 0 } )
6	1	cv	⊢ 𝑥
7		cc	⊢ ℂ
8	6 7	wcel	⊢ 𝑥 ∈ ℂ
9		cim	⊢ ℑ
10		clog	⊢ log
11	6 10	cfv	⊢ ( log ‘ 𝑥 )
12	11 9	cfv	⊢ ( ℑ ‘ ( log ‘ 𝑥 ) )
13		cltxr	⊢ <ℝ̅
14	6 3 13	wbr	⊢ 𝑥 <ℝ̅ 0
15		cpi	⊢ π
16		c1st	⊢ 1st
17	6 16	cfv	⊢ ( 1st ‘ 𝑥 )
18		cdiv	⊢ /
19		c2	⊢ 2
20		cmul	⊢ ·
21	19 15 20	co	⊢ ( 2 · π )
22	17 21 18	co	⊢ ( ( 1st ‘ 𝑥 ) / ( 2 · π ) )
23		cmin	⊢ −
24	22 15 23	co	⊢ ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π )
25	14 15 24	cif	⊢ if ( 𝑥 <ℝ̅ 0 , π , ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π ) )
26	8 12 25	cif	⊢ if ( 𝑥 ∈ ℂ , ( ℑ ‘ ( log ‘ 𝑥 ) ) , if ( 𝑥 <ℝ̅ 0 , π , ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π ) ) )
27	1 5 26	cmpt	⊢ ( 𝑥 ∈ ( ℂ̅ ∖ { 0 } ) ↦ if ( 𝑥 ∈ ℂ , ( ℑ ‘ ( log ‘ 𝑥 ) ) , if ( 𝑥 <ℝ̅ 0 , π , ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π ) ) ) )
28	0 27	wceq	⊢ Arg = ( 𝑥 ∈ ( ℂ̅ ∖ { 0 } ) ↦ if ( 𝑥 ∈ ℂ , ( ℑ ‘ ( log ‘ 𝑥 ) ) , if ( 𝑥 <ℝ̅ 0 , π , ( ( ( 1st ‘ 𝑥 ) / ( 2 · π ) ) − π ) ) ) )