:: RAT_1 semantic presentation
begin
definition
redefine
func
RAT
means
:: RAT_1:def 1
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( (
ext-real
) (
ext-real
)
set
) iff ex
m
,
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) st
x
: ( ( ) ( )
set
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
/
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) : ( ( ) (
ext-real
V31
()
real
)
set
) );
end;
definition
let
r
be ( ( ) ( )
number
) ;
attr
r
is
rational
means
:: RAT_1:def 2
r
: ( (
ext-real
) (
ext-real
)
set
)
in
RAT
: ( ( ) ( non
empty
)
set
) ;
end;
registration
cluster
ext-real
V31
()
real
rational
for ( ( ) ( )
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
end;
registration
cluster
rational
for ( ( ) ( )
set
) ;
end;
definition
mode
Rational
is
( (
rational
) (
rational
)
number
) ;
end;
theorem
:: RAT_1:1
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
RAT
: ( ( ) ( non
empty
)
set
) holds
ex
m
,
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) st
(
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
x
: ( ( ) ( )
set
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
/
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) : ( ( ) (
ext-real
V31
()
real
)
set
) ) ;
theorem
:: RAT_1:2
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
) is ( (
rational
) (
rational
)
Rational
) holds
ex
m
,
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) st
(
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
x
: ( ( ) ( )
set
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
/
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) : ( ( ) (
ext-real
V31
()
real
)
set
) ) ;
registration
cluster
rational
->
real
for ( ( ) ( )
set
) ;
end;
theorem
:: RAT_1:3
for
m
,
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) holds
m
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
/
n
: ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) : ( ( ) (
ext-real
V31
()
real
)
set
) is
rational
;
registration
cluster
integer
->
rational
for ( ( ) ( )
set
) ;
end;
registration
let
p
,
q
be ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ;
cluster
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
*
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
ext-real
V31
()
real
)
set
)
->
rational
;
cluster
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
+
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
ext-real
V31
()
real
)
set
)
->
rational
;
cluster
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
-
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
ext-real
V31
()
real
)
set
)
->
rational
;
cluster
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
/
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
ext-real
V31
()
real
)
set
)
->
rational
;
end;
registration
let
p
be ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ;
cluster
-
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( (
V31
() ) (
ext-real
V31
()
real
)
set
)
->
V31
()
rational
;
cluster
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
"
: ( (
V31
() ) (
ext-real
V31
()
real
)
set
)
->
V31
()
rational
;
end;
theorem
:: RAT_1:4
canceled;
theorem
:: RAT_1:5
canceled;
theorem
:: RAT_1:6
canceled;
theorem
:: RAT_1:7
for
a
,
b
being ( (
real
) (
ext-real
V31
()
real
)
number
) st
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
<
b
: ( (
real
) (
ext-real
V31
()
real
)
number
) holds
ex
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
(
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
<
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
b
: ( (
real
) (
ext-real
V31
()
real
)
number
) ) ;
theorem
:: RAT_1:8
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ex
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) ex
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) st
(
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:9
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ex
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) ex
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) st
(
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) & ( for
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
l
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) st
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
n
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) holds
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<=
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ) ;
definition
let
p
be ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ;
func
denominator
p
->
( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
means
:: RAT_1:def 3
(
it
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) & ex
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) st
p
: ( ( ) ( )
set
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
it
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) & ( for
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) st
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
p
: ( ( ) ( )
set
)
=
n
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) holds
it
: ( (
rational
) (
ext-real
V31
()
real
rational
)
set
)
<=
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) );
end;
definition
let
p
be ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ;
func
numerator
p
->
( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
equals
:: RAT_1:def 4
(
denominator
p
: ( ( ) ( )
set
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
p
: ( ( ) ( )
set
) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: RAT_1:10
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: RAT_1:11
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: RAT_1:12
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
"
: ( ( ) (
ext-real
non
negative
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RAT_1:13
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
>=
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
"
: ( ( ) (
ext-real
non
negative
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RAT_1:14
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:15
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
(
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
"
)
: ( ( ) (
ext-real
non
negative
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
(
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
"
)
: ( ( ) (
ext-real
non
negative
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) )
*
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:16
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
ext-real
V31
()
real
rational
)
set
) ;
theorem
:: RAT_1:17
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) is ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) holds
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ) ;
theorem
:: RAT_1:18
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st (
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) or
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) holds
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) is ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) ;
theorem
:: RAT_1:19
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) iff
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:20
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st (
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) or
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) is ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: RAT_1:21
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
( 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff not
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) is
integer
) ;
theorem
:: RAT_1:22
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
( 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
>
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
"
: ( ( ) (
ext-real
non
negative
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff not
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) is
integer
) ;
theorem
:: RAT_1:23
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:24
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
-
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:25
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
-
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( (
V31
() ) (
ext-real
V31
()
real
integer
rational
)
set
)
=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:26
for
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
(
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
)
: ( ( ) (
ext-real
V31
()
real
integer
rational
)
set
)
/
(
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
)
: ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
theorem
:: RAT_1:27
for
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
for
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) holds
ex
l
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) st
(
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) &
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:28
for
m
,
n
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
n
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( ( ) (
ext-real
V31
()
real
)
set
) &
n
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
ex
m1
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
) st
(
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
m1
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
set
) &
n
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
m1
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:29
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
for
l
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
( not 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) or for
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
( not
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) or not
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: RAT_1:30
for
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
for
m
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
/
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) &
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) & ( for
l
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
( not 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) or for
m1
being ( (
integer
) (
ext-real
V31
()
real
integer
)
Integer
)
for
k1
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) holds
( not
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
m1
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) or not
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
k1
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
*
l
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ) ) holds
(
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
m
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) ) ;
theorem
:: RAT_1:31
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<
-
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:32
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<=
-
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:33
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
-
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( (
V31
() ) (
ext-real
V31
()
real
integer
rational
)
set
) ) ;
theorem
:: RAT_1:34
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<=
-
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( (
V31
() ) (
ext-real
V31
()
real
integer
rational
)
set
) ) ;
theorem
:: RAT_1:35
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:36
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:37
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:38
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<=
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) iff
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
<=
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: RAT_1:39
for
a
being ( (
real
) (
ext-real
V31
()
real
)
number
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
<
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) iff
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
*
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) )
<
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) ) ;
theorem
:: RAT_1:40
for
a
being ( (
real
) (
ext-real
V31
()
real
)
number
)
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
<=
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) iff
a
: ( (
real
) (
ext-real
V31
()
real
)
number
)
*
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) )
<=
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) ) ;
theorem
:: RAT_1:41
for
p
,
q
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) st
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
denominator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
numerator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) holds
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) ;
theorem
:: RAT_1:42
for
p
,
q
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) iff
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
(
denominator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) )
<
(
numerator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
*
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: RAT_1:43
for
p
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
denominator
(
-
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
V31
() ) (
ext-real
V31
()
real
rational
)
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
numerator
(
-
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
V31
() ) (
ext-real
V31
()
real
rational
)
set
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
-
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( (
V31
() ) (
ext-real
V31
()
real
integer
rational
)
set
) ) ;
theorem
:: RAT_1:44
for
p
,
q
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) &
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
/
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff (
numerator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
denominator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) ) ) ;
theorem
:: RAT_1:45
for
p
,
q
being ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) holds
(
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
<
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
ext-real
non
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) &
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
/
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
ext-real
V31
()
real
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) iff (
numerator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
)
=
-
(
denominator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
non
positive
V31
()
real
integer
rational
)
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) &
denominator
q
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
non
negative
V31
()
real
integer
rational
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
=
-
(
numerator
p
: ( (
rational
) (
ext-real
V31
()
real
rational
)
Rational
)
)
: ( (
integer
) (
ext-real
V31
()
real
integer
rational
)
Integer
) : ( (
V31
() ) (
ext-real
V31
()
real
integer
rational
)
set
) ) ) ;