REAL is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
K99() is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of NAT
{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : ( R19(b1,b2) & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : ( R19(b1,b2) & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : ( R19(b1,b2) & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of omega : verum } ) \/ omega is non empty set
bool K99() is set
bool (bool K99()) is set
DEDEKIND_CUTS is non empty Element of bool (bool K99())
REAL+ is non empty set
COMPLEX is non empty set
K105() is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Element of K99()
K106() is non empty epsilon-transitive epsilon-connected ordinal Element of K99()
{K105()} is non empty set
[:{K105()},REAL+:] is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Element of NAT
{0} is non empty set
[:{0},REAL+:] is set
{{}} is non empty set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is non empty set
[{},{}] is set
{{},{}} is non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is non empty set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is set
{{},1} is non empty set
K78({{},1},REAL) is non empty M4({{},1}, REAL )
{ b1 where b1 is V6() V18({{},1}, REAL ) M5({{},1}, REAL ,K78({{},1},REAL)) : K11(b1,1) = {} } is set
K78({{},1},REAL) \ { b1 where b1 is V6() V18({{},1}, REAL ) M5({{},1}, REAL ,K78({{},1},REAL)) : K11(b1,1) = {} } is Element of bool K78({{},1},REAL)
bool K78({{},1},REAL) is set
(K78({{},1},REAL) \ { b1 where b1 is V6() V18({{},1}, REAL ) M5({{},1}, REAL ,K78({{},1},REAL)) : K11(b1,1) = {} } ) \/ REAL is non empty set
-infty is non empty ext-real non positive negative set
[0,REAL] is set
{0,REAL} is non empty set
{{0,REAL},{0}} is non empty set
+infty is non empty ext-real positive non negative set
z is complex Element of REAL
z is set
z is set
z is set
ExtREAL is non empty set
{+infty,-infty} is non empty set
REAL \/ {+infty,-infty} is non empty set
z is complex ext-real () set
j is complex ext-real () Element of REAL
x1 is complex ext-real () Element of REAL
[*j,x1*] is complex Element of COMPLEX
(0,1) --> (j,x1) is V6() V18({0,1}, REAL ) Element of bool [:{0,1},REAL:]
{0,1} is non empty set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set
z is complex ext-real () set
- z is complex set
z + (- z) is complex set
j is complex ext-real () Element of REAL
x1 is complex ext-real () Element of REAL
[*j,x1*] is complex Element of COMPLEX
x2 is complex ext-real () Element of REAL
y1 is complex ext-real () Element of REAL
[*x2,y1*] is complex Element of COMPLEX
+ (j,x2) is complex ext-real () Element of REAL
+ (x1,y1) is complex ext-real () Element of REAL
[*(+ (j,x2)),(+ (x1,y1))*] is complex Element of COMPLEX
z " is complex set
z * (z ") is complex set
j is complex ext-real () Element of REAL
x1 is complex ext-real () Element of REAL
[*j,x1*] is complex Element of COMPLEX
x2 is complex ext-real () Element of REAL
y1 is complex ext-real () Element of REAL
[*x2,y1*] is complex Element of COMPLEX
* (j,x2) is complex ext-real () Element of REAL
* (x1,y1) is complex ext-real () Element of REAL
opp (* (x1,y1)) is complex ext-real () Element of REAL
+ ((* (j,x2)),(opp (* (x1,y1)))) is complex ext-real () Element of REAL
* (j,y1) is complex ext-real () Element of REAL
* (x1,x2) is complex ext-real () Element of REAL
+ ((* (j,y1)),(* (x1,x2))) is complex ext-real () Element of REAL
[*(+ ((* (j,x2)),(opp (* (x1,y1))))),(+ ((* (j,y1)),(* (x1,x2))))*] is complex Element of COMPLEX
j is complex ext-real () set
z + j is complex set
x1 is complex ext-real () Element of REAL
x2 is complex ext-real () Element of REAL
[*x1,x2*] is complex Element of COMPLEX
y1 is complex ext-real () Element of REAL
y2 is complex ext-real () Element of REAL
[*y1,y2*] is complex Element of COMPLEX
+ (x1,y1) is complex ext-real () Element of REAL
+ (x2,y2) is complex ext-real () Element of REAL
[*(+ (x1,y1)),(+ (x2,y2))*] is complex Element of COMPLEX
z * j is complex set
x1 is complex ext-real () Element of REAL
x2 is complex ext-real () Element of REAL
[*x1,x2*] is complex Element of COMPLEX
y1 is complex ext-real () Element of REAL
y2 is complex ext-real () Element of REAL
[*y1,y2*] is complex Element of COMPLEX
* (x1,y1) is complex ext-real () Element of REAL
* (x2,y2) is complex ext-real () Element of REAL
opp (* (x2,y2)) is complex ext-real () Element of REAL
+ ((* (x1,y1)),(opp (* (x2,y2)))) is complex ext-real () Element of REAL
* (x1,y2) is complex ext-real () Element of REAL
* (x2,y1) is complex ext-real () Element of REAL
+ ((* (x1,y2)),(* (x2,y1))) is complex ext-real () Element of REAL
[*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] is complex Element of COMPLEX
opp x2 is complex ext-real () Element of REAL
* ((opp x2),y2) is complex ext-real () Element of REAL
+ ((* (x1,y1)),0) is complex ext-real () Element of REAL
z is complex ext-real () set
j is complex ext-real () set
z - j is complex set
- j is complex ext-real () set
z + (- j) is complex ext-real () set
z / j is complex set
j " is complex ext-real () set
z * (j ") is complex ext-real () set
z is complex ext-real () set
j is complex ext-real () set
x1 is Element of REAL+
x2 is Element of REAL+
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
y2 is Element of REAL+
[0,y2] is set
{0,y2} is non empty set
{{0,y2},{0}} is non empty set
x1 is Element of REAL+
x2 is Element of REAL+
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
y2 is Element of REAL+
[0,y2] is set
{0,y2} is non empty set
{{0,y2},{0}} is non empty set
x1 is Element of REAL+
x2 is Element of REAL+
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
y2 is Element of REAL+
[0,y2] is set
{0,y2} is non empty set
{{0,y2},{0}} is non empty set
z is complex ext-real () set
j is complex ext-real () set
x1 is Element of REAL+
x2 is Element of REAL+
y1 is Element of REAL+
y2 is Element of REAL+
x1 is Element of REAL+
[0,x1] is set
{0,x1} is non empty set
{{0,x1},{0}} is non empty set
x2 is Element of REAL+
[0,x2] is set
{0,x2} is non empty set
{{0,x2},{0}} is non empty set
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
y2 is Element of REAL+
[0,y2] is set
{0,y2} is non empty set
{{0,y2},{0}} is non empty set
z is complex ext-real () set
j is complex ext-real () set
x1 is complex ext-real () set
z + x1 is complex ext-real () set
j + x1 is complex ext-real () set
y2 is complex ext-real () Element of REAL
o is complex ext-real () Element of REAL
+ (o,y2) is complex ext-real () Element of REAL
r is complex ext-real () set
r + x1 is complex ext-real () set
s is complex ext-real () Element of REAL
t is complex ext-real () Element of REAL
[*s,t*] is complex Element of COMPLEX
x1 is complex ext-real () Element of REAL
y1 is complex ext-real () Element of REAL
[*x1,y1*] is complex Element of COMPLEX
+ (s,x1) is complex ext-real () Element of REAL
+ (t,y1) is complex ext-real () Element of REAL
[*(+ (s,x1)),(+ (t,y1))*] is complex Element of COMPLEX
y1 is complex ext-real () Element of REAL
+ (y1,y2) is complex ext-real () Element of REAL
x2 is complex ext-real () Element of REAL
+ (x2,y2) is complex ext-real () Element of REAL
o is Element of REAL+
r is Element of REAL+
o + r is Element of REAL+
s is Element of REAL+
t is Element of REAL+
s + t is Element of REAL+
x1 is Element of REAL+
y1 is Element of REAL+
o is Element of REAL+
r is Element of REAL+
o + r is Element of REAL+
s is Element of REAL+
[0,s] is set
{0,s} is non empty set
{{0,s},{0}} is non empty set
t is Element of REAL+
t - s is set
t -' s is Element of REAL+
s -' t is Element of REAL+
[0,(s -' t)] is set
{0,(s -' t)} is non empty set
{{0,(s -' t)},{0}} is non empty set
o is Element of REAL+
[0,o] is set
{0,o} is non empty set
{{0,o},{0}} is non empty set
r is Element of REAL+
r - o is set
s is Element of REAL+
[0,s] is set
{0,s} is non empty set
{{0,s},{0}} is non empty set
t is Element of REAL+
[0,t] is set
{0,t} is non empty set
{{0,t},{0}} is non empty set
x1 is Element of REAL+
[0,x1] is set
{0,x1} is non empty set
{{0,x1},{0}} is non empty set
y1 is Element of REAL+
y1 - x1 is set
y1 - o is set
y1 -' o is Element of REAL+
y1 -' x1 is Element of REAL+
r -' o is Element of REAL+
x1 -' y1 is Element of REAL+
[0,(x1 -' y1)] is set
{0,(x1 -' y1)} is non empty set
{{0,(x1 -' y1)},{0}} is non empty set
y1 - o is set
y1 -' o is Element of REAL+
o -' y1 is Element of REAL+
[0,(o -' y1)] is set
{0,(o -' y1)} is non empty set
{{0,(o -' y1)},{0}} is non empty set
o is Element of REAL+
r is Element of REAL+
[0,r] is set
{0,r} is non empty set
{{0,r},{0}} is non empty set
o - r is set
s is Element of REAL+
t is Element of REAL+
[0,t] is set
{0,t} is non empty set
{{0,t},{0}} is non empty set
s - t is set
x1 is Element of REAL+
y1 is Element of REAL+
o - t is set
o -' t is Element of REAL+
s -' t is Element of REAL+
o -' r is Element of REAL+
x1 is Element of REAL+
y1 is Element of REAL+
t -' s is Element of REAL+
[0,(t -' s)] is set
{0,(t -' s)} is non empty set
{{0,(t -' s)},{0}} is non empty set
o - t is set
o -' t is Element of REAL+
t -' o is Element of REAL+
x1 is Element of REAL+
y1 is Element of REAL+
[0,(t -' o)] is set
{0,(t -' o)} is non empty set
{{0,(t -' o)},{0}} is non empty set
o is Element of REAL+
[0,o] is set
{0,o} is non empty set
{{0,o},{0}} is non empty set
r is Element of REAL+
[0,r] is set
{0,r} is non empty set
{{0,r},{0}} is non empty set
o + r is Element of REAL+
[0,(o + r)] is set
{0,(o + r)} is non empty set
{{0,(o + r)},{0}} is non empty set
s is Element of REAL+
t is Element of REAL+
[0,t] is set
{0,t} is non empty set
{{0,t},{0}} is non empty set
s - t is set
s -' t is Element of REAL+
r -' s is Element of REAL+
r + o is Element of REAL+
[0,(r -' s)] is set
{0,(r -' s)} is non empty set
{{0,(r -' s)},{0}} is non empty set
o is Element of REAL+
[0,o] is set
{0,o} is non empty set
{{0,o},{0}} is non empty set
r is Element of REAL+
[0,r] is set
{0,r} is non empty set
{{0,r},{0}} is non empty set
o + r is Element of REAL+
[0,(o + r)] is set
{0,(o + r)} is non empty set
{{0,(o + r)},{0}} is non empty set
s is Element of REAL+
[0,s] is set
{0,s} is non empty set
{{0,s},{0}} is non empty set
t is Element of REAL+
[0,t] is set
{0,t} is non empty set
{{0,t},{0}} is non empty set
s + t is Element of REAL+
[0,(s + t)] is set
{0,(s + t)} is non empty set
{{0,(s + t)},{0}} is non empty set
x1 is Element of REAL+
[0,x1] is set
{0,x1} is non empty set
{{0,x1},{0}} is non empty set
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
o + t is Element of REAL+
s + r is Element of REAL+
z is complex ext-real () set
j is complex ext-real () set
x1 is complex ext-real () set
x2 is Element of REAL+
y1 is Element of REAL+
y2 is Element of REAL+
o is Element of REAL+
x2 is Element of REAL+
[0,x2] is set
{0,x2} is non empty set
{{0,x2},{0}} is non empty set
y1 is Element of REAL+
[0,y1] is set
{0,y1} is non empty set
{{0,y1},{0}} is non empty set
y2 is Element of REAL+
[0,y2] is set
{0,y2} is non empty set
{{0,y2},{0}} is non empty set
o is Element of REAL+
[0,o] is set
{0,o} is non empty set
{{0,o},{0}} is non empty set
z is Element of REAL+
j is Element of REAL+
- 1 is non empty complex ext-real () set
1 + (- 1) is complex ext-real () set
x1 is complex ext-real () Element of REAL
x2 is complex ext-real () Element of REAL
[*x1,x2*] is complex Element of COMPLEX
y1 is complex ext-real () Element of REAL
y2 is complex ext-real () Element of REAL
[*y1,y2*] is complex Element of COMPLEX
+ (x1,y1) is complex ext-real () Element of REAL
+ (x2,y2) is complex ext-real () Element of REAL
[*(+ (x1,y1)),(+ (x2,y2))*] is complex Element of COMPLEX
o is Element of REAL+
r is Element of REAL+
o + r is Element of REAL+
o is complex ext-real () set
r is complex ext-real () set
o + r is complex ext-real () set
0 + r is complex ext-real () set
o is complex ext-real () set
r is complex ext-real () set
o + r is complex ext-real () set
0 + r is complex ext-real () set
r is complex ext-real () set
s is complex ext-real () set
t is complex ext-real () set
r * t is complex ext-real () set
s * t is complex ext-real () set
o is Element of REAL+
z1 is complex ext-real () Element of REAL
s9 is complex ext-real () Element of REAL
* (s9,z1) is complex ext-real () Element of REAL
t99 is complex ext-real () set
t99 * t is complex ext-real () set
x99 is complex ext-real () Element of REAL
s99 is complex ext-real () Element of REAL
[*x99,s99*] is complex Element of COMPLEX
x9 is complex ext-real () Element of REAL
t9 is complex ext-real () Element of REAL
[*x9,t9*] is complex Element of COMPLEX
* (x99,x9) is complex ext-real () Element of REAL
* (s99,t9) is complex ext-real () Element of REAL
opp (* (s99,t9)) is complex ext-real () Element of REAL
+ ((* (x99,x9)),(opp (* (s99,t9)))) is complex ext-real () Element of REAL
* (x99,t9) is complex ext-real () Element of REAL
* (s99,x9) is complex ext-real () Element of REAL
+ ((* (x99,t9)),(* (s99,x9))) is complex ext-real () Element of REAL
[*(+ ((* (x99,x9)),(opp (* (s99,t9))))),(+ ((* (x99,t9)),(* (s99,x9))))*] is complex Element of COMPLEX
opp s99 is complex ext-real () Element of REAL
* ((opp s99),t9) is complex ext-real () Element of REAL
+ ((* (x99,x9)),(* ((opp s99),t9))) is complex ext-real () Element of REAL
y1 is complex ext-real () Element of REAL
* (y1,z1) is complex ext-real () Element of REAL
x1 is complex ext-real () Element of REAL
* (x1,z1) is complex ext-real () Element of REAL
s9 is Element of REAL+
t99 is Element of REAL+
s9 *' t99 is Element of REAL+
x99 is Element of REAL+
s99 is Element of REAL+
x99 *' s99 is Element of REAL+
s9 *' s99 is Element of REAL+
x9 is Element of REAL+
t9 is Element of REAL+
s9 is Element of REAL+
[0,s9] is set
{0,s9} is non empty set
{{0,s9},{0}} is non empty set
t99 is Element of REAL+
t99 *' s9 is Element of REAL+
[0,(t99 *' s9)] is set
{0,(t99 *' s9)} is non empty set
{{0,(t99 *' s9)},{0}} is non empty set
s9 is Element of REAL+
t99 is Element of REAL+
s9 *' t99 is Element of REAL+
s9 is Element of REAL+
[0,s9] is set
{0,s9} is non empty set
{{0,s9},{0}} is non empty set
t99 is Element of REAL+
t99 *' s9 is Element of REAL+
[0,(t99 *' s9)] is set
{0,(t99 *' s9)} is non empty set
{{0,(t99 *' s9)},{0}} is non empty set
x99 is Element of REAL+
[0,x99] is set
{0,x99} is non empty set
{{0,x99},{0}} is non empty set
s99 is Element of REAL+
[0,s99] is set
{0,s99} is non empty set
{{0,s99},{0}} is non empty set
x9 is Element of REAL+
[0,x9] is set
{0,x9} is non empty set
{{0,x9},{0}} is non empty set
t9 is Element of REAL+
t9 *' x9 is Element of REAL+
[0,(t9 *' x9)] is set
{0,(t9 *' x9)} is non empty set
{{0,(t9 *' x9)},{0}} is non empty set
s9 *' t9 is Element of REAL+
x9 *' t9 is Element of REAL+
r is complex ext-real () set
s is complex ext-real () set
r * s is complex ext-real () set
0 * s is complex ext-real () set
r is complex ext-real () set
s is complex ext-real () set
r * s is complex ext-real () set
r * 0 is complex ext-real () set
r is complex ext-real () set
- r is complex ext-real () set
s is complex ext-real () set
- s is complex ext-real () set
r - s is complex ext-real () set
r + (- s) is complex ext-real () set
s - s is complex ext-real () set
s + (- s) is complex ext-real () set
(r - s) - r is complex ext-real () set
(r - s) + (- r) is complex ext-real () set
0 - r is complex ext-real () set
0 + (- r) is complex ext-real () set
r is complex ext-real () set
s is complex ext-real () set
r * s is complex ext-real () set
r is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real () Element of NAT
r is non empty complex ext-real () set
r is complex ext-real non negative () set
s is complex ext-real non negative () set
r + s is complex ext-real () set
r is complex ext-real non positive () set
s is complex ext-real non positive () set
r + s is complex ext-real () set
r is non empty complex ext-real positive non negative () set
s is complex ext-real non negative () set
r + s is complex ext-real non negative () set
s + r is non empty complex ext-real positive non negative () set
r is non empty complex ext-real non positive negative () set
s is complex ext-real non positive () set
r + s is complex ext-real non positive () set
s + r is non empty complex ext-real non positive negative () set
r is complex ext-real non positive () set
- r is complex ext-real () set
- (- r) is complex ext-real () set
(- r) + (- (- r)) is complex ext-real () set
r is complex ext-real non negative () set
- r is complex ext-real () set
- (- r) is complex ext-real () set
(- r) + (- (- r)) is complex ext-real () set
r is complex ext-real non negative () set
s is complex ext-real non positive () set
r - s is complex ext-real () set
- s is complex ext-real non negative () set
r + (- s) is complex ext-real non negative () set
s - r is complex ext-real () set
- r is complex ext-real non positive () set
s + (- r) is complex ext-real non positive () set
r is non empty complex ext-real positive non negative () set
s is complex ext-real non positive () set
r - s is complex ext-real non negative () set
- s is complex ext-real non negative () set
r + (- s) is non empty complex ext-real positive non negative () set
s - r is complex ext-real non positive () set
- r is non empty complex ext-real non positive negative () set
s + (- r) is non empty complex ext-real non positive negative () set
r is non empty complex ext-real non positive negative () set
s is complex ext-real non negative () set
r - s is complex ext-real non positive () set
- s is complex ext-real non positive () set
r + (- s) is non empty complex ext-real non positive negative () set
s - r is complex ext-real non negative () set
- r is non empty complex ext-real positive non negative () set
s + (- r) is non empty complex ext-real positive non negative () set
r is complex ext-real non positive () set
s is complex ext-real non negative () set
r * s is complex ext-real () set
s * r is complex ext-real non positive () set
r is complex ext-real non positive () set
s is complex ext-real non positive () set
r * s is complex ext-real () set
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative () set
- (- 0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative () set
- r is complex ext-real non negative () set
- (- r) is complex ext-real non positive () set
s * (- r) is complex ext-real non positive () set
0 * (- r) is complex ext-real non positive () set
s * r is complex ext-real () set
- (s * r) is complex ext-real () set
- (- (s * r)) is complex ext-real () set
0 * r is complex ext-real non positive () set
- (0 * r) is complex ext-real non negative () set
- (- (0 * r)) is complex ext-real non positive () set
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative () set
- (- 0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative () set
- r is complex ext-real non negative () set
- (- r) is complex ext-real non positive () set
r is complex ext-real non negative () set
s is complex ext-real non negative () set
r * s is complex ext-real () set
r is non empty complex ext-real positive non negative () set
r " is non empty complex ext-real () set
(r ") " is non empty complex ext-real () set
(r ") * ((r ") ") is non empty complex ext-real () set
r is complex ext-real non positive () set
r " is complex ext-real () set
(r ") " is complex ext-real () set
(r ") * ((r ") ") is complex ext-real () set
r is non empty complex ext-real non positive negative () set
r " is non empty complex ext-real non positive negative () set
r is complex ext-real non negative () set
r " is complex ext-real () set
(r ") " is complex ext-real () set
(r ") * ((r ") ") is complex ext-real () set
r is complex ext-real non negative () set
s is complex ext-real non positive () set
r / s is complex ext-real () set
s " is complex ext-real non positive () set
r * (s ") is complex ext-real non positive () set
s / r is complex ext-real () set
r " is complex ext-real non negative () set
s * (r ") is complex ext-real non positive () set
r is complex ext-real non negative () set
s is complex ext-real non negative () set
r / s is complex ext-real () set
s " is complex ext-real non negative () set
r * (s ") is complex ext-real non negative () set
r is complex ext-real non positive () set
s is complex ext-real non positive () set
r / s is complex ext-real () set
s " is complex ext-real non positive () set
r * (s ") is complex ext-real non negative () set
r is complex ext-real () set
s is complex ext-real () set
min (r,s) is ext-real set
max (r,s) is ext-real set
r is complex ext-real () set
s is complex ext-real () set
r - s is complex ext-real () set
- s is complex ext-real () set
r + (- s) is complex ext-real () set
r is complex ext-real () set
s is complex ext-real () set
(r,s) is set
r - s is complex ext-real () set
- s is complex ext-real () set
r + (- s) is complex ext-real () set
r is complex ext-real () set
s is complex ext-real () set
(r,s) is complex ext-real () set
r - s is complex ext-real () set
- s is complex ext-real () set
r + (- s) is complex ext-real () set
t is complex ext-real () set