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

### Basic Properties of Extended Real Numbers

by
Noboru Endou,
Katsumi Wasaki, and
Yasunari Shidama

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

```environ

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

begin

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

theorem :: EXTREAL1:1
x <> +infty & x <> -infty implies x is Real;

theorem :: EXTREAL1:2
-infty <' +infty;

theorem :: EXTREAL1:3
x <' y implies x <> +infty & y <> -infty;

theorem :: EXTREAL1:4
(x = +infty iff -x = -infty) & (x = -infty iff -x = +infty);

theorem :: EXTREAL1:5
x - -y = x + y;

canceled;

theorem :: EXTREAL1:7
x <> -infty & y <> +infty & x <=' y implies x <> +infty & y <> -infty;

theorem :: EXTREAL1:8
not (x = +infty & y = -infty) & not (x = -infty & y = +infty) &
not ((y = +infty & z = -infty) or (y = -infty & z = +infty)) &
not ((x = +infty & z = -infty) or (x = -infty & z = +infty)) implies
x + y + z = x + (y + z);

theorem :: EXTREAL1:9
x + -x = 0.;

canceled;

theorem :: EXTREAL1:11
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);

begin  :: Operations "x * y","x / y", "|.x.|" in R_eal numbers

definition
let x,y be R_eal;
func x * y -> R_eal means
:: EXTREAL1:def 1
(ex a,b being Real st (x = a & y = b & it = a * b)) or
(((0. <' x & y=+infty) or (0. <' y & x=+infty) or (x <' 0. & y=-infty) or
(y <' 0. & x = -infty)) & it = +infty) or
(((x <' 0. & y=+infty) or (y <' 0. & x=+infty) or (0. <' x & y=-infty) or
(0. <' y & x = -infty)) & it = -infty) or
((x = 0. or y = 0.) & it = 0.);
end;

canceled;

theorem :: EXTREAL1:13
for x,y being R_eal holds
for a,b being Real holds
(x = a & y = b) implies x * y = a * b;

canceled 3;

theorem :: EXTREAL1:17
for x,y being R_eal holds x * y = y * x;

definition let x,y be R_eal;
redefine func x*y;
commutativity;
end;

theorem :: EXTREAL1:18
x = a implies (0 < a iff 0. <' x);

theorem :: EXTREAL1:19
x = a implies (a < 0 iff x <' 0.);

theorem :: EXTREAL1:20
(0. <' x & 0. <' y) or (x <' 0. & y <' 0.) implies 0. <' x * y;

theorem :: EXTREAL1:21
(0. <' x & y <' 0.) or (x <' 0. & 0. <' y) implies x * y <' 0.;

theorem :: EXTREAL1:22
x * y = 0. iff (x = 0. or y = 0.);

theorem :: EXTREAL1:23
x*y*z = x*(y*z);

theorem :: EXTREAL1:24
-0. = 0.;

theorem :: EXTREAL1:25
(0. <' x iff -x <' 0.) & (x <' 0. iff 0. <' -x);

theorem :: EXTREAL1:26
-(x * y) = x * (-y) & -(x * y) = (-x) * y;

theorem :: EXTREAL1:27
x <> +infty & x <> -infty & x * y = +infty implies y = +infty or y = -infty
;

theorem :: EXTREAL1:28
x <> +infty & x <> -infty & x * y = -infty implies y = +infty or y = -infty
;

theorem :: EXTREAL1:29
x <> +infty & x <> -infty implies x * (y + z) = x * y + x * z;

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

definition
let x,y be R_eal;
assume not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y <> 0.;
func x / y -> R_eal means
:: EXTREAL1:def 2
(ex a,b being Real st (x = a & y = b & it = a / b)) or
(((x=+infty & 0. <' y) or (x=-infty & y <' 0.)) & it = +infty) or
(((x=-infty & 0. <' y) or (x=+infty & y <' 0.)) & it = -infty) or
((y = -infty or y = +infty) & it = 0.);
end;

canceled;

theorem :: EXTREAL1:32
for x,y being R_eal st y <> 0. holds
for a,b being Real st x = a & y = b holds x / y = a / b;

theorem :: EXTREAL1:33
for x,y being R_eal st x <> -infty & x <> +infty &
(y = -infty or y = +infty) holds x / y = 0.;

theorem :: EXTREAL1:34
for x being R_eal st x <> -infty & x <> +infty & x <> 0. holds
x / x = 1;

definition let x be R_eal;
func |. x .| -> R_eal equals
:: EXTREAL1:def 3
x if 0. <=' x otherwise -x;
end;

canceled;

theorem :: EXTREAL1:36
for x being R_eal st 0. <' x holds |.x.| = x;

theorem :: EXTREAL1:37
for x being R_eal st x <' 0. holds |.x.| = -x;

theorem :: EXTREAL1:38
for a,b being Real holds R_EAL(a*b) = R_EAL a * R_EAL b;

theorem :: EXTREAL1:39
for a,b being Real st b <> 0 holds R_EAL(a/b) = R_EAL a / R_EAL b;

theorem :: EXTREAL1:40
for x,y being R_eal st x <=' y & (x <' +infty & -infty <' y) holds 0. <=' y-x
;

theorem :: EXTREAL1:41
for x,y being R_eal st x <' y & (x <' +infty & -infty <' y) holds 0. <' y-x
;

theorem :: EXTREAL1:42
x <=' y & 0. <=' z implies x*z <=' y*z;

theorem :: EXTREAL1:43
x <=' y & z <=' 0. implies y*z <=' x*z;

theorem :: EXTREAL1:44
x <' y & 0. <' z & z <> +infty implies x*z <' y*z;

theorem :: EXTREAL1:45
x <' y & z <' 0. & z <> -infty implies y*z <' x*z;

theorem :: EXTREAL1:46
(x is Real & y is Real) implies
(x <' y iff ex p,q being Real st (p = x & q = y & p < q));

theorem :: EXTREAL1:47
x <> -infty & y <> +infty & x <=' y & 0. <' z implies x/z <=' y/z;

theorem :: EXTREAL1:48
x <=' y & 0. <' z & z <> +infty implies x/z <=' y/z;

theorem :: EXTREAL1:49
x <> -infty & y <> +infty & x <=' y & z <' 0. implies y/z <=' x/z;

theorem :: EXTREAL1:50
x <=' y & z <' 0. & z <> -infty implies y/z <=' x/z;

theorem :: EXTREAL1:51
x <' y & 0. <' z & z <> +infty implies x/z <' y/z;

theorem :: EXTREAL1:52
x <' y & z <' 0. & z <> -infty implies y/z <' x/z;

```