Definition df-bj-arg 38305

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 38260), 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

Step	Hyp	Ref	Expression
1		carg 38304	. 2 class Arg
2		vx	. . 3 setvar 𝑥
3		cccbar 38276	. . . 4 class ℂ̅
4		cc0 11210	. . . . 5 class 0
5	4	csn 4587	. . . 4 class {0}
6	3, 5	cdif 4047	. . 3 class (ℂ̅ ∖ {0})
7	2	cv 1568	. . . . 5 class 𝑥
8		cc 11208	. . . . 5 class ℂ
9	7, 8	wcel 2146	. . . 4 wff 𝑥 ∈ ℂ
10		clog 26894	. . . . . 6 class log
11	7, 10	cfv 6546	. . . . 5 class (log‘𝑥)
12		cim 15277	. . . . 5 class ℑ
13	11, 12	cfv 6546	. . . 4 class (ℑ‘(log‘𝑥))
14		cltxr 38302	. . . . . 6 class <ℝ̅
15	7, 4, 14	wbr 5105	. . . . 5 wff 𝑥<ℝ̅0
16		cpi 16244	. . . . 5 class π
17		c1st 8006	. . . . . . . 8 class 1st
18	7, 17	cfv 6546	. . . . . . 7 class (1st ‘𝑥)
19		c2 12407	. . . . . . . 8 class 2
20		cmul 11215	. . . . . . . 8 class ·
21	19, 16, 20	co 7427	. . . . . . 7 class (2 · π)
22		cdiv 11983	. . . . . . 7 class /
23	18, 21, 22	co 7427	. . . . . 6 class ((1st ‘𝑥) / (2 · π))
24		cmin 11551	. . . . . 6 class −
25	23, 16, 24	co 7427	. . . . 5 class (((1st ‘𝑥) / (2 · π)) − π)
26	15, 16, 25	cif 4484	. . . 4 class if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))
27	9, 13, 26	cif 4484	. . 3 class if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))
28	2, 6, 27	cmpt 5188	. 2 class (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
29	1, 28	wceq 1569	1 wff Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))

This definition is used by: (None)