:: by Jan Popio{\l}ek

::

:: Received June 21, 1989

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

begin

definition

let x be real number ;

correctness

compatibility

for b_{1} being set 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 set 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 number holds

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

for x being real number holds

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

theorem :: ABSVALUE:13

for x, y being real number holds (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))

proof end;

:: Signum function

definition

let x be real number ;

coherence

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

consistency

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

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

projectivity

for b_{1}, b_{2} being real number 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 number ) & ( x < 0 implies - 1 is real number ) & ( not 0 < x & not x < 0 implies 0 is real number ) ) ;

consistency

for b

( b

projectivity

for b

( ( 0 < b

:: deftheorem Def2 defines sgn ABSVALUE:def 2 :

for x being real number 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 number holds

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

registration
end;

definition

let x be Real;

:: original: sgn

redefine func sgn x -> Real;

coherence

sgn x is Real by XREAL_0:def 1;

end;
:: original: sgn

redefine func sgn x -> Real;

coherence

sgn x is Real by XREAL_0:def 1;

:: from JORDAN2C, 2011.07.03, A.T,