The Mizar abstract of EXTREAL2

Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users
The abstract of the Mizar article:: Some Properties of Extended Real Numbers Operations: abs, min and max
by
Noboru Endou,
Katsumi Wasaki, and
Yasunari Shidama
Received September 15, 2000
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));
The abstract of the Mizar article:

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