Users' Mathboxes 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 32100
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 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π))))))

Detailed syntax breakdown of Definition df-bj-oppc
StepHypRef Expression
1 coppcc 32099 . 2 class -ℂ̅
2 vx . . 3 setvar 𝑥
3 cccbar 32075 . . . 4 class ℂ̅
4 ccchat 32092 . . . 4 class ℂ̂
53, 4cun 3537 . . 3 class (ℂ̅ ∪ ℂ̂)
62cv 1473 . . . . 5 class 𝑥
7 cinfty 32090 . . . . 5 class
86, 7wceq 1474 . . . 4 wff 𝑥 = ∞
9 cc 9790 . . . . . 6 class
106, 9wcel 1976 . . . . 5 wff 𝑥 ∈ ℂ
116cneg 10118 . . . . 5 class -𝑥
12 cc0 9792 . . . . . . . 8 class 0
13 c1st 7034 . . . . . . . . 9 class 1st
146, 13cfv 5790 . . . . . . . 8 class (1st𝑥)
15 clt 9930 . . . . . . . 8 class <
1612, 14, 15wbr 4577 . . . . . . 7 wff 0 < (1st𝑥)
17 cpi 14582 . . . . . . . 8 class π
18 cmin 10117 . . . . . . . 8 class
1914, 17, 18co 6527 . . . . . . 7 class ((1st𝑥) − π)
20 caddc 9795 . . . . . . . 8 class +
2114, 17, 20co 6527 . . . . . . 7 class ((1st𝑥) + π)
2216, 19, 21cif 4035 . . . . . 6 class if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π))
23 cinftyexpi 32066 . . . . . 6 class inftyexpi
2422, 23cfv 5790 . . . . 5 class (inftyexpi ‘if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π)))
2510, 11, 24cif 4035 . . . 4 class if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π))))
268, 7, 25cif 4035 . . 3 class if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π)))))
272, 5, 26cmpt 4637 . 2 class (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π))))))
281, 27wceq 1474 1 wff -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st𝑥), ((1st𝑥) − π), ((1st𝑥) + π))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator