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 Unicode 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	-cc CCbar CChat infty infty inftyexpi

**Detailed syntax breakdown of Definition df-bj-oppc**
Step	Hyp	Ref	Expression
1		coppcc 33126	. 2 -cc
2		vx	. . 3
3		cccbar 33102	. . . 4 CCbar
4		ccchat 33119	. . . 4 CChat
5	3, 4	cun 3572	. . 3 CCbar CChat
6	2	cv 1482	. . . . 5
7		cinfty 33117	. . . . 5 infty
8	6, 7	wceq 1483	. . . 4 infty
9		cc 9934	. . . . . 6
10	6, 9	wcel 1990	. . . . 5
11	6	cneg 10267	. . . . 5
12		cc0 9936	. . . . . . . 8
13		c1st 7166	. . . . . . . . 9
14	6, 13	cfv 5888	. . . . . . . 8
15		clt 10074	. . . . . . . 8
16	12, 14, 15	wbr 4653	. . . . . . 7
17		cpi 14797	. . . . . . . 8
18		cmin 10266	. . . . . . . 8
19	14, 17, 18	co 6650	. . . . . . 7
20		caddc 9939	. . . . . . . 8
21	14, 17, 20	co 6650	. . . . . . 7
22	16, 19, 21	cif 4086	. . . . . 6
23		cinftyexpi 33093	. . . . . 6 inftyexpi
24	22, 23	cfv 5888	. . . . 5 inftyexpi
25	10, 11, 24	cif 4086	. . . 4 inftyexpi
26	8, 7, 25	cif 4086	. . 3 infty infty inftyexpi
27	2, 5, 26	cmpt 4729	. 2 CCbar CChat infty infty inftyexpi
28	1, 27	wceq 1483	1 -cc CCbar CChat infty infty inftyexpi

Colors of variables: wff setvar class

This definition is referenced by: (None)

W3C validator