:: ABSVALUE semantic presentation

definition

let x be real number ;
redefine func |.x.| equals :Def1: :: ABSVALUE:def 1
x if 0 <= x
otherwise - x;
correctness by COMPLEX1:129, COMPLEX1:156;

end;

:: deftheorem Def1 defines |. ABSVALUE:def 1 :

theorem :: ABSVALUE:1

for x being real number holds
( abs x = x or abs x = - x )

proof end;

Lm1: for x being real number holds 0 <= abs x
by COMPLEX1:132;

Lm2: for x being real number st x <> 0 holds
0 < abs x
by COMPLEX1:133;

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

proof end;

Lm3: for x, y being real number holds abs (x * y) = (abs x) * (abs y)
by COMPLEX1:151;

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;

Lm4: for x, y being real number holds abs (x + y) <= (abs x) + (abs y)
by COMPLEX1:142;

theorem :: ABSVALUE:13

canceled;

theorem Th14: :: 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)

proof end;

Lm5: for x, y being real number holds abs (x / y) = (abs x) / (abs y)
by COMPLEX1:153;

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 -> set equals :Def2: :: ABSVALUE:def 2
1 if 0 < x
- 1 if x < 0
otherwise 0;
coherence ;
consistency ;

end;