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 32304

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 32303	. 2 class -_ℂ̅
2		vx	. . 3 setvar 𝑥
3		cccbar 32279	. . . 4 class ℂ̅
4		ccchat 32296	. . . 4 class ℂ̂
5	3, 4	cun 3538	. . 3 class (ℂ̅ ∪ ℂ̂)
6	2	cv 1474	. . . . 5 class 𝑥
7		cinfty 32294	. . . . 5 class ∞
8	6, 7	wceq 1475	. . . 4 wff 𝑥 = ∞
9		cc 9813	. . . . . 6 class ℂ
10	6, 9	wcel 1977	. . . . 5 wff 𝑥 ∈ ℂ
11	6	cneg 10146	. . . . 5 class -𝑥
12		cc0 9815	. . . . . . . 8 class 0
13		c1st 7057	. . . . . . . . 9 class 1^st
14	6, 13	cfv 5804	. . . . . . . 8 class (1^st ‘𝑥)
15		clt 9953	. . . . . . . 8 class <
16	12, 14, 15	wbr 4583	. . . . . . 7 wff 0 < (1^st ‘𝑥)
17		cpi 14636	. . . . . . . 8 class π
18		cmin 10145	. . . . . . . 8 class −
19	14, 17, 18	co 6549	. . . . . . 7 class ((1^st ‘𝑥) − π)
20		caddc 9818	. . . . . . . 8 class +
21	14, 17, 20	co 6549	. . . . . . 7 class ((1^st ‘𝑥) + π)
22	16, 19, 21	cif 4036	. . . . . 6 class if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))
23		cinftyexpi 32270	. . . . . 6 class inftyexpi
24	22, 23	cfv 5804	. . . . 5 class (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π)))
25	10, 11, 24	cif 4036	. . . 4 class if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))
26	8, 7, 25	cif 4036	. . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π)))))
27	2, 5, 26	cmpt 4643	. 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1^st ‘𝑥), ((1^st ‘𝑥) − π), ((1^st ‘𝑥) + π))))))
28	1, 27	wceq 1475	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