:: 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 b₁ being object holds
( ( 0 <= x implies ( b₁ = |.x.| iff b₁ = x ) ) & ( not 0 <= x implies ( b₁ = |.x.| iff b₁ = - x ) ) );
consistency
for b₁ 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 b₁ being Real st 0 < x & x < 0 holds
( b₁ = 1 iff b₁ = - 1 ) ;
projectivity
for b₁, b₂ being Real st ( 0 < b₂ implies b₁ = 1 ) & ( b₂ < 0 implies b₁ = - 1 ) & ( not 0 < b₂ & not b₂ < 0 implies b₁ = 0 ) holds
( ( 0 < b₁ implies b₁ = 1 ) & ( b₁ < 0 implies b₁ = - 1 ) & ( not 0 < b₁ & not b₁ < 0 implies b₁ = 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;