:: Some Properties of Functions Modul and Signum
:: by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990 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 ) ) & ( not 0 <= x implies ( b1 = |.x.| iff b1 = - x ) ) )
;
consistency
for b1 being set holds verum
;
by COMPLEX1:129, COMPLEX1:156;
end;

:: deftheorem Def1 defines |. ABSVALUE:def 1 :
for x being real number holds
( ( 0 <= x implies |.x.| = x ) & ( 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 :: ABSVALUE:2
canceled;

theorem :: ABSVALUE:3
canceled;

theorem :: ABSVALUE:4
canceled;

theorem :: ABSVALUE:5
canceled;

theorem :: ABSVALUE:6
canceled;

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

theorem :: ABSVALUE:8
canceled;

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

theorem :: ABSVALUE:10
canceled;

theorem :: ABSVALUE:11
for x being real number holds
( - (abs x) <= x & x <= abs x )
proof end;

theorem :: ABSVALUE:12
for y, x being real number holds
( ( - y <= x & x <= y ) iff abs x <= y )
proof end;

theorem :: ABSVALUE:13
canceled;

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

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

theorem :: ABSVALUE:16
canceled;

theorem :: ABSVALUE:17
canceled;

theorem :: ABSVALUE:18
canceled;

theorem :: ABSVALUE:19
canceled;

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

theorem :: ABSVALUE:21
for x, z, y, t being real number st abs x <= z & abs y <= t holds
abs (x + y) <= z + t
proof end;

theorem :: ABSVALUE:22
canceled;

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

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

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

theorem :: ABSVALUE:26
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;

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 ) & ( x < 0 implies - 1 is real number ) & ( not 0 < x & not x < 0 implies 0 is real number ) )
;
consistency
for b1 being real number st 0 < x & x < 0 holds
( b1 = 1 iff b1 = - 1 )
;
projectivity
for b1, b2 being real number st ( 0 < b2 implies b1 = 1 ) & ( b2 < 0 implies b1 = - 1 ) & ( not 0 < b2 & not b2 < 0 implies b1 = 0 ) holds
( ( 0 < b1 implies b1 = 1 ) & ( b1 < 0 implies b1 = - 1 ) & ( not 0 < b1 & 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 ) & ( x < 0 implies sgn x = - 1 ) & ( not 0 < x & not x < 0 implies sgn x = 0 ) );

registration
let x be real number ;
cluster sgn x -> real integer ;
coherence
sgn x is integer
proof end;
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:27
canceled;

theorem :: ABSVALUE:28
canceled;

theorem :: ABSVALUE:29
canceled;

theorem :: ABSVALUE:30
canceled;

theorem :: ABSVALUE:31
for x being real number st sgn x = 1 holds
0 < x
proof end;

theorem :: ABSVALUE:32
for x being real number st sgn x = - 1 holds
x < 0
proof end;

theorem Th33: :: ABSVALUE:33
for x being real number st sgn x = 0 holds
x = 0
proof end;

theorem :: ABSVALUE:34
for x being real number holds x = (abs x) * (sgn x)
proof end;

theorem Th35: :: ABSVALUE:35
for x, y being real number holds sgn (x * y) = (sgn x) * (sgn y)
proof end;

theorem :: ABSVALUE:36
for x being real number holds sgn (sgn x) = sgn x ;

theorem :: ABSVALUE:37
for x, y being real number holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1
proof end;

theorem Th38: :: ABSVALUE:38
for x being real number st x <> 0 holds
(sgn x) * (sgn (1 / x)) = 1
proof end;

theorem Th39: :: ABSVALUE:39
for x being real number holds 1 / (sgn x) = sgn (1 / x)
proof end;

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

theorem :: ABSVALUE:41
for x being real number holds sgn x = sgn (1 / x)
proof end;

theorem :: ABSVALUE:42
for x, y being real number holds sgn (x / y) = (sgn x) / (sgn y)
proof end;

theorem :: ABSVALUE:43
for r being real number holds 0 <= r + (abs r)
proof end;

theorem :: ABSVALUE:44
for r being real number holds 0 <= (- r) + (abs r)
proof end;

theorem :: ABSVALUE:45
for r, s being real number holds
( not abs r = abs s or r = s or r = - s )
proof end;

theorem :: ABSVALUE:46
for m being Nat holds m = abs m
proof end;