:: Some Properties of Functions Modul and Signum
:: by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let x be real number ;
redefine func |.x.| equals :Def1: :: ABSVALUE:def 1
x if  0 <= x
otherwise  - x;
correctness
compatibility
for b1 being set holds
( ( 0 <= x implies ( b1 = |.x.| iff b1 = x ) ) &amp; ( not 0 <= x implies ( b1 = |.x.| iff b1 = - x ) ) );
consistency
for b1 being set holds verum;
by COMPLEX1:43, COMPLEX1:70;
end;

:: deftheorem Def1 defines |. ABSVALUE:def_1_:_
 for x being real number holds
( ( 0 <= x implies |.x.| = x ) &amp; ( not 0 <= x implies |.x.| = - x ) );

theorem :: ABSVALUE:1
for x being real number holds
( abs x = x or abs x = - x ) by Def1;

theorem Th2: :: ABSVALUE:2
for x being real number holds
( x = 0 iff abs x = 0 ) by Def1, COMPLEX1:47;

theorem :: ABSVALUE:3
for x being real number st abs x = - x &amp; x <> 0 holds
x < 0 by Def1;

theorem :: ABSVALUE:4
for x being real number holds
( - (abs x) <= x &amp; x <= abs x )
proofend;

theorem :: ABSVALUE:5
for y, x being real number holds
( ( - y <= x &amp; x <= y ) iff abs x <= y )
proofend;

theorem :: ABSVALUE:6
for x being real number st x <> 0 holds
(abs x) * (abs (1 / x)) = 1
proofend;

theorem :: ABSVALUE:7
for x being real number holds abs (1 / x) = 1 / (abs x) by COMPLEX1:80;

theorem :: ABSVALUE:8
for x, y being real number st 0 <= x * y holds
sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y))
proofend;

theorem :: ABSVALUE:9
for x, z, y, t being real number st abs x <= z &amp; abs y <= t holds
abs (x + y) <= z + t
proofend;

theorem :: ABSVALUE:10
for x, y being real number st 0 < x / y holds
sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y))
proofend;

theorem :: ABSVALUE:11
for x, y being real number st 0 <= x * y holds
abs (x + y) = (abs x) + (abs y)
proofend;

theorem :: ABSVALUE:12
for x, y being real number st abs (x + y) = (abs x) + (abs y) holds
0 <= x * y
proofend;

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)))
proofend;

:: Signum function
definition
let x be real number ;
func sgn x ->  real number  equals :Def2: :: ABSVALUE:def 2
1 if  0 < x
- 1 if x < 0
otherwise  0 ;
coherence
 ( ( 0 < x implies 1 is real number ) &amp; ( x < 0 implies - 1 is real number ) &amp; ( not 0 < x &amp; not x < 0 implies 0 is real number ) ) ;
consistency
 for b1 being real number st 0 < x &amp; x < 0 holds
( b1 = 1 iff b1 = - 1 ) ;
projectivity
 for b1, b2 being real number st ( 0 < b2 implies b1 = 1 ) &amp; ( b2 < 0 implies b1 = - 1 ) &amp; ( not 0 < b2 &amp; not b2 < 0 implies b1 = 0 ) holds
( ( 0 < b1 implies b1 = 1 ) &amp; ( b1 < 0 implies b1 = - 1 ) &amp; ( not 0 < b1 &amp; not b1 < 0 implies b1 = 0 ) ) ;
end;

:: deftheorem Def2 defines sgn ABSVALUE:def_2_:_
 for x being real number holds
( ( 0 < x implies sgn x = 1 ) &amp; ( x < 0 implies sgn x = - 1 ) &amp; ( not 0 < x &amp; not x < 0 implies sgn x = 0 ) );

registration
let x be real number ;
cluster sgn x ->  real integer ;
coherence
 sgn x is integer
proofend;
end;

definition
let x be Real;
:: original:sgn
redefine func sgn x ->  Real;
coherence
 sgn x is Real by XREAL_0:def_1;
end;

theorem :: ABSVALUE:14
for x being real number st sgn x = 1 holds
0 < x
proofend;

theorem :: ABSVALUE:15
for x being real number st sgn x = - 1 holds
x < 0
proofend;

theorem Th16: :: ABSVALUE:16
for x being real number st sgn x = 0 holds
x = 0
proofend;

theorem :: ABSVALUE:17
for x being real number holds x = (abs x) * (sgn x)
proofend;

theorem Th18: :: ABSVALUE:18
for x, y being real number holds sgn (x * y) = (sgn x) * (sgn y)
proofend;

theorem :: ABSVALUE:19
canceled;

theorem :: ABSVALUE:20
for x, y being real number holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1
proofend;

theorem Th21: :: ABSVALUE:21
for x being real number st x <> 0 holds
(sgn x) * (sgn (1 / x)) = 1
proofend;

theorem Th22: :: ABSVALUE:22
for x being real number holds 1 / (sgn x) = sgn (1 / x)
proofend;

theorem :: ABSVALUE:23
for x, y being real number holds ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
proofend;

theorem :: ABSVALUE:24
for x being real number holds sgn x = sgn (1 / x)
proofend;

theorem :: ABSVALUE:25
for x, y being real number holds sgn (x / y) = (sgn x) / (sgn y)
proofend;

theorem :: ABSVALUE:26
for r being real number holds 0 <= r + (abs r)
proofend;

theorem :: ABSVALUE:27
for r being real number holds 0 <= (- r) + (abs r)
proofend;

theorem :: ABSVALUE:28
for r, s being real number holds
( not abs r = abs s or r = s or r = - s )
proofend;

theorem :: ABSVALUE:29
for m being Nat holds m = abs m
proofend;

:: from JORDAN2C, 2011.07.03, A.T,
theorem :: ABSVALUE:30
for r being real number st r <= 0 holds
abs r = - r
proofend;