:: ARYTM_1 semantic presentation
begin
theorem
:: ARYTM_1:1
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:2
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
( not
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) or
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) or
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ) ;
theorem
:: ARYTM_1:3
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:4
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:5
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:6
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:7
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) iff
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ) ;
theorem
:: ARYTM_1:8
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
definition
let
x
,
y
be ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
func
x
-'
y
->
( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
means
:: ARYTM_1:def 1
it
: ( ( ) ( )
Element
of
K6
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
if
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
otherwise
it
: ( ( ) ( )
Element
of
K6
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ;
end;
theorem
:: ARYTM_1:9
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) or
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<>
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ) ;
theorem
:: ARYTM_1:10
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:11
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:12
for
y
,
x
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
(
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:13
for
z
,
y
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:14
for
z
,
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
(
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:15
for
y
,
x
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
(
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:16
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:17
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
definition
let
x
,
y
be ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
func
x
-
y
->
( ( ) ( )
set
)
equals
:: ARYTM_1:def 2
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
if
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
otherwise
[
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ,
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
]
: ( ( ) ( )
set
) ;
end;
theorem
:: ARYTM_1:18
for
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:19
for
x
,
y
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<>
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
[
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ,
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
]
: ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:20
for
z
,
y
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:21
for
z
,
y
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st not
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:22
for
y
,
x
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) & not
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) ;
theorem
:: ARYTM_1:23
for
y
,
x
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st not
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) & not
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:24
for
y
,
x
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
+
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:25
for
x
,
y
,
z
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:26
for
z
,
y
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:27
for
z
,
y
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st not
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<>
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
[
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ,
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
(
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
]
: ( ( ) ( )
set
)
=
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: ARYTM_1:28
for
y
,
z
,
x
being ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<>
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) &
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<='
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) &
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
<>
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) holds
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
[
{}
: ( ( ) ( )
Element
of
RAT+
: ( ( ) ( )
set
) ) ,
(
x
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
*'
(
y
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
-'
z
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
REAL+
: ( ( ) ( )
set
) )
]
: ( ( ) ( )
set
) ;