:: EXTREAL2 semantic presentation
begin
begin
theorem
:: EXTREAL2:1
for
x
being ( ( ) (
ext-real
)
R_eal
)
for
a
being ( ( ) (
V11
()
V12
()
ext-real
)
Real
) st
x
: ( ( ) (
ext-real
)
R_eal
)
=
a
: ( ( ) (
V11
()
V12
()
ext-real
)
Real
) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
abs
a
: ( ( ) (
V11
()
V12
()
ext-real
)
Real
) : ( ( ) (
V11
()
V12
()
ext-real
)
M2
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) )) ;
theorem
:: EXTREAL2:2
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
x
: ( ( ) (
ext-real
)
R_eal
) or
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
-
x
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) ;
theorem
:: EXTREAL2:3
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
<=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:4
for
x
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
ext-real
)
R_eal
)
<>
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
<
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:5
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
x
: ( ( ) (
ext-real
)
R_eal
)
=
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) iff
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) ) ;
theorem
:: EXTREAL2:6
for
x
being ( ( ) (
ext-real
)
R_eal
) st
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
-
x
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
x
: ( ( ) (
ext-real
)
R_eal
)
<>
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
x
: ( ( ) (
ext-real
)
R_eal
)
<
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: EXTREAL2:7
for
x
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
ext-real
)
R_eal
)
<=
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
-
x
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:8
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
*
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
*
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:9
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
-
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
positive
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) ;
theorem
:: EXTREAL2:10
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
y
: ( ( ) (
ext-real
)
R_eal
) holds
(
-
y
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
y
: ( ( ) (
ext-real
)
R_eal
) ) ;
theorem
:: EXTREAL2:11
for
y
,
x
being ( ( ) (
ext-real
)
R_eal
) st
-
y
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
y
: ( ( ) (
ext-real
)
R_eal
) holds
(
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
<
y
: ( ( ) (
ext-real
)
R_eal
) &
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
y
: ( ( ) (
ext-real
)
R_eal
) ) ;
theorem
:: EXTREAL2:12
for
y
,
x
being ( ( ) (
ext-real
)
R_eal
) holds
( (
-
y
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<=
y
: ( ( ) (
ext-real
)
R_eal
) ) iff
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
y
: ( ( ) (
ext-real
)
R_eal
) ) ;
theorem
:: EXTREAL2:13
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
+
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:14
for
x
being ( ( ) (
ext-real
)
R_eal
) st
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
x
: ( ( ) (
ext-real
)
R_eal
) &
x
: ( ( ) (
ext-real
)
R_eal
)
<
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
x
: ( ( ) (
ext-real
)
R_eal
)
<>
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
*
|.
(
1.
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
x
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
1.
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:15
for
x
being ( ( ) (
ext-real
)
R_eal
) st (
x
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) or
x
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
*
|.
(
1.
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
x
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) ;
theorem
:: EXTREAL2:16
for
x
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
ext-real
)
R_eal
)
<>
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
|.
(
1.
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
x
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
1.
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:17
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st ( ( not
x
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) & not
x
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) or ( not
y
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) & not
y
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) ) &
y
: ( ( ) (
ext-real
)
R_eal
)
<>
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) )) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
/
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:18
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
|.
(
-
x
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:19
(
|.
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
|.
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) ;
theorem
:: EXTREAL2:20
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st (
x
: ( ( ) (
ext-real
)
R_eal
) is ( ( ) (
V11
()
V12
()
ext-real
)
Real
) or
y
: ( ( ) (
ext-real
)
R_eal
) is ( ( ) (
V11
()
V12
()
ext-real
)
Real
) ) holds
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
-
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
-
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:21
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
-
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
+
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:22
canceled;
theorem
:: EXTREAL2:23
for
x
,
z
,
y
,
w
being ( ( ) (
ext-real
)
R_eal
) st
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
z
: ( ( ) (
ext-real
)
R_eal
) &
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
w
: ( ( ) (
ext-real
)
R_eal
) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
z
: ( ( ) (
ext-real
)
R_eal
)
+
w
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:24
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st (
x
: ( ( ) (
ext-real
)
R_eal
) is ( ( ) (
V11
()
V12
()
ext-real
)
Real
) or
y
: ( ( ) (
ext-real
)
R_eal
) is ( ( ) (
V11
()
V12
()
ext-real
)
Real
) ) holds
|.
(
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
-
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<=
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
-
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:25
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st
0
: ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
non
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
<=
x
: ( ( ) (
ext-real
)
R_eal
)
*
y
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) holds
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
+
|.
y
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
begin
theorem
:: EXTREAL2:26
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
ext-real
)
R_eal
)
<>
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
<>
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) & not (
x
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) & not (
x
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) holds
min
(
x
: ( ( ) (
ext-real
)
R_eal
) ,
y
: ( ( ) (
ext-real
)
R_eal
) ) : ( ( ) (
ext-real
)
set
)
=
(
(
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
-
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
-
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
(
R_EAL
2 : ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
theorem
:: EXTREAL2:27
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) st
x
: ( ( ) (
ext-real
)
R_eal
)
<>
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
<>
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) & not (
x
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) & not (
x
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) &
y
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) holds
max
(
x
: ( ( ) (
ext-real
)
R_eal
) ,
y
: ( ( ) (
ext-real
)
R_eal
) ) : ( ( ) (
ext-real
)
set
)
=
(
(
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
+
|.
(
x
: ( ( ) (
ext-real
)
R_eal
)
-
y
: ( ( ) (
ext-real
)
R_eal
)
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
/
(
R_EAL
2 : ( ( ) (
V1
()
V10
()
V11
()
V12
()
ext-real
positive
non
negative
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V81
()
V82
() )
M3
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ,
NAT
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V42
()
V43
()
V44
() )
M2
(
K6
(
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
definition
let
x
,
y
be ( ( ) (
ext-real
)
R_eal
) ;
:: original:
max
redefine
func
max
(
x
,
y
)
->
( ( ) (
ext-real
)
R_eal
) ;
:: original:
min
redefine
func
min
(
x
,
y
)
->
( ( ) (
ext-real
)
R_eal
) ;
end;
theorem
:: EXTREAL2:28
for
x
,
y
being ( ( ) (
ext-real
)
R_eal
) holds
(
min
(
x
: ( ( ) (
ext-real
)
R_eal
) ,
y
: ( ( ) (
ext-real
)
R_eal
) )
)
: ( ( ) (
ext-real
)
R_eal
)
+
(
max
(
x
: ( ( ) (
ext-real
)
R_eal
) ,
y
: ( ( ) (
ext-real
)
R_eal
) )
)
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
x
: ( ( ) (
ext-real
)
R_eal
)
+
y
: ( ( ) (
ext-real
)
R_eal
) : ( ( ) (
ext-real
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ;
begin
theorem
:: EXTREAL2:29
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
( not
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) or
x
: ( ( ) (
ext-real
)
R_eal
)
=
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) or
x
: ( ( ) (
ext-real
)
R_eal
)
=
-infty
: ( ( ) (
V1
()
V12
()
ext-real
non
positive
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) ) ;
theorem
:: EXTREAL2:30
for
x
being ( ( ) (
ext-real
)
R_eal
) holds
(
|.
x
: ( ( ) (
ext-real
)
R_eal
)
.|
: ( ( ) (
ext-real
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) ))
<
+infty
: ( ( ) (
V1
()
V12
()
ext-real
positive
non
negative
)
M2
(
ExtREAL
: ( ( ) (
V1
()
V39
() )
set
) )) iff
x
: ( ( ) (
ext-real
)
R_eal
)
in
REAL
: ( ( ) (
V1
()
V30
()
V38
()
V39
()
V40
()
V44
() )
set
) ) ;