:: Some Properties of Functions Modul and Signum
:: by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990-2021 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;
begin :: Absolute value
reserve x, y, z, r, s, t for Real;
definition let x be Real;
redefine func |.x.| equals
:: ABSVALUE:def 1
x if 0 <= x otherwise -x;
end;
registration
let x be non negative Real;
reduce |.x.| to x;
end;
theorem :: ABSVALUE:1
|.x.| = x or |.x.| = -x;
theorem :: ABSVALUE:2
x = 0 iff |.x.| = 0;
theorem :: ABSVALUE:3
|.x.| = -x & x <> 0 implies x < 0;
theorem :: ABSVALUE:4
-|.x.| <= x & x <= |.x.|;
theorem :: ABSVALUE:5
-y <= x & x <= y iff |.x.| <= y;
theorem :: ABSVALUE:6
x <> 0 implies |.x.| * |.1/x.| = 1;
theorem :: ABSVALUE:7
|.1/x.| = 1/|.x.|;
theorem :: ABSVALUE:8 :: SQUARE_1:98
0 <= x*y implies sqrt (x*y) = sqrt |.x.|*sqrt |.y.|;
theorem :: ABSVALUE:9
|.x.| <= z & |.y.| <= t implies |.x+y.| <= z + t;
theorem :: ABSVALUE:10 :: SQUARE_1:100
0 < x/y implies sqrt (x/y) = sqrt |.x.| / sqrt |.y.|;
theorem :: ABSVALUE:11
0 <= x * y implies |.x+y.| = |.x.| + |.y.|;
theorem :: ABSVALUE:12
|.x+y.| = |.x.| + |.y.| implies 0 <= x * y;
theorem :: ABSVALUE:13
|.x+y.|/(1 + |.x+y.|) <= |.x.|/(1 + |.x.|) + |.y.|/(1 + |.y.|);
:: Signum function
definition
let x;
func sgn x -> Real equals
:: ABSVALUE:def 2
1 if 0 < x, -1 if x < 0 otherwise 0;
projectivity;
end;
registration
let x;
cluster sgn x -> integer;
end;
theorem :: ABSVALUE:14
sgn x = 1 implies 0 < x;
theorem :: ABSVALUE:15
sgn x = -1 implies x < 0;
theorem :: ABSVALUE:16
sgn x = 0 implies x = 0;
theorem :: ABSVALUE:17
x = |.x.| * sgn x;
theorem :: ABSVALUE:18
sgn (x * y) = sgn x * sgn y;
::$CT
theorem :: ABSVALUE:20
sgn (x + y) <= sgn x + sgn y + 1;
theorem :: ABSVALUE:21
x <> 0 implies sgn x * sgn (1/x) = 1;
theorem :: ABSVALUE:22
1/(sgn x) = sgn (1/x);
theorem :: ABSVALUE:23
sgn x + sgn y - 1 <= sgn ( x + y );
theorem :: ABSVALUE:24
sgn x = sgn (1/x);
theorem :: ABSVALUE:25
sgn (x/y) = (sgn x)/(sgn y);
:: from SCMPDS_9. 2008.05.06, A.T.
theorem :: ABSVALUE:26
0 <= r + |.r.|;
theorem :: ABSVALUE:27
0 <= -r + |.r.|;
theorem :: ABSVALUE:28
|.r.| = |.s.| implies r = s or r = -s;
theorem :: ABSVALUE:29
for m being Nat holds m = |.m.|;
:: from JORDAN2C, 2011.07.03, A.T,
theorem :: ABSVALUE:30
r <= 0 implies |.r.| = -r;