:: 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;