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