:: Some Properties of Extended Real Numbers Operations: absolute
:: value, min and max
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 15, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUPINF_1, REAL_1, COMPLEX1, CARD_1, XXREAL_0, ARYTM_1,
ARYTM_3, RELAT_1, MESFUNC1, MEASURE6;
notations NUMBERS, XXREAL_0, COMPLEX1, REAL_1, SUPINF_1, SUPINF_2, MEASURE6,
EXTREAL1, MESFUNC1;
constructors REAL_1, COMPLEX1, SUPINF_2, MEASURE6, EXTREAL1, MESFUNC1,
SUPINF_1, BINOP_2;
registrations NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XBOOLE_0, XXREAL_3,
EXTREAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions SUPINF_2, XXREAL_3;
theorems MEASURE6, SUPINF_2, EXTREAL1, MESFUNC1, ABSVALUE, XCMPLX_1, COMPLEX1,
XREAL_1, XXREAL_0, XXREAL_3;
begin :: Preliminaries
reserve x,y,w,z for R_eal,
a for Real;
begin :: Basic properties of absolute value for extended real numbers
theorem Th1:
x = a implies |.x.| = abs(a)
proof
assume
A1: x = a;
per cases;
suppose
0 <= x;
then |.x.| = a by A1,EXTREAL1:def 1;
hence thesis by ABSVALUE:def 1;
end;
suppose
A2: not 0 <= x;
then |.x.| = -x by EXTREAL1:4
.= -a by A1,SUPINF_2:2;
hence thesis by A1,A2,ABSVALUE:def 1;
end;
end;
theorem
|.x.| = x or |.x.| = -x by EXTREAL1:def 1;
theorem
0 <= |.x.|;
theorem Th4:
x <> 0 implies 0 < |.x.|
proof
assume
A1: x <> 0;
per cases;
suppose
0 <= x;
hence thesis by A1,EXTREAL1:def 1;
end;
suppose
A2: not 0 <= x;
then 0 < -x;
hence thesis by A2,EXTREAL1:def 1;
end;
end;
theorem
x = 0 iff |.x.| = 0 by Th4,EXTREAL1:def 1;
theorem
|.x.| = -x & x <> 0 implies x < 0;
theorem Th7:
x <= 0 implies |.x.| = -x
proof
assume
A1: x <= 0;
per cases by A1;
suppose
x < 0;
hence thesis by EXTREAL1:def 1;
end;
suppose
A2: x = 0;
then -0 = -x;
hence thesis by A2,EXTREAL1:def 1;
end;
end;
theorem
|.x * y.| = |.x.| * |.y.|
proof
per cases;
suppose
x = 0;
then |.x.| = 0 & |.x * y.| = 0 by EXTREAL1:def 1;
hence thesis;
end;
suppose
A1: 0 < x;
per cases;
suppose
y = 0;
then |.y.| = 0 & |.x * y.| = 0 by EXTREAL1:def 1;
hence thesis;
end;
suppose
0 < y;
then
A2: |.y.| = y by EXTREAL1:def 1;
|.x.| = x by A1,EXTREAL1:def 1;
hence thesis by A2,EXTREAL1:def 1;
end;
suppose
A3: y < 0;
then
A4: |.y.| = -y by EXTREAL1:def 1;
|.x.| = x by A1,EXTREAL1:def 1;
then |.x.| * |.y.| = -(x * y) by A4,XXREAL_3:92;
hence thesis by A1,A3,EXTREAL1:def 1;
end;
end;
suppose
A5: x < 0;
per cases;
suppose
y = 0;
then |.y.| = 0 & |.x * y.| = 0 by EXTREAL1:def 1;
hence thesis;
end;
suppose
A6: 0 < y;
then |.y.| = y by EXTREAL1:def 1;
then
A7: |.x.| * |.y.| = (-x) * y by A5,EXTREAL1:def 1;
|.x * y.| = -(x * y) by A5,A6,EXTREAL1:def 1;
hence thesis by A7,XXREAL_3:92;
end;
suppose
y < 0;
then |.y.| = -y by EXTREAL1:def 1;
then |.x.| * |.y.| = (-x) * (-y) by A5,EXTREAL1:def 1;
then |.x.| * |.y.| = -(x * (-y)) by XXREAL_3:92
.= -(-(x * y)) by XXREAL_3:92;
hence thesis by EXTREAL1:def 1;
end;
end;
end;
theorem Th9:
-|.x.| <= x & x <= |.x.|
proof
per cases;
suppose
A1: 0 <= x;
thus thesis by A1,EXTREAL1:def 1;
end;
suppose
not 0 <= x;
then |.x.|=-x by EXTREAL1:def 1;
hence thesis;
end;
end;
theorem Th10:
|.x.| < y implies -y < x & x < y
proof
assume
A1: |.x.| < y;
per cases;
suppose 0 <= x;
hence thesis by A1,EXTREAL1:def 1;
end;
suppose
A2: not 0 <= x;
then |.x.|=-x by EXTREAL1:def 1;
hence thesis by A1,A2,XXREAL_3:60;
end;
end;
theorem Th11:
-y < x & x < y implies 0 < y & |.x.| < y
proof
assume that
A1: -y < x and
A2: x < y;
per cases;
suppose
0 <= x;
hence thesis by A2,EXTREAL1:def 1;
end;
suppose
A3: not 0 <= x;
-x < y by A1,XXREAL_3:60;
hence thesis by A3,EXTREAL1:def 1;
end;
end;
theorem Th12:
-y <= x & x <= y iff |.x.| <= y
proof
A1: -y <= x & x <= y implies |.x.| <= y
proof
assume that
A2: -y <= x and
A3: x <= y;
per cases;
suppose
0 <= x;
hence thesis by A3,EXTREAL1:def 1;
end;
suppose
A4: not 0 <= x;
-x <= y by A2,XXREAL_3:60;
hence thesis by A4,EXTREAL1:def 1;
end;
end;
|.x.| <= y implies -y <= x & x <= y
proof
assume
A5: |.x.| <= y;
per cases by A5,XXREAL_0:1;
suppose
|.x.| = y;
hence thesis by Th9;
end;
suppose
|.x.| < y;
hence thesis by Th10;
end;
end;
hence thesis by A1;
end;
theorem Th13:
|.x + y.| <= |.x.| + |.y.|
proof
A1: -|.x.| <= x & -|.y.| <= y by Th9;
A2: x <= |.x.| & y <= |.y.| by Th9;
A3: -|.x.|-|.y.| = -(|.x.|+|.y.|) by XXREAL_3:25;
x + y <= |.x.| + |.y.| & -|.x.|+(-|.y.|) <= x + y by A1,A2,XXREAL_3:36;
hence thesis by A3,Th12;
end;
theorem Th14:
-infty < x & x < +infty & x <> 0 implies |.x.|*|. 1./x .| = 1.
proof
assume that
A1: -infty < x & x < +infty and
A2: x <> 0;
reconsider a = x as Real by A1,XXREAL_0:14;
A3: 1./x = 1/a by EXTREAL1:2,MESFUNC1:def 8;
per cases;
suppose
0 <= x;
then |.x.| = a & |. 1./x .| = 1/a by A3,EXTREAL1:def 1;
then |.x.|*|. 1./x .| = a * (1/a) by EXTREAL1:1;
hence thesis by A2,MESFUNC1:def 8,XCMPLX_1:106;
end;
suppose
A4: not 0 <= x;
then
A5: |.x.| = -x by EXTREAL1:def 1
.= -a by SUPINF_2:2;
|. 1./x .| = -(1./x) by A3,A4,EXTREAL1:4,XREAL_1:142
.= -(1/a) by A3,SUPINF_2:2;
then |.x.|*|. 1./x .| = (-a) * (-(1/a)) by A5,EXTREAL1:1
.= a * (1/a);
hence thesis by A4,MESFUNC1:def 8,XCMPLX_1:106;
end;
end;
theorem
x = +infty or x = -infty implies |.x.|*|. 1./x .| = 0
proof
assume x = +infty or x = -infty;
then |. 1./x .| = 0 by EXTREAL1:def 1;
hence thesis;
end;
theorem
x <> 0 implies |. 1./x .| = 1./|.x.|
proof
assume
A1: x <> 0;
per cases;
suppose
A2: x = +infty;
then |. 1./x .| = 0 by EXTREAL1:def 1;
hence thesis by A2,EXTREAL1:3;
end;
suppose
x = -infty;
then |. 1./x .| = 0 & |.x.| = +infty by EXTREAL1:def 1,XXREAL_3:5;
hence thesis;
end;
suppose
A3: x <> +infty & x <> -infty;
A4: 0 < |.x.| by A1,Th4;
A5: x < +infty by A3,XXREAL_0:4;
-infty <= x by XXREAL_0:5;
then
A6: -infty < x by A3,XXREAL_0:1;
then -(+infty) < x by XXREAL_3:def 3;
then
A7: |.x.| < +infty by A5,Th11;
|. 1./x .|*|.x.| = 1. by A1,A6,A5,Th14;
hence thesis by A4,A7,XXREAL_3:88;
end;
end;
theorem
not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y<>0 implies |.
x/y.| = |.x.|/|.y.|
proof
assume that
A1: not((x=-infty or x=+infty) & (y=-infty or y=+infty)) and
A2: y<>0;
per cases;
suppose
A3: x = +infty;
A4: -infty < y by A1,A3,XXREAL_0:12,14;
per cases by A2;
suppose
A5: 0 < y;
then x / y = +infty by A3,A1,XXREAL_3:83;
then
A6: |.x/y.| = +infty by EXTREAL1:3;
|.y.| = y by A5,EXTREAL1:3;
hence thesis by A3,A1,A5,A6,XXREAL_3:83;
end;
suppose
A7: y < 0;
then |.y.| = -y by EXTREAL1:4;
then
A8: |.y.| < +infty by A4,XXREAL_3:5,38;
x / y = -infty by A3,A1,A7,XXREAL_3:85;
then |.x/y.| = +infty by EXTREAL1:4,XXREAL_3:5;
hence thesis by A8,A2,A3,Th4,XXREAL_3:83;
end;
end;
suppose
A9: x = -infty;
A10: -infty < y by A1,A9,XXREAL_0:12,14;
per cases by A2;
suppose
A11: 0 < y;
then
A12: x / y = -infty by A9,A1,XXREAL_3:86;
A13: |.x.| = +infty by A9,EXTREAL1:4,XXREAL_3:5;
|.y.| = y by A11,EXTREAL1:3;
hence thesis by A9,A1,A11,A12,A13,XXREAL_3:83;
end;
suppose
A14: y < 0;
then |.y.| = -y by EXTREAL1:4;
then
A15: |.y.| < +infty by A10,XXREAL_3:5,38;
A16: x / y = +infty by A9,A1,A14,XXREAL_3:84;
0 < |.y.| & |.x.| = +infty by A2,A9,Th4,EXTREAL1:4,XXREAL_3:5;
hence thesis by A15,A16,XXREAL_3:83;
end;
end;
suppose
x <> +infty & x <> -infty;
then reconsider a = x as Real by XXREAL_0:14;
per cases;
suppose
y = +infty;
then |.x/y.| = 0 & |.y.| = +infty by EXTREAL1:def 1;
hence thesis;
end;
suppose
y = -infty;
then |.x/y.| = 0 & |.y.| = +infty by EXTREAL1:def 1,XXREAL_3:5;
hence thesis;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Real by XXREAL_0:14;
|.x.| = abs(a) & |.y.| = abs b by Th1;
then
A17: |.x.|/|.y.| = abs(a)/abs(b) by EXTREAL1:2;
x / y = a / b by EXTREAL1:2;
then |.x/y.| = abs(a/b) by Th1;
hence thesis by A17,COMPLEX1:67;
end;
end;
end;
theorem Th18:
|.x.| = |.-x.|
proof
per cases;
suppose 0 < x;
then |.-x.| = -(-x) by EXTREAL1:4
.= x;
hence thesis;
end;
suppose x < 0;
then |.x.| = -x by EXTREAL1:4;
hence thesis;
end;
suppose x = 0;
hence thesis;
end;
end;
theorem Th19:
|.+infty.| = +infty & |.-infty.| = +infty
proof
thus |.+infty.| = +infty by EXTREAL1:3;
--infty = +infty by XXREAL_3:23;
hence thesis by EXTREAL1:4;
end;
theorem Th20:
x is Real or y is Real implies |.x.|-|.y.| <= |.x-y.|
proof
assume
A1: x is Real or y is Real;
per cases by A1;
suppose
A2: y is Real;
then (x - y) + y = x by XXREAL_3:22;
then
A3: |.x.| <= |.x-y.| + |.y.| by Th13;
reconsider b = y as Real by A2;
thus thesis by A3,XXREAL_3:42;
end;
suppose
x is Real;
then reconsider a = x as Real;
A4: |.x.| = abs a by Th1;
per cases;
suppose y = +infty or y = -infty;
hence thesis by A4,Th19,XXREAL_3:13;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Real by XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then
A5: |.x-y.| = abs(a-b) by Th1;
|.y.| = abs b by Th1;
then |.x.|-|.y.| = abs(a)-abs(b) by A4,SUPINF_2:3;
hence thesis by A5,COMPLEX1:59;
end;
end;
end;
theorem
|.x-y.| <= |.x.| + |.y.|
proof
per cases;
suppose x = +infty or x = -infty;
then |.x.| + |.y.| = +infty by XXREAL_3:def 2,Th19;
hence thesis by XXREAL_0:3;
end;
suppose
A1: x <> +infty & x <> -infty;
then reconsider a = x as Real by XXREAL_0:14;
per cases;
suppose
A2: y = +infty;
x - y = -infty by A1,A2,XXREAL_3:13;
hence thesis by A2,Th19,XXREAL_3:def 2;
end;
suppose
A3: y = -infty;
x - y = +infty by A1,A3,XXREAL_3:14;
hence thesis by A3,Th19,XXREAL_3:def 2;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Real by XXREAL_0:14;
|.x.|=abs a & |.y.|=abs b by Th1;
then
A4: |.x.|+|.y.|=abs(a)+abs(b) by SUPINF_2:1;
x - y = a - b by SUPINF_2:3;
then |.x-y.| = abs(a-b) by Th1;
hence thesis by A4,COMPLEX1:57;
end;
end;
end;
canceled;
theorem
|.x.| <= z & |.y.| <= w implies |.x+y.| <= z + w
proof
assume
A1: |.x.| <= z & |.y.| <= w;
then -z <= x & -w <= y by Th12;
then
A2: -z + -w <= x + y by XXREAL_3:36;
x <= z & y <= w by A1,Th12;
then
A3: x + y <= z + w by XXREAL_3:36;
-z -w = -(z + w) by XXREAL_3:25;
hence thesis by A3,A2,Th12;
end;
theorem
x is Real or y is Real implies |.|.x.|-|.y.|.| <= |.x-y.|
proof
A1: |.y.|-|.x.| = -(|.x.|-|.y.|) by XXREAL_3:26;
assume
A2: x is Real or y is Real;
then
A3: |.x.|-|.y.| <= |.x-y.| by Th20;
y - x = -(x - y) by XXREAL_3:26;
then
A4: |.y-x.| = |.x-y.| by Th18;
|.y.|-|.x.| <= |.y-x.| by A2,Th20;
then -|.x-y.| <= -(-(|.x.|-|.y.|)) by A4,A1,XXREAL_3:38;
hence thesis by A3,Th12;
end;
theorem
0 <= x * y implies |.x+y.| = |.x.|+|.y.|
proof
assume
A1: 0 <= x * y;
per cases by A1;
suppose
(0 <= x or 0 < x) & (0 <= y or 0 < y);
then |.x.| = x & |.y.| = y by EXTREAL1:def 1;
hence thesis by EXTREAL1:def 1;
end;
suppose
A2: (x <= 0 or x < 0) & (y <= 0 or y < 0);
then
A3: |.x+y.| = -(x + y) by Th7
.= -x -y by XXREAL_3:25;
|.x.| = -x by A2,Th7;
hence thesis by A2,A3,Th7;
end;
end;
begin
theorem
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
proof
assume that
A1: x <> +infty and
A2: y <> +infty and
A3: not ( x = +infty & y = +infty or x = -infty & y = -infty );
per cases;
suppose
A4: x = -infty;
then x + y = -infty & x - y = -infty by A2,A3,XXREAL_3:14,def 2;
then
A5: x + y - |.x - y.| = -infty by XXREAL_3:14;
A6: min(x,y) = -infty by A4,XXREAL_0:44;
R_EAL 2 = 2 by MEASURE6:def 1;
hence thesis by A6,A5,XXREAL_3:86;
end;
suppose
x <> -infty;
then reconsider a = x as Real by A1,XXREAL_0:14;
per cases;
suppose
A7: y = -infty;
then x + y = -infty & x - y = +infty by A1,A3,XXREAL_3:14,def 2;
then
A8: x + y - |.x - y.| = -infty by XXREAL_3:14;
A9: min(x,y) = -infty by A7,XXREAL_0:44;
R_EAL 2 = 2 by MEASURE6:def 1;
hence thesis by A9,A8,XXREAL_3:86;
end;
suppose
y <> -infty;
then reconsider b = y as Real by A2,XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then x + y = a + b & |.x - y.| = abs(a - b) by Th1,SUPINF_2:1;
then
A10: x + y - |.x - y.| = a + b - abs(a - b) by SUPINF_2:3;
R_EAL 2 = 2 by MEASURE6:def 1;
then (x + y - |.x - y.|) / R_EAL 2 = (a+b-abs(a-b))/2 by A10,EXTREAL1:2
;
hence thesis by COMPLEX1:73;
end;
end;
end;
theorem
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
proof
assume that
A1: x <> -infty and
A2: y <> -infty and
A3: not ( x = +infty & y = +infty or x = -infty & y = -infty );
per cases;
suppose
A4: x = +infty;
then x + y = +infty & x - y = +infty by A2,A3,XXREAL_3:13,def 2;
then
A5: x + y + |.x - y.| = +infty by XXREAL_3:def 2;
A6: max(x,y) = +infty by A4,XXREAL_0:41;
R_EAL 2 = 2 by MEASURE6:def 1;
hence thesis by A6,A5,XXREAL_3:83;
end;
suppose
x <> +infty;
then reconsider a = x as Real by A1,XXREAL_0:14;
per cases;
suppose
A7: y = +infty;
then x + y = +infty & x - y = -infty by A1,A3,XXREAL_3:13,def 2;
then
A8: x + y + |.x - y.| = +infty by XXREAL_3:def 2;
A9: max(x,y) = +infty by A7,XXREAL_0:41;
R_EAL 2 = 2 by MEASURE6:def 1;
hence thesis by A9,A8,XXREAL_3:83;
end;
suppose
y <> +infty;
then reconsider b = y as Real by A2,XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then x + y = a + b & |.x - y.| = abs(a - b) by Th1,SUPINF_2:1;
then
A10: x + y + |.x - y.| = a + b + abs(a - b) by SUPINF_2:1;
R_EAL 2 = 2 by MEASURE6:def 1;
then (x + y + |.x - y.|) / R_EAL 2 = (a+b+abs(a-b))/2 by A10,EXTREAL1:2
;
hence thesis by COMPLEX1:74;
end;
end;
end;
definition
let x,y be R_eal;
redefine func max(x,y) -> R_eal;
coherence by XXREAL_0:def 1;
redefine func min(x,y) -> R_eal;
coherence by XXREAL_0:def 1;
end;
theorem
min(x,y) + max(x,y)= x + y
proof
per cases;
suppose
A1: x <= y;
then min(x,y) = x by XXREAL_0:def 9;
hence thesis by A1,XXREAL_0:def 10;
end;
suppose
A2: not x <= y;
then min(x,y) = y by XXREAL_0:def 9;
hence thesis by A2,XXREAL_0:def 10;
end;
end;
begin ::Addenda
:: missing, 2007.07.20, A.T.
theorem Th29:
|.x.| = +infty implies x = +infty or x = -infty
proof
A1: |.x.| = x or -|.x.| = --x by EXTREAL1:def 1;
assume |.x.| = +infty;
hence thesis by A1,XXREAL_3:5;
end;
theorem
|.x.| < +infty iff x in REAL
proof
thus |.x.| < +infty implies x in REAL by Th19,XXREAL_0:14;
assume
A1: x in REAL;
assume |.x.| >= +infty;
hence contradiction by A1,Th29,XXREAL_0:4;
end;