:: by Jan Popio{\l}ek

::

:: Received June 21, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let x be Real;

correctness

compatibility

for b_{1} being object holds

( ( 0 <= x implies ( b_{1} = |.x.| iff b_{1} = x ) ) & ( not 0 <= x implies ( b_{1} = |.x.| iff b_{1} = - x ) ) );

consistency

for b_{1} being object holds verum;

by COMPLEX1:43, COMPLEX1:70;

end;
correctness

compatibility

for b

( ( 0 <= x implies ( b

consistency

for b

by COMPLEX1:43, COMPLEX1:70;

:: deftheorem Def1 defines |. ABSVALUE:def 1 :

for x being Real holds

( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

for x being Real holds

( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

theorem :: ABSVALUE:13

for x, y being Real holds |.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))

proof end;

:: Signum function

definition

let x be Real;

coherence

( ( 0 < x implies 1 is Real ) & ( x < 0 implies - 1 is Real ) & ( not 0 < x & not x < 0 implies 0 is Real ) ) ;

consistency

for b_{1} being Real st 0 < x & x < 0 holds

( b_{1} = 1 iff b_{1} = - 1 )
;

projectivity

for b_{1}, b_{2} being Real st ( 0 < b_{2} implies b_{1} = 1 ) & ( b_{2} < 0 implies b_{1} = - 1 ) & ( not 0 < b_{2} & not b_{2} < 0 implies b_{1} = 0 ) holds

( ( 0 < b_{1} implies b_{1} = 1 ) & ( b_{1} < 0 implies b_{1} = - 1 ) & ( not 0 < b_{1} & not b_{1} < 0 implies b_{1} = 0 ) )
;

end;
coherence

( ( 0 < x implies 1 is Real ) & ( x < 0 implies - 1 is Real ) & ( not 0 < x & not x < 0 implies 0 is Real ) ) ;

consistency

for b

( b

projectivity

for b

( ( 0 < b

:: deftheorem Def2 defines sgn ABSVALUE:def 2 :

for x being Real holds

( ( 0 < x implies sgn x = 1 ) & ( x < 0 implies sgn x = - 1 ) & ( not 0 < x & not x < 0 implies sgn x = 0 ) );

for x being Real holds

( ( 0 < x implies sgn x = 1 ) & ( x < 0 implies sgn x = - 1 ) & ( not 0 < x & not x < 0 implies sgn x = 0 ) );

::$CT

:: from SCMPDS_9. 2008.05.06, A.T.

:: from JORDAN2C, 2011.07.03, A.T,