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;