:: RAT_1 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
RAT+ is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer Element of NAT
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } ) \/ omega is non empty set
bool RAT+ is set
bool (bool RAT+) is set
DEDEKIND_CUTS is non empty Element of bool (bool RAT+)
REAL+ is non empty set
COMPLEX is non empty set
INT is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer Element of NAT
{{}} 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
RAT is non empty set
[:{{}},RAT+:] is set
RAT+ \/ [:{{}},RAT+:] is non empty set
(RAT+ \/ [:{{}},RAT+:]) \ {[{},{}]} is Element of bool (RAT+ \/ [:{{}},RAT+:])
bool (RAT+ \/ [:{{}},RAT+:]) is set
one is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer Element of RAT+
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer Element of RAT+
{0} is non empty set
[:{0},REAL+:] is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } ) \/ omega is non empty set
09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
09 / p is Element of RAT+
09 / p is ext-real non negative V31() real Element of REAL
p " is ext-real non negative V31() real set
09 * (p ") is ext-real non negative V31() real set
opp 0 is ext-real V31() real Element of REAL
+ (0,(opp 0)) is ext-real V31() real Element of REAL
p " is ext-real non negative V31() real Element of REAL
p * (p ") is ext-real non negative V31() real Element of REAL
s is ext-real V31() real Element of REAL
r is ext-real V31() real Element of REAL
[*s,r*] is Element of COMPLEX
k is ext-real V31() real Element of REAL
m is ext-real V31() real Element of REAL
[*k,m*] is Element of COMPLEX
* (s,k) is ext-real V31() real Element of REAL
* (r,m) is ext-real V31() real Element of REAL
opp (* (r,m)) is ext-real V31() real Element of REAL
+ ((* (s,k)),(opp (* (r,m)))) is ext-real V31() real Element of REAL
* (s,m) is ext-real V31() real Element of REAL
* (r,k) is ext-real V31() real Element of REAL
+ ((* (s,m)),(* (r,k))) is ext-real V31() real Element of REAL
[*(+ ((* (s,k)),(opp (* (r,m))))),(+ ((* (s,m)),(* (r,k))))*] is Element of COMPLEX
+ ((* (s,k)),(opp 0)) is ext-real V31() real Element of REAL
l is Element of RAT+
z is Element of RAT+
l *' z is Element of RAT+
numerator l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator l) *^ (numerator z) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator l) *^ (denominator z) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator l) *^ (numerator z)) / ((denominator l) *^ (denominator z)) is Element of RAT+
x9 is Element of REAL+
y9 is Element of REAL+
x9 *' y9 is Element of REAL+
xx1 is ext-real V31() real Element of REAL
yy1 is ext-real V31() real Element of REAL
* (xx1,yy1) is ext-real V31() real Element of REAL
a is Element of REAL+
b is Element of REAL+
a *' b is Element of REAL+
x91 is Element of RAT+
x92 is Element of RAT+
x91 *' x92 is Element of RAT+
numerator x91 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator x92 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator x91) *^ (numerator x92) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator x91 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator x92 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator x91) *^ (denominator x92) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator x91) *^ (numerator x92)) / ((denominator x91) *^ (denominator x92)) is Element of RAT+
09 * (p ") is ext-real non negative V31() real Element of REAL
x91 is ext-real V31() real Element of REAL
x92 is ext-real V31() real Element of REAL
[*x91,x92*] is Element of COMPLEX
y91 is ext-real V31() real Element of REAL
y92 is ext-real V31() real Element of REAL
[*y91,y92*] is Element of COMPLEX
* (x91,y91) is ext-real V31() real Element of REAL
* (x92,y92) is ext-real V31() real Element of REAL
opp (* (x92,y92)) is ext-real V31() real Element of REAL
+ ((* (x91,y91)),(opp (* (x92,y92)))) is ext-real V31() real Element of REAL
* (x91,y92) is ext-real V31() real Element of REAL
* (x92,y91) is ext-real V31() real Element of REAL
+ ((* (x91,y92)),(* (x92,y91))) is ext-real V31() real Element of REAL
[*(+ ((* (x91,y91)),(opp (* (x92,y92))))),(+ ((* (x91,y92)),(* (x92,y91))))*] is Element of COMPLEX
x19 is Element of REAL+
y19 is Element of REAL+
x19 *' y19 is Element of REAL+
* (x91,k) is ext-real V31() real Element of REAL
* (x92,0) is ext-real V31() real Element of REAL
opp (* (x92,0)) is ext-real V31() real Element of REAL
+ ((* (x91,k)),(opp (* (x92,0)))) is ext-real V31() real Element of REAL
+ ((* (x91,k)),0) is ext-real V31() real Element of REAL
x9 is Element of REAL+
y9 is Element of REAL+
x9 *' y9 is Element of REAL+
x99 is Element of RAT+
y99 is Element of RAT+
x99 *' y99 is Element of RAT+
numerator x99 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator y99 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator x99) *^ (numerator y99) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator x99 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator y99 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator x99) *^ (denominator y99) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator x99) *^ (numerator y99)) / ((denominator x99) *^ (denominator y99)) is Element of RAT+
a is Element of RAT+
b is Element of RAT+
a *' b is Element of RAT+
numerator a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator a) *^ (numerator b) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator a) *^ (denominator b) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator a) *^ (numerator b)) / ((denominator a) *^ (denominator b)) is Element of RAT+
p / one is Element of RAT+
(09 / p) *' (p / one) is Element of RAT+
numerator (09 / p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator (p / one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator (09 / p)) *^ (numerator (p / one)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator (09 / p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator (p / one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator (09 / p)) *^ (denominator (p / one)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator (09 / p)) *^ (numerator (p / one))) / ((denominator (09 / p)) *^ (denominator (p / one))) is Element of RAT+
09 *^ p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
p *^ one is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
(09 *^ p) / (p *^ one) is Element of RAT+
09 / one is Element of RAT+
p / p is Element of RAT+
(09 / one) *' (p / p) is Element of RAT+
numerator (09 / one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator (p / p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator (09 / one)) *^ (numerator (p / p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator (09 / one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator (p / p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator (09 / one)) *^ (denominator (p / p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator (09 / one)) *^ (numerator (p / p))) / ((denominator (09 / one)) *^ (denominator (p / p))) is Element of RAT+
(09 / one) *' one is Element of RAT+
numerator one is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator (09 / one)) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator one is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator (09 / one)) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator (09 / one)) *^ (numerator one)) / ((denominator (09 / one)) *^ (denominator one)) is Element of RAT+
x99 *' one is Element of RAT+
(numerator x99) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
(denominator x99) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator x99) *^ (numerator one)) / ((denominator x99) *^ (denominator one)) is Element of RAT+
(x99 *' y99) *' b is Element of RAT+
numerator (x99 *' y99) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator (x99 *' y99)) *^ (numerator b) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator (x99 *' y99) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator (x99 *' y99)) *^ (denominator b) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator (x99 *' y99)) *^ (numerator b)) / ((denominator (x99 *' y99)) *^ (denominator b)) is Element of RAT+
c₂₆ is Element of RAT+
c₂₇ is Element of RAT+
c₂₆ *' c₂₇ is Element of RAT+
numerator c₂₆ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
numerator c₂₇ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator c₂₆) *^ (numerator c₂₇) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
denominator c₂₆ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator c₂₇ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(denominator c₂₆) *^ (denominator c₂₇) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer set
((numerator c₂₆) *^ (numerator c₂₇)) / ((denominator c₂₆) *^ (denominator c₂₇)) is Element of RAT+
09 is Element of REAL+
p is ext-real V31() real set
- p is ext-real V31() real set
q is Element of REAL+
09 - q is set
q -' 09 is Element of REAL+
[{},(q -' 09)] is set
{{},(q -' 09)} is non empty set
{{}} is non empty set
{{{},(q -' 09)},{{}}} is non empty set
[0,0] is set
{0,0} is non empty set
{{0,0},{0}} is non empty set
{[0,0]} is non empty set
(q -' 09) + 09 is Element of REAL+
REAL+ \/ [:{0},REAL+:] is non empty set
r is ext-real V31() real Element of REAL
p + r is ext-real V31() real Element of REAL
k is ext-real V31() real Element of REAL
m is ext-real V31() real Element of REAL
[*k,m*] is Element of COMPLEX
l is ext-real V31() real Element of REAL
z is ext-real V31() real Element of REAL
[*l,z*] is Element of COMPLEX
+ (k,l) is ext-real V31() real Element of REAL
+ (m,z) is ext-real V31() real Element of REAL
[*(+ (k,l)),(+ (m,z))*] is Element of COMPLEX
x9 is Element of REAL+
y9 is Element of REAL+
[0,y9] is set
{0,y9} is non empty set
{{0,y9},{0}} is non empty set
x9 - y9 is set
p is set
q is Element of RAT+
numerator q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
denominator q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
(numerator q) / (denominator q) is ext-real non negative V31() real set
(denominator q) " is ext-real non negative V31() real set
(numerator q) * ((denominator q) ") is ext-real non negative V31() real set
(numerator q) / (denominator q) is Element of RAT+
[:{0},RAT+:] is set
[0,0] is set
{0,0} is non empty set
{{0,0},{0}} is non empty set
{[0,0]} is non empty set
q is set
s is set
[q,s] is set
{q,s} is non empty set
{q} is non empty set
{{q,s},{q}} is non empty set
r is Element of RAT+
k is Element of REAL+
[0,k] is set
{0,k} is non empty set
{{0,k},{0}} is non empty set
numerator r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
- (numerator r) is ext-real non positive V31() real integer set
m is ext-real non positive V31() real integer set
denominator r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega
m / l is ext-real non positive V31() real set
l " is ext-real non negative V31() real set
m * (l ") is ext-real non positive V31() real set
(numerator r) / (denominator r) is Element of RAT+
(numerator r) / l is ext-real non negative V31() real set
(numerator r) * (l ") is ext-real non negative V31() real set
09 - k is set
- ((numerator r) / l) is ext-real non positive V31() real set
[:{0},RAT+:] is set
p is set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
s is ext-real V31() real integer set
s / q is ext-real V31() real Element of REAL
q " is ext-real non negative V31() real set
s * (q ") is ext-real V31() real set
[0,0] is set
{0,0} is non empty set
{{0,0},{0}} is non empty set
{[0,0]} is non empty set
0 " is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer Element of REAL
s * (0 ") is ext-real V31() real integer Element of REAL
[:{0},RAT+:] is set
RAT+ \/ [:{0},RAT+:] is non empty set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
r / q is Element of RAT+
[:{0},RAT+:] is set
RAT+ \/ [:{0},RAT+:] is non empty set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
- r is ext-real non positive V31() real integer Element of REAL
r / q is ext-real non negative V31() real Element of REAL
r * (q ") is ext-real non negative V31() real set
r / q is Element of RAT+
- (r / q) is ext-real non positive V31() real Element of REAL
k is Element of REAL+
09 - k is set
[0,k] is set
{0,k} is non empty set
{{0,k},{0}} is non empty set
[:{0},RAT+:] is set
RAT+ \/ [:{0},RAT+:] is non empty set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
p is set
q is ext-real V31() real integer set
s is ext-real V31() real integer set
q / s is ext-real V31() real set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of NAT
- r is ext-real non positive V31() real integer Element of REAL
- q is ext-real V31() real integer set
(- q) / r is ext-real V31() real Element of REAL
r " is ext-real non negative V31() real set
(- q) * (r ") is ext-real V31() real set
p is set
q is set
s is set
r is ext-real V31() real integer set
k is ext-real V31() real integer set
r / k is ext-real V31() real set
k " is ext-real V31() real set
r * (k ") is ext-real V31() real set
q is set
s is ext-real V31() real integer set
r is ext-real V31() real integer set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
q is set
s is ext-real V31() real integer set
r is ext-real V31() real integer set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
p is ext-real V31() real integer set
q is ext-real V31() real integer set
p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
s is ext-real V31() real set
p is ext-real V31() real integer set
q is ext-real V31() real integer set
p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
s is ext-real V31() real set
p is set
0 / 1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer Element of REAL
1 " is non empty ext-real positive non negative V31() real set
0 * (1 ") is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real integer set
q is ext-real V31() real integer set
s is ext-real V31() real integer set
q / s is ext-real V31() real set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set
p is set
p is set
p is ext-real V31() real integer set
q is ext-real V31() real integer set
p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
p is set
q is ext-real V31() real integer set
q / 1 is ext-real V31() real Element of REAL
1 " is non empty ext-real positive non negative V31() real set
q * (1 ") is ext-real V31() real set
p is ext-real V31() real () set
q is ext-real V31() real () set
p * q is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * s is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
(k * s) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
(k * s) * ((m * r) ") is ext-real V31() real set
p + q is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * r is ext-real V31() real integer () set
s * m is ext-real V31() real integer () set
(k * r) + (s * m) is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
((k * r) + (s * m)) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
((k * r) + (s * m)) * ((m * r) ") is ext-real V31() real set
p - q is ext-real V31() real set
- q is ext-real V31() real set
p + (- q) is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * r is ext-real V31() real integer () set
s * m is ext-real V31() real integer () set
(k * r) - (s * m) is ext-real V31() real integer () set
- (s * m) is ext-real V31() real integer () set
(k * r) + (- (s * m)) is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
((k * r) - (s * m)) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
((k * r) - (s * m)) * ((m * r) ") is ext-real V31() real set
p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
1 / (k / m) is ext-real V31() real Element of REAL
(k / m) " is ext-real V31() real set
1 * ((k / m) ") is ext-real V31() real set
p * (1 / (k / m)) is ext-real V31() real Element of REAL
1 * m is ext-real V31() real integer () Element of REAL
(1 * m) / k is ext-real V31() real Element of REAL
k " is ext-real V31() real set
(1 * m) * (k ") is ext-real V31() real set
p * ((1 * m) / k) is ext-real V31() real Element of REAL
s * m is ext-real V31() real integer () set
r * k is ext-real V31() real integer () set
(s * m) / (r * k) is ext-real V31() real set
(r * k) " is ext-real V31() real set
(s * m) * ((r * k) ") is ext-real V31() real set
p is ext-real V31() real () set
- p is ext-real V31() real set
s is ext-real V31() real integer () set
q is ext-real V31() real integer () set
q / s is ext-real V31() real () set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set
- q is ext-real V31() real integer () set
(- q) / s is ext-real V31() real () set
(- q) * (s ") is ext-real V31() real set
p " is ext-real V31() real set
1 / p is ext-real V31() real () Element of REAL
1 * (p ") is ext-real V31() real set
p is ext-real V31() real set
q is ext-real V31() real set
q - p is ext-real V31() real set
- p is ext-real V31() real set
q + (- p) is ext-real V31() real set
(q - p) " is ext-real V31() real set
[\((q - p) ")/] is ext-real V31() real integer () set
[\((q - p) ")/] + 1 is ext-real V31() real integer () Element of REAL
([\((q - p) ")/] + 1) * p is ext-real V31() real Element of REAL
[\(([\((q - p) ")/] + 1) * p)/] is ext-real V31() real integer () set
[\(([\((q - p) ")/] + 1) * p)/] + 1 is ext-real V31() real integer () Element of REAL
([\(([\((q - p) ")/] + 1) * p)/] + 1) / ([\((q - p) ")/] + 1) is ext-real V31() real () Element of REAL
([\((q - p) ")/] + 1) " is ext-real V31() real () set
([\(([\((q - p) ")/] + 1) * p)/] + 1) * (([\((q - p) ")/] + 1) ") is ext-real V31() real () set
p - p is ext-real V31() real set
p + (- p) is ext-real V31() real set
((q - p) ") - 1 is ext-real V31() real Element of REAL
- 1 is ext-real non positive V31() real integer () set
((q - p) ") + (- 1) is ext-real V31() real set
([\((q - p) ")/] + 1) * (q - p) is ext-real V31() real Element of REAL
((q - p) ") * (q - p) is ext-real V31() real set
(([\((q - p) ")/] + 1) * p) - 1 is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) * p) + (- 1) is ext-real V31() real set
([\((q - p) ")/] + 1) " is ext-real V31() real () Element of REAL
(([\((q - p) ")/] + 1) ") * ([\(([\((q - p) ")/] + 1) * p)/] + 1) is ext-real V31() real () Element of REAL
(([\((q - p) ")/] + 1) ") * (([\((q - p) ")/] + 1) * p) is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1) is ext-real V31() real () Element of REAL
((([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1)) * p is ext-real V31() real Element of REAL
1 * p is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) * p) + (([\((q - p) ")/] + 1) * (q - p)) is ext-real V31() real Element of REAL
([\((q - p) ")/] + 1) * q is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) ") * (([\((q - p) ")/] + 1) * q) is ext-real V31() real Element of REAL
((([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1)) * q is ext-real V31() real Element of REAL
1 * q is ext-real V31() real Element of REAL
p is ext-real V31() real () set
s is ext-real V31() real integer () set
q is ext-real V31() real integer () set
q / s is ext-real V31() real () set
s " is ext-real V31() real () set
q * (s ") is ext-real V31() real () set
- q is ext-real V31() real integer () set
(- q) / s is ext-real V31() real () set
(- q) * (s ") is ext-real V31() real () set
- ((- q) / s) is ext-real V31() real () set
- s is ext-real V31() real integer () set
(- q) / (- s) is ext-real V31() real () set
(- s) " is ext-real V31() real () set
(- q) * ((- s) ") is ext-real V31() real () set
p is ext-real V31() real () set
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q is ext-real V31() real integer () set
q / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
q * (s ") is ext-real V31() real () set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () set
s is ext-real V31() real integer () set
s / q is ext-real V31() real () set
q " is ext-real non negative V31() real () set
s * (q ") is ext-real V31() real () set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () set
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r is ext-real V31() real integer () set
r / q is ext-real V31() real () set
q " is ext-real non negative V31() real () set
r * (q ") is ext-real V31() real () set
r is ext-real V31() real integer () set
r / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
r * (s ") is ext-real V31() real () set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k is ext-real V31() real integer () set
k / m is ext-real V31() real () Element of REAL
m " is ext-real non negative V31() real () set
k * (m ") is ext-real V31() real () set
p is ext-real V31() real () set
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q is ext-real V31() real integer () set
q / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
q * (s ") is ext-real V31() real () set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r is ext-real V31() real integer () set
r / k is ext-real V31() real () Element of REAL
k " is ext-real non negative V31() real () set
r * (k ") is ext-real V31() real () set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r is ext-real V31() real integer () set
r / q is ext-real V31() real () Element of REAL
q " is ext-real non negative V31() real () set
r * (q ") is ext-real V31() real () set
r is ext-real V31() real integer () set
r / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
r * (s ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real integer () set
q / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
q * ((p) ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) " is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) " is ext-real non negative V31() real () Element of REAL
1 * ((p) ") is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
(p) " is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
((p) ") * (p) is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
p * ((p) * ((p) ")) is ext-real V31() real () Element of REAL
p * 1 is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) / p is ext-real V31() real () set
p " is ext-real V31() real () set
(p) * (p ") is ext-real V31() real () set
(p ") * p is ext-real V31() real () set
((p ") * p) * (p) is ext-real V31() real () Element of REAL
(p ") * (p) is ext-real V31() real () set
1 * (p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real integer () set
q / 1 is ext-real V31() real () Element of REAL
1 " is non empty ext-real positive non negative V31() real () set
q * (1 ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
1 " is non empty ext-real positive non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) " is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
- 1 is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real non positive V31() real integer () Element of REAL
(- (p)) / (p) is ext-real non positive V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(- (p)) * ((p) ") is ext-real non positive V31() real () set
(p) / (p) is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () set
- ((p) / (p)) is ext-real non positive V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real integer () set
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) * q is ext-real V31() real () Element of REAL
(q) * p is ext-real V31() real integer () set
(q) * p is ext-real V31() real integer () Element of REAL
((q) * p) / ((q) * p) is ext-real V31() real () Element of REAL
((q) * p) " is ext-real V31() real () set
((q) * p) * (((q) * p) ") is ext-real V31() real () set
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q is ext-real V31() real integer () set
q / p is ext-real V31() real () Element of REAL
p " is ext-real non negative V31() real () set
q * (p ") is ext-real V31() real () set
s is ext-real V31() real () set
(s) is ext-real V31() real integer () set
(s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * s is ext-real V31() real () Element of REAL
s * p is ext-real V31() real () Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer () Element of NAT
p * 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () set
r * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
1 * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () set
r * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * k is ext-real V31() real integer () Element of REAL
(s) * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
0 + (k * (s)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p - (k * (s)) is ext-real V31() real integer () Element of REAL
- (k * (s)) is ext-real non positive V31() real integer () set
p + (- (k * (s))) is ext-real V31() real integer () set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((s) * k) / (k * (s)) is ext-real V31() real () Element of REAL
(k * (s)) " is ext-real non negative V31() real () set
((s) * k) * ((k * (s)) ") is ext-real V31() real () set
q - ((s) * k) is ext-real V31() real integer () Element of REAL
- ((s) * k) is ext-real V31() real integer () set
q + (- ((s) * k)) is ext-real V31() real integer () set
(q - ((s) * k)) / m is ext-real V31() real () Element of REAL
m " is ext-real non negative V31() real () set
(q - ((s) * k)) * (m ") is ext-real V31() real () set
(k * (s)) + (1 * (s)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer () Element of NAT
(k + 1) * (s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) / (s) is ext-real V31() real () Element of REAL
(s) " is ext-real non negative V31() real () set
(s) * ((s) ") is ext-real V31() real () set
((s) / (s)) * ((s) * k) is ext-real V31() real () Element of REAL
((s) / (s)) * (s) is ext-real V31() real () Element of REAL
(((s) / (s)) * (s)) * k is ext-real V31() real () Element of REAL
p is ext-real V31() real integer () set
q is ext-real V31() real integer () set
p / q is ext-real V31() real () set
q " is ext-real V31() real () set
p * (q ") is ext-real V31() real () set
s is ext-real V31() real () set
(s) is ext-real V31() real integer () set
(s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * s is ext-real V31() real () Element of REAL
- q is ext-real V31() real integer () set
- p is ext-real V31() real integer () set
(- p) / q is ext-real V31() real () set
(- p) * (q ") is ext-real V31() real () set
- ((- p) / q) is ext-real V31() real () set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(- p) / r is ext-real V31() real () Element of REAL
r " is ext-real non negative V31() real () set
(- p) * (r ") is ext-real V31() real () set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * k is ext-real V31() real integer () Element of REAL
(s) * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
- k is ext-real non positive V31() real integer () Element of REAL
m is ext-real non positive V31() real integer () Element of REAL
(s) * m is ext-real V31() real integer () set
(s) * m is ext-real non positive V31() real integer () Element of REAL
- ((s) * k) is ext-real V31() real integer () Element of REAL
(s) * m is ext-real V31() real integer () Element of REAL
- ((s) * k) is ext-real non positive V31() real integer () Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * k is ext-real V31() real integer () Element of REAL
(s) * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
m is ext-real V31() real integer () set
(s) * m is ext-real V31() real integer () set
(s) * m is ext-real V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r * q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r * q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
r * q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s * q) / (r * q) is ext-real V31() real () Element of REAL
(r * q) " is ext-real non negative V31() real () set
(s * q) * ((r * q) ") is ext-real V31() real () set
s / r is ext-real V31() real () Element of REAL
r " is ext-real non negative V31() real () set
s * (r ") is ext-real V31() real () set
q / q is ext-real non negative V31() real () Element of REAL
q " is ext-real non negative V31() real () set
q * (q ") is ext-real non negative V31() real () set
(s / r) * (q / q) is ext-real V31() real () Element of REAL
(s / r) * 1 is ext-real V31() real () Element of REAL
r * 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q is ext-real V31() real integer () set
q / p is ext-real V31() real () Element of REAL
p " is ext-real non negative V31() real () set
q * (p ") is ext-real V31() real () set
s is ext-real V31() real () set
(s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) is ext-real V31() real integer () set
(s) * s is ext-real V31() real () Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(s) * r is ext-real V31() real integer () Element of REAL
(s) * r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
- (p) is ext-real non positive V31() real integer () Element of REAL
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () Element of REAL
(- 1) * (p) is ext-real non positive V31() real integer () Element of REAL
((- 1) * (p)) * ((p) ") is ext-real non positive V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
(- 1) * ((p) * ((p) ")) is ext-real non positive V31() real () Element of REAL
(- 1) * 1 is ext-real non positive V31() real integer () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
((p) / (p)) * (p) is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
- (- (p)) is ext-real V31() real integer () set
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (- (p)) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
1 * (p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((p) / (p)) * (p) is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real set
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) * q is ext-real V31() real () Element of REAL
p * (q) is ext-real V31() real Element of REAL
(q) " is ext-real non negative V31() real () Element of REAL
(q) * ((q) ") is ext-real V31() real () Element of REAL
(p * (q)) * ((q) ") is ext-real V31() real Element of REAL
(q) * ((q) ") is ext-real non negative V31() real () Element of REAL
p * ((q) * ((q) ")) is ext-real V31() real Element of REAL
p * 1 is ext-real V31() real Element of REAL
p is ext-real V31() real set
q is ext-real V31() real () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p * (q) is ext-real V31() real Element of REAL
(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL
1 * (q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p * (q)) / (1 * (q)) is ext-real V31() real Element of REAL
(1 * (q)) " is ext-real non negative V31() real () set
(p * (q)) * ((1 * (q)) ") is ext-real V31() real set
p / 1 is ext-real V31() real Element of REAL
1 " is non empty ext-real positive non negative V31() real () set
p * (1 ") is ext-real V31() real set
(q) / (q) is ext-real non negative V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real non negative V31() real () set
(p / 1) * ((q) / (q)) is ext-real V31() real Element of REAL
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) * q is ext-real V31() real () Element of REAL
(q) * (p) is ext-real V31() real integer () Element of REAL
(p) * (q) is ext-real V31() real integer () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set
p is ext-real V31() real () set
- p is ext-real V31() real () set
((- p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((- p)) is ext-real V31() real integer () set
((- p)) * (- p) is ext-real V31() real () Element of REAL
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (- p) is ext-real V31() real () set
((- p)) / ((- p)) is ext-real V31() real () Element of REAL
((- p)) " is ext-real non negative V31() real () set
((- p)) * (((- p)) ") is ext-real V31() real () set
- (((- p)) / ((- p))) is ext-real V31() real () Element of REAL
- ((- p)) is ext-real V31() real integer () set
(- ((- p))) / ((- p)) is ext-real V31() real () Element of REAL
(- ((- p))) * (((- p)) ") is ext-real V31() real () set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * q is ext-real V31() real integer () Element of REAL
(p) * q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
- ((p) / (p)) is ext-real V31() real () Element of REAL
(- (p)) / (p) is ext-real V31() real () Element of REAL
(- (p)) * ((p) ") is ext-real V31() real () set
s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((- p)) * s is ext-real V31() real integer () Element of REAL
((- p)) * s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((p) * q) * s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
q * s is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) * (q * s) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
1 / p is ext-real V31() real () Element of REAL
p " is ext-real V31() real () set
1 * (p ") is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) * q is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
1 / ((p) / (p)) is ext-real V31() real () Element of REAL
((p) / (p)) " is ext-real V31() real () set
1 * (((p) / (p)) ") is ext-real V31() real () set
1 * (p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(1 * (p)) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real V31() real () set
(1 * (p)) * ((p) ") is ext-real V31() real () set
(p) / (p) is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
l * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
l * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
l * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
0 * m is ext-real V31() real integer () Element of REAL
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
z * k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
p is ext-real V31() real () set
1 / p is ext-real V31() real () Element of REAL
p " is ext-real V31() real () set
1 * (p ") is ext-real V31() real () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
- (p) is ext-real non positive V31() real integer () Element of REAL
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(q) * q is ext-real V31() real () Element of REAL
- q is ext-real V31() real () set
- p is ext-real V31() real () set
1 / (- p) is ext-real V31() real () Element of REAL
(- p) " is ext-real V31() real () set
1 * ((- p) ") is ext-real V31() real () set
((- q)) is ext-real V31() real integer () set
((- q)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
((- q)) * (- q) is ext-real V31() real () Element of REAL
((- p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
- (q) is ext-real V31() real integer () set
- (- (q)) is ext-real V31() real integer () set
((- p)) is ext-real V31() real integer () set
((- p)) * (- p) is ext-real V31() real () Element of REAL
(- (p)) / (- (p)) is ext-real V31() real () Element of REAL
(- (p)) " is ext-real V31() real () set
(- (p)) * ((- (p)) ") is ext-real V31() real () set
(p) / (- (p)) is ext-real V31() real () Element of REAL
(p) * ((- (p)) ") is ext-real V31() real () set
- ((p) / (- (p))) is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real V31() real () set
(p) * ((p) ") is ext-real V31() real () set
- ((p) / (p)) is ext-real V31() real () Element of REAL
- (- ((p) / (p))) is ext-real V31() real () Element of REAL
1 * (p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT
(1 * (p)) / (p) is ext-real V31() real () Element of REAL
(1 * (p)) * ((p) ") is ext-real V31() real () set
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
1 / ((p) / (p)) is ext-real V31() real () Element of REAL
((p) / (p)) " is ext-real V31() real () set
1 * (((p) / (p)) ") is ext-real V31() real () set