df-bj-oppc - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-oppc		Structured version Visualization version GIF version

Definition df-bj-oppc 33127

Description: Define the negation (operation givin the opposite) the set of extended complex numbers and the complex projective line (Riemann sphere). One could use the prcpal function in the infinite case, but we want to use only basic functions at this point. (Contributed by BJ, 22-Jun-2019.)

**Assertion**
Ref	Expression
df-bj-oppc	⊢ -_ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))))

**Detailed syntax breakdown of Definition df-bj-oppc**
Step	Hyp	Ref	Expression
1		coppcc 33126	. 2 class -_ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 33102	. . . 4 class ℂ̅
4		ccchat 33119	. . . 4 class ℂ̂
5	3, 4	cun 3572	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1482	. . . . 5 class 𝑥
7		cinfty 33117	. . . . 5 class ∞
8	6, 7	wceq 1483	. . . 4 wff 𝑥 = ∞
9		cc 9934	. . . . . 6 class ℂ
10	6, 9	wcel 1990	. . . . 5 wff 𝑥 ∈ ℂ
11	6	cneg 10267	. . . . 5 class -𝑥
12		cc0 9936	. . . . . . . 8 class 0
13		c1st 7166	. . . . . . . . 9 class 1^st
14	6, 13	cfv 5888	. . . . . . . 8 class (1^st ‘𝑥)
15		clt 10074	. . . . . . . 8 class <
16	12, 14, 15	wbr 4653	. . . . . . 7 wff 0 < (1^st ‘𝑥)
17		cpi 14797	. . . . . . . 8 class π
18		cmin 10266	. . . . . . . 8 class −
19	14, 17, 18	co 6650	. . . . . . 7 class ((1^st ‘𝑥) − π)
20		caddc 9939	. . . . . . . 8 class +
21	14, 17, 20	co 6650	. . . . . . 7 class ((1^st ‘𝑥) + π)
22	16, 19, 21	cif 4086	. . . . . 6 class if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))
23		cinftyexpi 33093	. . . . . 6 class inftyexpi
24	22, 23	cfv 5888	. . . . 5 class (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π)))
25	10, 11, 24	cif 4086	. . . 4 class if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))
26	8, 7, 25	cif 4086	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π)))))
27	2, 5, 26	cmpt 4729	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))))
28	1, 27	wceq 1483	1 wff -_ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))))

Colors of variables: wff setvar class

This definition is referenced by: (None)

W3C validator