:: Some Properties of Functions Modul and Signum :: by Jan Popio{\l}ek :: :: Received June 21, 1989 :: Copyright (c) 1990-2018 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;