:: 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
b
1
being
set
holds
( (
0
<=
x
implies (
b
1
=
|.
x
.|
iff
b
1
=
x
) ) & ( not
0
<=
x
implies (
b
1
=
|.
x
.|
iff
b
1
=
-
x
) ) )
;
consistency
for
b
1
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
) & ( 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
&
x
<>
0
holds
x
<
0
by
Def1
;
theorem
:: ABSVALUE:4
for
x
being
real
number
holds
(
-
(
abs
x
)
<=
x
&
x
<=
abs
x
)
proof
end;
theorem
:: ABSVALUE:5
for
y
,
x
being
real
number
holds
( (
-
y
<=
x
&
x
<=
y
) iff
abs
x
<=
y
)
proof
end;
theorem
:: ABSVALUE:6
for
x
being
real
number
st
x
<>
0
holds
(
abs
x
)
*
(
abs
(
1
/
x
)
)
=
1
proof
end;
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
)
)
proof
end;
theorem
:: ABSVALUE:9
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:10
for
x
,
y
being
real
number
st
0
<
x
/
y
holds
sqrt
(
x
/
y
)
=
(
sqrt
(
abs
x
)
)
/
(
sqrt
(
abs
y
)
)
proof
end;
theorem
:: ABSVALUE:11
for
x
,
y
being
real
number
st
0
<=
x
*
y
holds
abs
(
x
+
y
)
=
(
abs
x
)
+
(
abs
y
)
proof
end;
theorem
:: ABSVALUE:12
for
x
,
y
being
real
number
st
abs
(
x
+
y
)
=
(
abs
x
)
+
(
abs
y
)
holds
0
<=
x
*
y
proof
end;
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
)
)
)
proof
end;
:: 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
) & (
x
<
0
implies
-
1 is
real
number
) & ( not
0
<
x
& not
x
<
0
implies
0
is
real
number
) )
;
consistency
for
b
1
being
real
number
st
0
<
x
&
x
<
0
holds
(
b
1
=
1 iff
b
1
=
-
1 )
;
projectivity
for
b
1
,
b
2
being
real
number
st (
0
<
b
2
implies
b
1
=
1 ) & (
b
2
<
0
implies
b
1
=
-
1 ) & ( not
0
<
b
2
& not
b
2
<
0
implies
b
1
=
0
) holds
( (
0
<
b
1
implies
b
1
=
1 ) & (
b
1
<
0
implies
b
1
=
-
1 ) & ( not
0
<
b
1
& not
b
1
<
0
implies
b
1
=
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:14
for
x
being
real
number
st
sgn
x
=
1 holds
0
<
x
proof
end;
theorem
:: ABSVALUE:15
for
x
being
real
number
st
sgn
x
=
-
1 holds
x
<
0
proof
end;
theorem
Th16
:
:: ABSVALUE:16
for
x
being
real
number
st
sgn
x
=
0
holds
x
=
0
proof
end;
theorem
:: ABSVALUE:17
for
x
being
real
number
holds
x
=
(
abs
x
)
*
(
sgn
x
)
proof
end;
theorem
Th18
:
:: ABSVALUE:18
for
x
,
y
being
real
number
holds
sgn
(
x
*
y
)
=
(
sgn
x
)
*
(
sgn
y
)
proof
end;
theorem
:: ABSVALUE:19
canceled;
theorem
:: ABSVALUE:20
for
x
,
y
being
real
number
holds
sgn
(
x
+
y
)
<=
(
(
sgn
x
)
+
(
sgn
y
)
)
+
1
proof
end;
theorem
Th21
:
:: ABSVALUE:21
for
x
being
real
number
st
x
<>
0
holds
(
sgn
x
)
*
(
sgn
(
1
/
x
)
)
=
1
proof
end;
theorem
Th22
:
:: ABSVALUE:22
for
x
being
real
number
holds 1
/
(
sgn
x
)
=
sgn
(
1
/
x
)
proof
end;
theorem
:: ABSVALUE:23
for
x
,
y
being
real
number
holds
(
(
sgn
x
)
+
(
sgn
y
)
)
-
1
<=
sgn
(
x
+
y
)
proof
end;
theorem
:: ABSVALUE:24
for
x
being
real
number
holds
sgn
x
=
sgn
(
1
/
x
)
proof
end;
theorem
:: ABSVALUE:25
for
x
,
y
being
real
number
holds
sgn
(
x
/
y
)
=
(
sgn
x
)
/
(
sgn
y
)
proof
end;
theorem
:: ABSVALUE:26
for
r
being
real
number
holds
0
<=
r
+
(
abs
r
)
proof
end;
theorem
:: ABSVALUE:27
for
r
being
real
number
holds
0
<=
(
-
r
)
+
(
abs
r
)
proof
end;
theorem
:: ABSVALUE:28
for
r
,
s
being
real
number
holds
( not
abs
r
=
abs
s
or
r
=
s
or
r
=
-
s
)
proof
end;
theorem
:: ABSVALUE:29
for
m
being
Nat
holds
m
=
abs
m
proof
end;
:: from JORDAN2C, 2011.07.03, A.T,
theorem
:: ABSVALUE:30
for
r
being
real
number
st
r
<=
0
holds
abs
r
=
-
r
proof
end;