Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### Some Properties of Extended Real Numbers Operations: abs, min and max

by
Noboru Endou,
Katsumi Wasaki, and
Yasunari Shidama

MML identifier: EXTREAL2
[ Mizar article, MML identifier index ]

```environ

vocabulary SUPINF_1, RLVECT_1, ARYTM, MEASURE6, GROUP_1, ARYTM_1, ARYTM_3,
COMPLEX1, ABSVALUE, SQUARE_1;
notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, SQUARE_1, SUPINF_1,
SUPINF_2, MEASURE6, EXTREAL1, MESFUNC1;
constructors SQUARE_1, MESFUNC1, SUPINF_2, MEASURE6, EXTREAL1, REAL_1,
MEMBERED, ABSVALUE;
clusters XREAL_0, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin :: Preliminaries

reserve x,y,w,z for R_eal;
reserve a,b for Real;

canceled;

theorem :: EXTREAL2:2  :: extension of AXIOMS:19
x <> +infty & x <> -infty implies ex y st x + y = 0.;

theorem :: EXTREAL2:3  :: extension of AXIOMS:20
x <> +infty & x <> -infty & x <> 0. implies ex y st x*y = 1.;

theorem :: EXTREAL2:4
1. * x = x & x * 1. = x & R_EAL 1 * x = x & x * R_EAL 1 = x;

theorem :: EXTREAL2:5  :: extension of REAL_1:25
0. - x = -x;

canceled;

theorem :: EXTREAL2:7
0. <=' x & 0. <=' y implies 0. <=' x + y;

theorem :: EXTREAL2:8
(0. <=' x & 0. <' y) or (0. <' x & 0. <=' y) implies 0. <' x + y;

theorem :: EXTREAL2:9
x <=' 0. & y <=' 0. implies x + y <=' 0.;

theorem :: EXTREAL2:10
(x <=' 0. & y <' 0.) or (x <' 0. & y <=' 0.) implies x + y <' 0.;

theorem :: EXTREAL2:11
z <> +infty & z <> -infty & x + z = y implies x = y - z;

theorem :: EXTREAL2:12  :: extension of REAL_1:34
x <> +infty & x <> -infty & x <> 0. implies x*(1./x) = 1. & (1./x)*x = 1.;

theorem :: EXTREAL2:13  :: extension of REAL_1:36
x <> +infty & x <> -infty implies x - x = 0.;

theorem :: EXTREAL2:14   :: extension of REAL_2:6
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) implies
-(x + y) = -x + -y & -(x + y) = -y - x & -(x + y) = -x - y;

theorem :: EXTREAL2:15   :: extension of REAL_2:8
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
-(x - y) = -x + y & -(x - y) = y - x;

theorem :: EXTREAL2:16  :: extension of REAL_2:9
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
-(-x + y) = x - y & -(-x + y) = x + -y;

theorem :: EXTREAL2:17
(x = +infty & 0. <' y & y <' +infty) or (x = -infty & y <' 0. & -infty <' y)
implies x / y = +infty;

theorem :: EXTREAL2:18
(x = +infty & y <' 0. & -infty <' y) or (x = -infty & 0. <' y & y <' +infty)
implies x / y = -infty;

theorem :: EXTREAL2:19   :: extension of REAL_2:62
-infty <' y & y <' +infty & y <> 0. implies x * y / y = x & x * (y / y) = x;

theorem :: EXTREAL2:20
1. <' +infty & -infty <' 1.;

theorem :: EXTREAL2:21
x = +infty or x = -infty implies
(for y st y in REAL holds x + y <> 0.);

theorem :: EXTREAL2:22
x = +infty or x = -infty implies
for y holds x * y <> 1.;

theorem :: EXTREAL2:23
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
x + y <' +infty implies x <> +infty & y <> +infty;

theorem :: EXTREAL2:24
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
-infty <' x + y implies x <> -infty & y <> -infty;

theorem :: EXTREAL2:25
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
x - y <' +infty implies x <> +infty & y <> -infty;

theorem :: EXTREAL2:26
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
-infty <' x - y implies x <> -infty & y <> +infty;

theorem :: EXTREAL2:27
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
x + y <' z implies x <> +infty & y <> +infty & z <> -infty & x <' z - y;

theorem :: EXTREAL2:28
not ((z = +infty & y = +infty) or (z = -infty & y = -infty)) &
x <' z - y implies x <> +infty & y <> +infty & z <> -infty & x + y <' z;

theorem :: EXTREAL2:29
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
x - y <' z implies x <> +infty & y <> -infty & z <> -infty & x <' z + y;

theorem :: EXTREAL2:30
not ((z = +infty & y = -infty) or (z = -infty & y = +infty)) &
x <' z + y implies x <> +infty & y <> -infty & z <> -infty & x - y <' z;

theorem :: EXTREAL2:31
not ((x = +infty & y = -infty) or (x = -infty & y = +infty) or
(y = +infty & z = +infty) or (y = -infty & z = -infty)) &
x + y <=' z implies y <> +infty & x <=' z - y;

theorem :: EXTREAL2:32
not (x = +infty & y = -infty) & not (x = -infty & y = +infty) &
not (y = +infty & z = +infty) &
x <=' z - y implies y <> +infty & x + y <=' z;

theorem :: EXTREAL2:33
not ((x = +infty & y = +infty) or (x = -infty & y = -infty) or
(y = +infty & z = -infty) or (y = -infty & z = +infty)) &
x - y <=' z implies y <> -infty & x <=' z + y;

theorem :: EXTREAL2:34
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = -infty & z = +infty) &
x <=' z + y implies y <> -infty & x - y <=' z;

canceled 5;

theorem :: EXTREAL2:40  :: extension of REAL_1:27
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = +infty & z = -infty) & not (y = -infty & z = +infty) &
not (x = +infty & z = +infty) & not (x = -infty & z = -infty)
implies x - y - z = x - (y + z);

theorem :: EXTREAL2:41  :: extension of REAL_1:28
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = +infty & z = +infty) & not (y = -infty & z = -infty) &
not (x = +infty & z = -infty) & not (x = -infty & z = +infty)
implies x - y + z = x - (y - z);

theorem :: EXTREAL2:42
x * y <> +infty & x * y <> -infty implies x is Real or y is Real;

theorem :: EXTREAL2:43   :: extension of EXTREAL1:21
(0. <' x & 0. <' y) or (x <' 0. & y <' 0.) iff 0. <' x * y;

theorem :: EXTREAL2:44   :: extension of EXTREAL1:22
(0. <' x & y <' 0.) or (x <' 0. & 0. <' y) iff x * y <' 0.;

theorem :: EXTREAL2:45   :: extension of REAL_2:121
((0. <=' x or 0. <' x) & (0. <=' y or 0. <' y)) or
((x <=' 0. or x <' 0.) & (y <=' 0. or y <' 0.))
iff 0. <=' x * y;

theorem :: EXTREAL2:46  :: extension of REAL_2:123
((x <=' 0. or x <' 0.) & (0. <=' y or 0. <' y)) or
((0. <=' x or 0. <' x) & (y <=' 0. or y <' 0.))
iff x * y <=' 0.;

theorem :: EXTREAL2:47
(x <=' -y iff y <=' -x) & (-x <=' y iff -y <=' x);

theorem :: EXTREAL2:48
(x <' -y iff y <' -x) & (-x <' y iff -y <' x);

begin :: Basic properties of absolute value for extended real numbers

theorem :: EXTREAL2:49
x = a implies |.x.| = abs(a);

theorem :: EXTREAL2:50
|.x.| = x or |.x.| = -x;

theorem :: EXTREAL2:51   :: extension of ABSVALUE:5
0. <=' |.x.|;

theorem :: EXTREAL2:52   :: extension of ABSVALUE:6
x <> 0. implies 0. <' |.x.|;

theorem :: EXTREAL2:53  :: extension of ABSVALUE:7
x = 0. iff |.x.| = 0.;

theorem :: EXTREAL2:54  :: extension of ABSVALUE:9
|.x.| = -x & x <> 0. implies x <' 0.;

theorem :: EXTREAL2:55
x <=' 0. implies |.x.| = -x;

theorem :: EXTREAL2:56  :: extension of ABSVALUE:10
|.x * y.| = |.x.| * |.y.|;

theorem :: EXTREAL2:57   :: extension of ABSVALUE:11
-|.x.| <=' x & x <=' |.x.|;

theorem :: EXTREAL2:58
|.x.| <' y implies -y <' x & x <' y;

theorem :: EXTREAL2:59
-y <' x & x <' y implies 0. <' y & |.x.| <' y;

theorem :: EXTREAL2:60  :: extension of ABSVALUE:12
-y <=' x & x <=' y iff |.x.| <=' y;

theorem :: EXTREAL2:61   :: extension of ABSVALUE:13
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) implies
|.x + y.| <=' |.x.| + |.y.|;

theorem :: EXTREAL2:62   :: extension of ABSVALUE:14
-infty <' x & x <' +infty & x <> 0. implies |.x.|*|. 1./x .| = 1.;

theorem :: EXTREAL2:63
x = +infty or x = -infty implies |.x.|*|. 1./x .| = 0.;

theorem :: EXTREAL2:64  :: extension of ABSVALUE:15
x <> 0. implies |. 1./x .| = 1./|.x.|;

theorem :: EXTREAL2:65  :: extension of ABSVALUE:16
not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y<>0. implies
|.x/y.| = |.x.|/|.y.|;

theorem :: EXTREAL2:66   :: extension of ABSVALUE:17
|.x.| = |.-x.|;

theorem :: EXTREAL2:67
x = +infty or x = -infty implies |.x.| = +infty;

theorem :: EXTREAL2:68   :: extension of ABSVALUE:18
x is Real or y is Real implies |.x.|-|.y.| <=' |.x-y.|;

theorem :: EXTREAL2:69  :: extension of ABSVALUE:19
not((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
|.x-y.| <=' |.x.| + |.y.|;

theorem :: EXTREAL2:70  :: extension of ABSVALUE:20
|.|.x.|.| = |.x.|;

theorem :: EXTREAL2:71  :: extension of ABSVALUE:21
not((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
|.x.| <=' z & |.y.| <=' w implies |.x+y.| <=' z + w;

theorem :: EXTREAL2:72  :: extension of ABSVALUE:22
x is Real or y is Real implies |.|.x.|-|.y.|.| <=' |.x-y.|;

theorem :: EXTREAL2:73  :: extension of ABSVALUE:24
0. <=' x * y implies |.x+y.| = |.x.|+|.y.|;

begin
:: Definitions of MIN,MAX for extended real numbers and their basic properties

theorem :: EXTREAL2:74
x = a & y = b implies (b < a iff y <' x) & (b <= a iff y <=' x);

definition let x,y;
func min(x,y) -> R_eal equals
:: EXTREAL2:def 1
x if x <=' y otherwise y;
func max(x,y) -> R_eal equals
:: EXTREAL2:def 2
x if y <=' x otherwise y;
end;

theorem :: EXTREAL2:75
x = -infty or y = -infty implies min(x,y) = -infty;

theorem :: EXTREAL2:76
x = +infty or y = +infty implies max(x,y) = +infty;

theorem :: EXTREAL2:77
for x,y being R_eal holds
for a,b being Real holds
(x = a & y = b) implies min(x,y) = min(a,b) & max(x,y) = max(a,b);

theorem :: EXTREAL2:78   :: extension of SQUARE_1:32
y <=' x implies min(x,y) = y;

theorem :: EXTREAL2:79   :: extension of SQUARE_1:33
not y <=' x implies min(x,y) = x;

theorem :: EXTREAL2:80  :: extension of SQUARE_1:34
x <> +infty & y <> +infty &
not ((x = +infty & y = +infty) or (x = -infty & y = -infty))
implies min(x,y) = (x + y - |.x - y.|) / R_EAL 2;

theorem :: EXTREAL2:81   :: extension of SQUARE_1:35
min(x,y) <=' x & min(y,x) <=' x;

canceled;

theorem :: EXTREAL2:83   :: extension of SQUARE_1:37
min(x,y) = min(y,x);

theorem :: EXTREAL2:84   :: extension of SQUARE_1:38
min(x,y) = x or min(x,y) = y;

theorem :: EXTREAL2:85   :: extension of SQUARE_1:39
x <=' y & x <=' z iff x <=' min(y,z);

canceled;

theorem :: EXTREAL2:87
min(x,y) = y implies y <=' x;

theorem :: EXTREAL2:88  :: extension of SQUARE_1:40
min(x,min(y,z)) = min(min(x,y),z);

theorem :: EXTREAL2:89   :: extension of SQUARE_1:43
x <=' y implies max(x,y) = y;

theorem :: EXTREAL2:90   :: extension of SQUARE_1:44
not x <=' y implies max(x,y) = x;

theorem :: EXTREAL2:91  :: extension of SQUARE_1:45
x <> -infty & y <> -infty &
not ((x = +infty & y = +infty) or (x = -infty & y = -infty))
implies max(x,y) = (x + y + |.x - y.|) / R_EAL 2;

theorem :: EXTREAL2:92   :: extension of SQUARE_1:46
x <=' max(x,y) & x <=' max(y,x);

canceled;

theorem :: EXTREAL2:94   :: extension of SQUARE_1:48
max(x,y) = max(y,x);

theorem :: EXTREAL2:95   :: extension of SQUARE_1:49
max(x,y) = x or max(x,y) = y;

theorem :: EXTREAL2:96   :: extension of SQUARE_1:50
y <=' x & z <=' x iff max(y,z) <=' x;

canceled;

theorem :: EXTREAL2:98
max(x,y) = y implies x <=' y;

theorem :: EXTREAL2:99  :: extension of SQUARE_1:51
max(x,max(y,z)) = max(max(x,y),z);

theorem :: EXTREAL2:100  :: extension of SQUARE_1:53
min(x,y) + max(x,y) = x + y;

theorem :: EXTREAL2:101   :: extension of SQUARE_1:54
max(x,min(x,y)) = x & max(min(x,y),x) = x &
max(min(y,x),x) = x & max(x,min(y,x)) = x;

theorem :: EXTREAL2:102   :: extension of SQUARE_1:55
min(x,max(x,y)) = x & min(max(x,y),x) = x &
min(max(y,x),x) = x & min(x,max(y,x)) = x;

theorem :: EXTREAL2:103  :: extension of SQUARE_1:56
min(x,max(y,z)) = max(min(x,y),min(x,z)) &
min(max(y,z),x) = max(min(y,x),min(z,x));

theorem :: EXTREAL2:104  :: extension of SQUARE_1:57
max(x,min(y,z)) = min(max(x,y),max(x,z)) &
max(min(y,z),x) = min(max(y,x),max(z,x));
```