:: XREAL_0 semantic presentation

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

{ [b

1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real Element of NAT

{ [b

{ [b

bool { [b

( { [b

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 )

{ b

K78({{},1},REAL) \ { b

bool K78({{},1},REAL) is set

(K78({{},1},REAL) \ { b

-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