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	$$⊢\mathrm{Arg}=\left(x\in \left(\overline{ℂ}\setminus \left\{0\right\}\right)⟼if\left(x\in ℂ,\Im \left(\log x\right),if\left(x{<}_{R}0,\mathrm{\pi },\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carg	$$class\mathrm{Arg}$$
1		vx	$$setvarx$$
2		cccbar	$$class\overline{ℂ}$$
3		cc0	$$class0$$
4	3	csn	$$class\left\{0\right\}$$
5	2 4	cdif	$$class\left(\overline{ℂ}\setminus \left\{0\right\}\right)$$
6	1	cv	$$setvarx$$
7		cc	$$classℂ$$
8	6 7	wcel	$$wffx\in ℂ$$
9		cim	$$class\Im$$
10		clog	$$classlog$$
11	6 10	cfv	$$class\log x$$
12	11 9	cfv	$$class\Im \left(\log x\right)$$
13		cltxr	$$class{<}_R$$
14	6 3 13	wbr	$$wffx{<}_{R}0$$
15		cpi	$$class\mathrm{\pi }$$
16		c1st	$$class{1}^{st}$$
17	6 16	cfv	$$class{1}^{st}\left(x\right)$$
18		cdiv	$$class÷$$
19		c2	$$class2$$
20		cmul	$$class\times$$
21	19 15 20	co	$$class2\mathrm{\pi }$$
22	17 21 18	co	$$class\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)$$
23		cmin	$$class-$$
24	22 15 23	co	$$class\left(\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)$$
25	14 15 24	cif	$$classif\left(x{<}_{R}0,\mathrm{\pi },\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)$$
26	8 12 25	cif	$$classif\left(x\in ℂ,\Im \left(\log x\right),if\left(x{<}_{R}0,\mathrm{\pi },\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)\right)$$
27	1 5 26	cmpt	$$class\left(x\in \left(\overline{ℂ}\setminus \left\{0\right\}\right)⟼if\left(x\in ℂ,\Im \left(\log x\right),if\left(x{<}_{R}0,\mathrm{\pi },\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)\right)\right)$$
28	0 27	wceq	$$wff\mathrm{Arg}=\left(x\in \left(\overline{ℂ}\setminus \left\{0\right\}\right)⟼if\left(x\in ℂ,\Im \left(\log x\right),if\left(x{<}_{R}0,\mathrm{\pi },\left(\frac{1^{st}\left(x\right)}{2\mathrm{\pi }}\right)-\mathrm{\pi }\right)\right)\right)$$