The abstract of the Mizar article:

Basic Properties of Extended Real Numbers

by

Noboru Endou,

Katsumi Wasaki, and

Yasunari Shidama

Received September 7, 2000

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;