Definition df-bj-arg 32308

Description: Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses [0, 2π) 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 = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥)))

Detailed syntax breakdown of Definition df-bj-arg

Step	Hyp	Ref	Expression
1		carg 32307	. 2 class Arg
2		vx	. . 3 setvar 𝑥
3		cccbar 32279	. . . 4 class ℂ̅
4		cc0 9815	. . . . 5 class 0
5	4	csn 4125	. . . 4 class {0}
6	3, 5	cdif 3537	. . 3 class (ℂ̅ ∖ {0})
7	2	cv 1474	. . . . 5 class 𝑥
8		cc 9813	. . . . 5 class ℂ
9	7, 8	wcel 1977	. . . 4 wff 𝑥 ∈ ℂ
10		clog 24105	. . . . . 6 class log
11	7, 10	cfv 5804	. . . . 5 class (log‘𝑥)
12		cim 13686	. . . . 5 class ℑ
13	11, 12	cfv 5804	. . . 4 class (ℑ‘(log‘𝑥))
14		c1st 7057	. . . . 5 class 1st
15	7, 14	cfv 5804	. . . 4 class (1st ‘𝑥)
16	9, 13, 15	cif 4036	. . 3 class if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥))
17	2, 6, 16	cmpt 4643	. 2 class (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥)))
18	1, 17	wceq 1475	1 wff Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥)))

This definition is referenced by: (None)