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


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

:: deftheorem Def1 defines |. ABSVALUE:def 1 :
for x being Real holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

registration
let x be non negative Real;
reduce |.x.| to x;
reducibility
|.x.| = x
by Def1;
end;

theorem :: ABSVALUE:1
for x being Real holds
( |.x.| = x or |.x.| = - x ) by Def1;

theorem :: ABSVALUE:2
for x being Real holds
( x = 0 iff |.x.| = 0 ) by COMPLEX1:47;

theorem :: ABSVALUE:3
for x being Real st |.x.| = - x & x <> 0 holds
x < 0 by Def1;

theorem :: ABSVALUE:4
for x being Real holds
( - |.x.| <= x & x <= |.x.| )
proof end;

theorem :: ABSVALUE:5
for x, y being Real holds
( ( - y <= x & x <= y ) iff |.x.| <= y )
proof end;

theorem :: ABSVALUE:6
for x being Real st x <> 0 holds
|.x.| * |.(1 / x).| = 1
proof end;

theorem :: ABSVALUE:7
for x being Real holds |.(1 / x).| = 1 / |.x.| by COMPLEX1:80;

theorem :: ABSVALUE:8
for x, y being Real st 0 <= x * y holds
sqrt (x * y) = (sqrt |.x.|) * (sqrt |.y.|)
proof end;

theorem :: ABSVALUE:9
for x, y, z, t being Real st |.x.| <= z & |.y.| <= t holds
|.(x + y).| <= z + t
proof end;

theorem :: ABSVALUE:10
for x, y being Real st 0 < x / y holds
sqrt (x / y) = (sqrt |.x.|) / (sqrt |.y.|)
proof end;

theorem :: ABSVALUE:11
for x, y being Real st 0 <= x * y holds
|.(x + y).| = |.x.| + |.y.|
proof end;

theorem :: ABSVALUE:12
for x, y being Real st |.(x + y).| = |.x.| + |.y.| holds
0 <= x * y
proof end;

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;
func sgn x -> Real equals :Def2: :: ABSVALUE:def 2
1 if 0 < x
- 1 if x < 0
otherwise 0 ;
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 b1 being Real st 0 < x & x < 0 holds
( b1 = 1 iff b1 = - 1 )
;
projectivity
for b1, b2 being Real 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 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;
cluster sgn x -> integer ;
coherence
sgn x is integer
proof end;
end;

theorem :: ABSVALUE:14
for x being Real st sgn x = 1 holds
0 < x
proof end;

theorem :: ABSVALUE:15
for x being Real st sgn x = - 1 holds
x < 0
proof end;

theorem Th16: :: ABSVALUE:16
for x being Real st sgn x = 0 holds
x = 0
proof end;

theorem :: ABSVALUE:17
for x being Real holds x = |.x.| * (sgn x)
proof end;

theorem Th18: :: ABSVALUE:18
for x, y being Real holds sgn (x * y) = (sgn x) * (sgn y)
proof end;

theorem :: ABSVALUE:19
canceled;

::$CT
theorem :: ABSVALUE:20
for x, y being Real holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1
proof end;

theorem Th20: :: ABSVALUE:21
for x being Real st x <> 0 holds
(sgn x) * (sgn (1 / x)) = 1
proof end;

theorem Th21: :: ABSVALUE:22
for x being Real holds 1 / (sgn x) = sgn (1 / x)
proof end;

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

theorem :: ABSVALUE:24
for x being Real holds sgn x = sgn (1 / x)
proof end;

theorem :: ABSVALUE:25
for x, y being Real holds sgn (x / y) = (sgn x) / (sgn y)
proof end;

:: from SCMPDS_9. 2008.05.06, A.T.
theorem :: ABSVALUE:26
for r being Real holds 0 <= r + |.r.|
proof end;

theorem :: ABSVALUE:27
for r being Real holds 0 <= (- r) + |.r.|
proof end;

theorem :: ABSVALUE:28
for r, s being Real holds
( not |.r.| = |.s.| or r = s or r = - s )
proof end;

theorem :: ABSVALUE:29
for m being Nat holds m = |.m.| ;

:: from JORDAN2C, 2011.07.03, A.T,
theorem :: ABSVALUE:30
for r being Real st r <= 0 holds
|.r.| = - r
proof end;