:: Some Properties of Functions Modul and Signum
:: by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990-2019 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, XREAL_0, COMPLEX1, CARD_1, XXREAL_0, ARYTM_1, ARYTM_3,
RELAT_1, SQUARE_1, REAL_1, ABSVALUE, INT_1, NAT_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, COMPLEX1,
SQUARE_1, XXREAL_0;
constructors REAL_1, SQUARE_1, COMPLEX1, INT_1, XXREAL_0;
registrations XXREAL_0, XREAL_0, ORDINAL1, NAT_1, INT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
theorems XCMPLX_0, XCMPLX_1, COMPLEX1, SQUARE_1, XREAL_1, XXREAL_0;
begin :: Absolute value
reserve x, y, z, r, s, t for Real;
definition let x be Real;
redefine func |.x.| equals :Def1:
x if 0 <= x otherwise -x;
correctness by COMPLEX1:43,70;
end;
registration
let x be non negative Real;
reduce |.x.| to x;
reducibility by Def1;
end;
theorem
|.x.| = x or |.x.| = -x by Def1;
theorem
x = 0 iff |.x.| = 0 by COMPLEX1:47;
theorem
|.x.| = -x & x <> 0 implies x < 0 by Def1;
theorem
-|.x.| <= x & x <= |.x.|
proof
per cases;
suppose
A1: x < 0;
then |.x.| = -x by Def1;
hence thesis by A1;
end;
suppose
A2: 0 <= x;
then -x <= -0;
hence thesis by A2,Def1;
end;
end;
theorem
-y <= x & x <= y iff |.x.| <= y
proof
hereby
assume that
A1: -y <= x and
A2: x <= y;
-x <= --y by A1,XREAL_1:24;
hence |.x.| <= y by A2,Def1;
end;
assume
A3: |.x.| <= y;
then
A4: 0 <= y by COMPLEX1:46;
per cases;
suppose 0 < x;
hence thesis by A3,A4,Def1;
end;
suppose
A5: x < 0;
then -x <= y by A3,Def1;
then -y <= --x by XREAL_1:24;
hence thesis by A5;
end;
suppose x = -0;
hence thesis by A3;
end;
end;
theorem
x <> 0 implies |.x.| * |.1/x.| = 1
proof
assume x <> 0;
then |.x.| * |.1/x.| = |.x * (1/x).| & |.x * (1/x).| = |.1.|
by COMPLEX1:65,XCMPLX_1:106;
hence thesis;
end;
theorem
|.1/x.| = 1/|.x.| by COMPLEX1:80;
theorem :: SQUARE_1:98
0 <= x*y implies sqrt (x*y) = sqrt |.x.|*sqrt |.y.|
proof
assume 0 <= x*y;
then |.x*y.| = x*y by Def1;
then
A1: |.x.|*|.y.| = x*y by COMPLEX1:65;
0 <= |.x.| & 0 <= |.y.| by COMPLEX1:46;
hence thesis by A1,SQUARE_1:29;
end;
theorem
|.x.| <= z & |.y.| <= t implies |.x+y.| <= z + t
proof
assume |.x.| <= z & |.y.| <= t;
then |.x+y.| <= |.x.| + |.y.| & |.x.| + |.y.| <= z + t by COMPLEX1:56
,XREAL_1:7;
hence thesis by XXREAL_0:2;
end;
theorem :: SQUARE_1:100
0 < x/y implies sqrt (x/y) = sqrt |.x.| / sqrt |.y.|
proof
assume 0 < x/y;
then x/y = |.x/y.| by Def1;
then
A1: x/y = |.x.|/|.y.| by COMPLEX1:67;
0 <= |.x.| & 0 <= |.y.| by COMPLEX1:46;
hence thesis by A1,SQUARE_1:30;
end;
theorem
0 <= x * y implies |.x+y.| = |.x.| + |.y.|
proof
assume
A1: 0 <= x * y;
per cases by A1;
suppose
x * y = 0;
then x = 0 or y = 0 by XCMPLX_1:6;
hence thesis;
end;
suppose
A5: 0 < x * y;
then
A6: x <> 0 & y <> 0;
per cases by A5,A6;
suppose that
A7: 0 < x & 0 < y;
|.x.| = x & |.y.| = y by A7,Def1;
hence thesis by A7,Def1;
end;
suppose that
A8: x < 0 and
A9: y < 0;
|.x.| = -x by A8,Def1;
then |.x.| + |.y.| = (-1) * x + -(1 * y) by A9,Def1
.= - ( x + y );
hence thesis by A8,A9,Def1;
end;
end;
end;
theorem
|.x+y.| = |.x.| + |.y.| implies 0 <= x * y
proof
A1: x * y < 0 implies x < 0 & 0 < y or 0 < x & y < 0
proof
assume
A2: x * y < 0;
then x <> 0 & y <> 0;
hence thesis by A2;
end;
A3: x < 0 & 0 < y & x + y < 0 implies |.x+y.| <> |.x.| + |.y.|
proof
assume that
A4: x < 0 and
A5: 0 < y and
A6: x + y < 0;
-(1 * x) + -y < -x + y by A5,XREAL_1:6;
then
A7: -( 1 * ( x + y ) ) < -x + y;
|.x.| = -x & |.y.| = y by A4,A5,Def1;
hence thesis by A6,A7,Def1;
end;
A8: 0 < x & y < 0 & x + y < 0 implies |.x+y.| <> |.x.| + |.y.|
proof
assume that
A9: 0 < x and
A10: y < 0 and
A11: x + y < 0;
-(1 * x) + -y < x + -y by A9,XREAL_1:6;
then
A12: - (1 * ( x + y )) < x + -y;
|.x.| = x & |.y.| = -y by A9,A10,Def1;
hence thesis by A11,A12,Def1;
end;
A13: 0 < x & y < 0 & 0 <= x + y implies |.x+y.| <> |.x.| + |.y.|
proof
assume that
A14: 0 < x and
A15: y < 0 and
A16: 0 <= x + y;
A17: |.y.| = -y by A15,Def1;
x + y < x + -y & |.x.| = x by A14,A15,Def1,XREAL_1:6;
hence thesis by A16,A17,Def1;
end;
A18: x < 0 & 0 < y & 0 <= x + y implies |.x+y.| <> |.x.| + |.y.|
proof
assume that
A19: x < 0 and
A20: 0 < y and
A21: 0 <= x + y;
A22: |.y.| = y by A20,Def1;
x + y < -x + y & |.x.| = -x by A19,Def1,XREAL_1:6;
hence thesis by A21,A22,Def1;
end;
assume |.x+y.| = |.x.| + |.y.| & 0 > x * y;
hence contradiction by A1,A3,A18,A8,A13;
end;
theorem
|.x+y.|/(1 + |.x+y.|) <= |.x.|/(1 + |.x.|) + |.y.|/(1 + |.y.|)
proof
A1: s <= t & 0 < 1 + s & 0 < 1 + t implies s/(1 + s) <= t/(1 + t)
proof
assume that
A2: s <= t and
A3: 0 < 1 + s and
A4: 0 < 1 + t;
s * 1 + s * t <= t + s * t by A2,XREAL_1:6;
then s * (1 + t) * (1 + s)" <= t * (1 + s) * (1 + s)" by A3,XREAL_1:64;
then s * (1 + t) * (1 + s)" <= t * ((1 + s) * (1 + s)");
then s * (1 + t) * (1 + s)" <= t * 1 by A3,XCMPLX_0:def 7;
then (s * (1 + s)") * (1 + t) * (1 + t)" <= t * (1 + t)" by A4,XREAL_1:64;
then (s * (1 + s)") * ((1 + t) * (1 + t)") <= t * (1 + t)";
then (s * (1 + s)") * 1 <= t * (1 + t)" by A4,XCMPLX_0:def 7;
then s/(1 + s) <= t * (1 + t)" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
set a = |.x.|, b = |.y.|, c = |.x+y.|;
A5: 0 <= a by COMPLEX1:46;
A6: 0 <= b by COMPLEX1:46;
A7: 0 + 0 < 1 + a by COMPLEX1:46,XREAL_1:8;
A8: 0 < 1 + a & 0 < 1 + a + b implies a/(1 + a + b) <= a/(1 + a)
proof
assume that
A9: 0 < 1 + a and
A10: 0 < 1 + a + b;
0 + a <= a * b + a by A5,A6,XREAL_1:6;
then a * 1 + a * a <= a * (1 + b) + a * a by XREAL_1:6;
then a * (1 + a) * (1 + a)" <= a * (1 + a + b) * (1 + a)" by A9,XREAL_1:64;
then a * ((1 + a) * (1 + a)") <= a * (1 + a + b) * (1 + a)";
then a * 1 <= a * (1 + a + b) * (1 + a)" by A7,XCMPLX_0:def 7;
then a * (1 + a + b)" <= (a * (1 + a)") * (1 + a + b) * (1 + a + b)" by A10
,XREAL_1:64;
then a * (1 + a + b)" <= (a * (1 + a)") * ((1 + a + b) * (1 + a + b)");
then a * (1 + a + b)" <= (a * (1 + a)") * 1 by A5,A6,XCMPLX_0:def 7;
then a/(1 + a + b) <= a * (1 + a)" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
A11: 0 + 0 < 1 + b by COMPLEX1:46,XREAL_1:8;
A12: 0 < 1 + b & 0 < 1 + a + b implies b/(1 + a + b) <= b/(1 + b)
proof
assume that
A13: 0 < 1 + b and
A14: 0 < 1 + a + b;
0 + b <= a * b + b by A5,A6,XREAL_1:6;
then b * 1 + b * b <= (1 + a) * b + b * b by XREAL_1:6;
then (b * (1 + b)) * (1 + b)" <= (b * (1 + a + b)) * (1 + b)" by A13,
XREAL_1:64;
then b * ((1 + b) * (1 + b)") <= (b * (1 + a + b)) * (1 + b)";
then b * 1 <= (b * (1 + a + b)) * (1 + b)" by A11,XCMPLX_0:def 7;
then
b * (1 + a + b)" <= ((b * (1 + b)") * (1 + a + b )) * (1 + a + b)" by A14,
XREAL_1:64;
then b * (1 + a + b)" <= (b * (1 + b)") * ((1 + a + b) *(1 + a + b)");
then b * (1 + a + b)" <= (b * (1 + b)") * 1 by A5,A6,XCMPLX_0:def 7;
then b/(1 + a + b) <= b * (1 + b)" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
0 + 0 < 1 + c by COMPLEX1:46,XREAL_1:8;
then
A15: c/(1 + c) <= (a + b)/(1 + (a + b)) by A5,A6,A1,COMPLEX1:56;
(a + b)/(1 + a + b) = a/(1 + a + b) + b/(1 + a + b) by XCMPLX_1:62;
then (a + b)/(1 + a + b) <= a/(1 + a) + b/(1 + b) by A6,A7,A8,A12,XREAL_1:7;
hence thesis by A15,XXREAL_0:2;
end;
:: Signum function
definition
let x;
func sgn x -> Real equals
:Def2:
1 if 0 < x, -1 if x < 0 otherwise 0;
coherence;
consistency;
projectivity;
end;
registration
let x;
cluster sgn x -> integer;
coherence
proof
x = 0 or x > 0 or x < 0;
hence thesis by Def2;
end;
end;
theorem
sgn x = 1 implies 0 < x
proof
assume that
A1: sgn x = 1 and
A2: 0 >= x;
x < 0 or x = 0 by A2;
hence contradiction by A1,Def2;
end;
theorem
sgn x = -1 implies x < 0
proof
assume that
A1: sgn x = -1 and
A2: x >= 0;
0 < x or x = 0 by A2;
hence contradiction by A1,Def2;
end;
theorem Th16:
sgn x = 0 implies x = 0
proof
assume that
A1: sgn x = 0 and
A2: x <> 0;
0 < x or x < 0 by A2;
hence contradiction by A1,Def2;
end;
theorem
x = |.x.| * sgn x
proof
A1: 0 < x implies x = |.x.| * sgn x
proof
assume
A2: 0 < x;
then |.x.| = x by Def1;
then |.x.| * sgn x = x * 1 by A2,Def2;
hence thesis;
end;
A3: x < 0 implies x = |.x.| * sgn x
proof
assume
A4: x < 0;
then |.x.| = -x by Def1;
then |.x.| * sgn x = (-x) * (-1) by A4,Def2
.= x;
hence thesis;
end;
x = 0 implies x = |.x.| * sgn x;
hence thesis by A1,A3;
end;
theorem Th18:
sgn (x * y) = sgn x * sgn y
proof
A1: 0 < x & 0 < y implies sgn (x * y) = sgn x * sgn y
proof
assume that
A2: 0 < x and
A3: 0 < y;
A4: sgn y = 1 by A3,Def2;
0 * y < x * y & sgn x = 1 by A2,A3,Def2,XREAL_1:68;
hence thesis by A4,Def2;
end;
A5: 0 < x & y < 0 implies sgn (x * y) = sgn x * sgn y
proof
assume that
A6: 0 < x and
A7: y < 0;
sgn y = -1 by A7,Def2;
then
A8: sgn x * sgn y = 1 * (-1) by A6,Def2
.= -1;
x * y < 0 * y by A6,A7,XREAL_1:69;
hence thesis by A8,Def2;
end;
A9: x < 0 & y < 0 implies sgn (x * y) = sgn x * sgn y
proof
assume that
A10: x < 0 and
A11: y < 0;
sgn y = -1 by A11,Def2;
then
A12: sgn x * sgn y = (-1) * (-1) by A10,Def2
.= 1;
x * 0 < x * y by A10,A11,XREAL_1:69;
hence thesis by A12,Def2;
end;
A13: x < 0 & 0 < y implies sgn (x * y) = sgn x * sgn y
proof
assume that
A14: x < 0 and
A15: 0 < y;
sgn y = 1 by A15,Def2;
then
A16: sgn x * sgn y = -1 by A14,Def2;
x * y < 0 * y by A14,A15,XREAL_1:68;
hence thesis by A16,Def2;
end;
x = 0 or y = 0 implies sgn (x * y) = sgn x * sgn y
proof
assume
A17: x = 0 or y = 0;
then sgn x = 0 or sgn y = 0 by Def2;
hence thesis by A17;
end;
hence thesis by A1,A5,A13,A9;
end;
::$CT
theorem
sgn (x + y) <= sgn x + sgn y + 1
proof
A1: y = 0 implies sgn (x + y) <= sgn x + sgn y + 1
proof
assume
A2: y = 0;
then sgn x + sgn y + 1 = sgn x + 0 + 1 by Def2
.= sgn x + 1;
hence thesis by A2,XREAL_1:29;
end;
A3: 0 < x & 0 < y implies sgn (x + y) <= sgn x + sgn y + 1
proof
sgn x < sgn x + 1 by XREAL_1:29;
then
A4: sgn x + 0 < sgn x + 1 + 1 by XREAL_1:8;
assume
A5: 0 < x & 0 < y;
then sgn x = 1 & sgn y = 1 by Def2;
hence thesis by A5,A4,Def2;
end;
A6: x < 0 & 0 < y implies sgn (x + y) <= sgn x + sgn y + 1
proof
assume that
A7: x < 0 and
A8: 0 < y;
sgn x = -1 by A7,Def2;
then
A9: sgn x + sgn y + 1 = 1 by A8,Def2;
x + y < 0 or x + y = 0 or 0 < x + y;
hence thesis by A9,Def2;
end;
A10: 0 < x & y < 0 implies sgn (x + y) <= sgn x + sgn y +1
proof
assume that
A11: 0 < x and
A12: y < 0;
sgn x = 1 by A11,Def2;
then
A13: sgn x + sgn y + 1 = 1 + -1 + 1 by A12,Def2
.= 1;
x + y < 0 or x + y = 0 or 0 < x + y;
hence thesis by A13,Def2;
end;
A14: x < 0 & y < 0 implies sgn (x + y) <= sgn x + sgn y + 1
proof
assume that
A15: x < 0 and
A16: y < 0;
sgn y = -1 by A16,Def2;
then sgn x + sgn y + 1 = -1 by A15,Def2;
hence thesis by A15,A16,Def2;
end;
x = 0 implies sgn (x + y) <= sgn x + sgn y + 1
proof
assume
A17: x = 0;
then sgn x + sgn y + 1 = 0 + sgn y + 1 by Def2
.= sgn y + 1;
hence thesis by A17,XREAL_1:29;
end;
hence thesis by A3,A10,A6,A14,A1;
end;
theorem Th20:
x <> 0 implies sgn x * sgn (1/x) = 1
proof
assume x <> 0;
then sgn ( x * (1/x) ) = sgn 1 by XCMPLX_1:106;
then sgn ( x * (1/x) ) = 1 by Def2;
hence thesis by Th18;
end;
theorem Th21:
1/(sgn x) = sgn (1/x)
proof
per cases;
suppose
A1: x = 0;
hence 1/(sgn x) = 1/0 by Def2
.= sgn (1/x) by A1,Def2;
end;
suppose
A2: x <> 0;
then (sgn x * sgn (1/x)) * (1/(sgn x)) = 1 * (1/(sgn x)) by Th20;
then sgn (1/x) * (sgn x * (1/(sgn x))) = 1/(sgn x);
then sgn (1/x) * 1 = 1 /(sgn x) by A2,Th16,XCMPLX_1:106;
hence thesis;
end;
end;
theorem
sgn x + sgn y - 1 <= sgn ( x + y )
proof
A1: x = 0 or y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
proof
A2: y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
proof
A3: sgn x - 1 < sgn x + -1 + 1 by XREAL_1:29;
assume
A4: y = 0;
then sgn x + sgn y - 1 = sgn x + 0 - 1 by Def2
.= sgn x - 1;
hence thesis by A4,A3;
end;
A5: x = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
proof
A6: sgn y - 1 < sgn y + -1 + 1 by XREAL_1:29;
assume
A7: x = 0;
then sgn x + sgn y - 1 = 0 + sgn y - 1 by Def2
.= sgn y - 1;
hence thesis by A7,A6;
end;
assume x = 0 or y = 0;
hence thesis by A5,A2;
end;
A8: x < 0 & y < 0 implies sgn x + sgn y - 1 <= sgn (x + y)
proof
assume that
A9: x < 0 and
A10: y < 0;
sgn x = -1 by A9,Def2;
then
A11: sgn x = sgn (x + y) by A9,A10,Def2;
A12: sgn (x + y) + -1 - 1 < sgn (x + y) + -1 - 1 + 1 & sgn (x + y) + -1 <
sgn (x + y) + -1 + 1 by XREAL_1:29;
sgn y = -1 by A10,Def2;
hence thesis by A11,A12,XXREAL_0:2;
end;
A13: 0 < x & y < 0 implies sgn x + sgn y - 1 <= sgn (x + y)
proof
assume that
A14: 0 < x and
A15: y < 0;
sgn x = 1 by A14,Def2;
then
A16: sgn x + sgn y = 1 + -1 by A15,Def2
.= 0;
x + y < 0 or x + y = 0 or 0 < x + y;
hence thesis by A16,Def2;
end;
A17: x < 0 & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
proof
assume that
A18: x < 0 and
A19: 0 < y;
sgn x = -1 by A18,Def2;
then
A20: sgn x + sgn y = -1 + 1 by A19,Def2
.= 0;
x + y < 0 or x + y = 0 or 0 < x + y;
hence thesis by A20,Def2;
end;
0 < x & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
proof
assume that
A21: 0 < x and
A22: 0 < y;
sgn y = 1 by A22,Def2;
then sgn x + sgn y - 1 = 1 by A21,Def2;
hence thesis by A21,A22,Def2;
end;
hence thesis by A8,A17,A13,A1;
end;
theorem
sgn x = sgn (1/x)
proof
A1: 0 < x implies sgn x = sgn (1/x)
proof
assume
A2: 0 < x;
sgn (1/x) = 1/(sgn x) by Th21;
then sgn (1/x) = 1/1 by A2,Def2
.= 1;
hence thesis by A2,Def2;
end;
x < 0 implies sgn x = sgn (1/x)
proof
assume
A3: x < 0;
then sgn x = -1 by Def2;
then sgn (1/x) = 1/(-1) by Th21;
hence thesis by A3,Def2;
end;
hence thesis by A1;
end;
theorem
sgn (x/y) = (sgn x)/(sgn y)
proof
per cases;
suppose
A1: y = 0;
hence sgn (x/y) = sgn (x*0") by XCMPLX_0:def 9
.= (sgn x)*0" by Def2
.= (sgn x)/0 by XCMPLX_0:def 9
.= (sgn x)/(sgn y) by A1,Def2;
end;
suppose
A2: y <> 0;
x/y = (x/y) * 1 .= (x/y) * (y * (1/y)) by A2,XCMPLX_1:106
.= ((x/y) * y) * (1/y)
.= x * (1/y) by A2,XCMPLX_1:87;
then sgn (x/y) = sgn x * sgn (1/y) by Th18
.= ((sgn x)/1) * (1/(sgn y)) by Th21
.= (sgn x * 1)/(1 * sgn y) by XCMPLX_1:76
.= (sgn x)/(1 * sgn y);
hence thesis;
end;
end;
:: from SCMPDS_9. 2008.05.06, A.T.
theorem
0 <= r + |.r.|
proof
A1: 0 <= |.r.| by COMPLEX1:46;
|.r.| + |.r.| = r + |.r.| or |.r.| + r = -r + r by Def1;
hence thesis by A1;
end;
theorem
0 <= -r + |.r.|
proof
-r >= -|.r.| by XREAL_1:24,COMPLEX1:76;
then -r+|.r.| >= -|.r.|+|.r.| by XREAL_1:7;
hence thesis;
end;
theorem
|.r.| = |.s.| implies r = s or r = -s
proof
assume
A1: |.r.| = |.s.|;
assume
A2: r <> s;
per cases by Def1;
suppose
|.r.| = r & |.s.| = s;
hence thesis by A1,A2;
end;
suppose
|.r.| = r & |.s.| = -s;
hence thesis by A1;
end;
suppose
|.r.| = -r & |.s.| = s;
hence thesis by A1;
end;
suppose
|.r.| = -r & |.s.| = -s;
hence thesis by A1,A2;
end;
end;
theorem
for m being Nat holds m = |.m.|;
:: from JORDAN2C, 2011.07.03, A.T,
theorem
r <= 0 implies |.r.| = -r
proof
assume r<=0;
then r < 0 or r = 0;
hence thesis by Def1;
end;