:: ABSVALUE semantic presentation

begin


definition
let x be real number ;
redefine func |.x.| equals :Def1: :: ABSVALUE:def 1
x if  0 <= x
otherwise  - x;
correctness
compatibility
for b1 being set holds
( ( 0 <= x implies ( b1 = |.x.| iff b1 = x ) ) & ( not 0 <= x implies ( b1 = |.x.| iff b1 = - x ) ) );
consistency
for b1 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
let x be real number ; ::_thesis: ( - (abs x) <= x & x <= abs x )
percases ( x < 0 or 0 <= x ) ;
supposeA1: x < 0 ; ::_thesis: ( - (abs x) <= x & x <= abs x )
then  abs x = - x by Def1;
hence  ( - (abs x) <= x & x <= abs x ) by A1; ::_thesis: verum
end;
supposeA2: 0 <= x ; ::_thesis: ( - (abs x) <= x & x <= abs x )
then  - x <= - 0 ;
hence  ( - (abs x) <= x & x <= abs x ) by A2, Def1; ::_thesis: verum
end;
end;
end;

theorem :: ABSVALUE:5
for y, x being real number holds
( ( - y <= x & x <= y ) iff abs x <= y )
proof
let y, x be real number ; ::_thesis: ( ( - y <= x & x <= y ) iff abs x <= y )
hereby  ::_thesis: ( abs x <= y implies ( - y <= x & x <= y ) )
assume that
A1: - y <= x and
A2: x <= y ; ::_thesis: abs x <= y
 - x <= - (- y) by A1, XREAL_1:24;
hence  abs x <= y by A2, Def1; ::_thesis: verum
end;
assume A3: abs x <= y ; ::_thesis: ( - y <= x & x <= y )
then A4: 0 <= y by COMPLEX1:46;
percases ( 0 < x or x < 0 or x = - 0 ) ;
suppose 0 < x ; ::_thesis: ( - y <= x & x <= y )
hence  ( - y <= x & x <= y ) by A3, A4, Def1; ::_thesis: verum
end;
supposeA5: x < 0 ; ::_thesis: ( - y <= x & x <= y )
then  - x <= y by A3, Def1;
then  - y <= - (- x) by XREAL_1:24;
hence  ( - y <= x & x <= y ) by A5; ::_thesis: verum
end;
suppose x = - 0 ; ::_thesis: ( - y <= x & x <= y )
hence  ( - y <= x & x <= y ) by A4; ::_thesis: verum
end;
end;
end;

theorem :: ABSVALUE:6
for x being real number st x <> 0 holds
(abs x) * (abs (1 / x)) = 1
proof
let x be real number ; ::_thesis: ( x <> 0 implies (abs x) * (abs (1 / x)) = 1 )
assume  x <> 0 ; ::_thesis: (abs x) * (abs (1 / x)) = 1
then  ( (abs x) * (abs (1 / x)) = abs (x * (1 / x)) & abs (x * (1 / x)) = abs 1 ) by COMPLEX1:65, XCMPLX_1:106;
hence  (abs x) * (abs (1 / x)) = 1 by Def1; ::_thesis: verum
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
let x, y be real number ; ::_thesis: ( 0 <= x * y implies sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) )
assume  0 <= x * y ; ::_thesis: sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y))
then  abs (x * y) = x * y by Def1;
then A1: (abs x) * (abs y) = x * y by COMPLEX1:65;
 ( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46;
hence  sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) by A1, SQUARE_1:29; ::_thesis: verum
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
let x, z, y, t be real number ; ::_thesis: ( abs x <= z & abs y <= t implies abs (x + y) <= z + t )
assume  ( abs x <= z & abs y <= t ) ; ::_thesis: abs (x + y) <= z + t
then  ( abs (x + y) <= (abs x) + (abs y) & (abs x) + (abs y) <= z + t ) by COMPLEX1:56, XREAL_1:7;
hence  abs (x + y) <= z + t by XXREAL_0:2; ::_thesis: verum
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
let x, y be real number ; ::_thesis: ( 0 < x / y implies sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) )
assume  0 < x / y ; ::_thesis: sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y))
then  x / y = abs (x / y) by Def1;
then A1: x / y = (abs x) / (abs y) by COMPLEX1:67;
 ( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46;
hence  sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) by A1, SQUARE_1:30; ::_thesis: verum
end;

theorem :: ABSVALUE:11
for x, y being real number st 0 <= x * y holds
abs (x + y) = (abs x) + (abs y)
proof
let x, y be real number ; ::_thesis: ( 0 <= x * y implies abs (x + y) = (abs x) + (abs y) )
assume A1: 0 <= x * y ; ::_thesis: abs (x + y) = (abs x) + (abs y)
percases ( x * y = 0 or 0 < x * y ) by A1;
supposeA2: x * y = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y)
percases ( x = 0 or y = 0 ) by A2, XCMPLX_1:6;
supposeA3: x = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y)
then (abs x) + (abs y) = 0 + (abs y) by Def1
.= abs y ;
hence  abs (x + y) = (abs x) + (abs y) by A3; ::_thesis: verum
end;
supposeA4: y = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y)
then (abs x) + (abs y) = (abs x) + 0 by Def1
.= abs x ;
hence  abs (x + y) = (abs x) + (abs y) by A4; ::_thesis: verum
end;
end;
end;
supposeA5: 0 < x * y ; ::_thesis: abs (x + y) = (abs x) + (abs y)
then A6: ( x <> 0 & y <> 0 ) ;
percases ( ( 0 < x & 0 < y ) or ( x < 0 & y < 0 ) ) by A5, A6;
supposeA7: ( 0 < x & 0 < y ) ; ::_thesis: abs (x + y) = (abs x) + (abs y)
 ( abs x = x & abs y = y ) by A7, Def1;
hence  abs (x + y) = (abs x) + (abs y) by A7, Def1; ::_thesis: verum
end;
supposethat A8: x < 0 and
A9: y < 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y)
 abs x = - x by A8, Def1;
then (abs x) + (abs y) = ((- 1) * x) + (- (1 * y)) by A9, Def1
.= - (x + y) ;
hence  abs (x + y) = (abs x) + (abs y) by A8, A9, Def1; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: ABSVALUE:12
for x, y being real number st abs (x + y) = (abs x) + (abs y) holds
0 <= x * y
proof
let x, y be real number ; ::_thesis: ( abs (x + y) = (abs x) + (abs y) implies 0 <= x * y )
A1: ( not x * y < 0 or ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )
proof
assume A2: x * y < 0 ; ::_thesis: ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )
then  ( x <> 0 & y <> 0 ) ;
hence  ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) by A2; ::_thesis: verum
end;
A3: ( x < 0 & 0 < y & x + y < 0 implies abs (x + y) <> (abs x) + (abs y) )
proof
assume that
A4: x < 0 and
A5: 0 < y and
A6: x + y < 0 ; ::_thesis: abs (x + y) <> (abs x) + (abs y)
 (- (1 * x)) + (- y) < (- x) + y by A5, XREAL_1:6;
then A7: - (1 * (x + y)) < (- x) + y ;
 ( abs x = - x & abs y = y ) by A4, A5, Def1;
hence  abs (x + y) <> (abs x) + (abs y) by A6, A7, Def1; ::_thesis: verum
end;
A8: ( 0 < x & y < 0 & x + y < 0 implies abs (x + y) <> (abs x) + (abs y) )
proof
assume that
A9: 0 < x and
A10: y < 0 and
A11: x + y < 0 ; ::_thesis: abs (x + y) <> (abs x) + (abs y)
 (- (1 * x)) + (- y) < x + (- y) by A9, XREAL_1:6;
then A12: - (1 * (x + y)) < x + (- y) ;
 ( abs x = x & abs y = - y ) by A9, A10, Def1;
hence  abs (x + y) <> (abs x) + (abs y) by A11, A12, Def1; ::_thesis: verum
end;
A13: ( 0 < x & y < 0 & 0 <= x + y implies abs (x + y) <> (abs x) + (abs y) )
proof
assume that
A14: 0 < x and
A15: y < 0 and
A16: 0 <= x + y ; ::_thesis: abs (x + y) <> (abs x) + (abs y)
A17: abs y = - y by A15, Def1;
 ( x + y < x + (- y) & abs x = x ) by A14, A15, Def1, XREAL_1:6;
hence  abs (x + y) <> (abs x) + (abs y) by A16, A17, Def1; ::_thesis: verum
end;
A18: ( x < 0 & 0 < y & 0 <= x + y implies abs (x + y) <> (abs x) + (abs y) )
proof
assume that
A19: x < 0 and
A20: 0 < y and
A21: 0 <= x + y ; ::_thesis: abs (x + y) <> (abs x) + (abs y)
A22: abs y = y by A20, Def1;
 ( x + y < (- x) + y & abs x = - x ) by A19, Def1, XREAL_1:6;
hence  abs (x + y) <> (abs x) + (abs y) by A21, A22, Def1; ::_thesis: verum
end;
assume  ( abs (x + y) = (abs x) + (abs y) & 0 > x * y ) ; ::_thesis: contradiction
hence  contradiction by A1, A3, A18, A8, A13; ::_thesis: verum
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
let x, y be real number ; ::_thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
A1: for s, t being real number st s <= t & 0 < 1 + s & 0 < 1 + t holds
s / (1 + s) <= t / (1 + t)
proof
let s, t be real number ; ::_thesis: ( s <= t & 0 < 1 + s & 0 < 1 + t implies s / (1 + s) <= t / (1 + t) )
assume that
A2: s <= t and
A3: 0 < 1 + s and
A4: 0 < 1 + t ; ::_thesis: s / (1 + s) <= t / (1 + t)
 (s * 1) + (s * t) <= t + (s * t) by A2, XREAL_1:6;
then  (s * (1 + t)) * ((1 + s) ") <= (t * (1 + s)) * ((1 + s) ") by A3, XREAL_1:64;
then  (s * (1 + t)) * ((1 + s) ") <= t * ((1 + s) * ((1 + s) ")) ;
then  (s * (1 + t)) * ((1 + s) ") <= t * 1 by A3, XCMPLX_0:def_7;
then  ((s * ((1 + s) ")) * (1 + t)) * ((1 + t) ") <= t * ((1 + t) ") by A4, XREAL_1:64;
then  (s * ((1 + s) ")) * ((1 + t) * ((1 + t) ")) <= t * ((1 + t) ") ;
then  (s * ((1 + s) ")) * 1 <= t * ((1 + t) ") by A4, XCMPLX_0:def_7;
then  s / (1 + s) <= t * ((1 + t) ") by XCMPLX_0:def_9;
hence  s / (1 + s) <= t / (1 + t) by XCMPLX_0:def_9; ::_thesis: verum
end;
set a = abs x;
set b = abs y;
set c = abs (x + y);
A5: 0 <= abs x by COMPLEX1:46;
A6: 0 <= abs y by COMPLEX1:46;
A7: 0 + 0 < 1 + (abs x) by COMPLEX1:46, XREAL_1:8;
A8: ( 0 < 1 + (abs x) & 0 < (1 + (abs x)) + (abs y) implies (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) )
proof
assume that
A9: 0 < 1 + (abs x) and
A10: 0 < (1 + (abs x)) + (abs y) ; ::_thesis: (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x))
 0 + (abs x) <= ((abs x) * (abs y)) + (abs x) by A5, A6, XREAL_1:6;
then  ((abs x) * 1) + ((abs x) * (abs x)) <= ((abs x) * (1 + (abs y))) + ((abs x) * (abs x)) by XREAL_1:6;
then  ((abs x) * (1 + (abs x))) * ((1 + (abs x)) ") <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") by A9, XREAL_1:64;
then  (abs x) * ((1 + (abs x)) * ((1 + (abs x)) ")) <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") ;
then  (abs x) * 1 <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") by A7, XCMPLX_0:def_7;
then  (abs x) * (((1 + (abs x)) + (abs y)) ") <= (((abs x) * ((1 + (abs x)) ")) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) ") by A10, XREAL_1:64;
then  (abs x) * (((1 + (abs x)) + (abs y)) ") <= ((abs x) * ((1 + (abs x)) ")) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) ")) ;
then  (abs x) * (((1 + (abs x)) + (abs y)) ") <= ((abs x) * ((1 + (abs x)) ")) * 1 by A5, A6, XCMPLX_0:def_7;
then  (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) * ((1 + (abs x)) ") by XCMPLX_0:def_9;
hence  (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) by XCMPLX_0:def_9; ::_thesis: verum
end;
A11: 0 + 0 < 1 + (abs y) by COMPLEX1:46, XREAL_1:8;
A12: ( 0 < 1 + (abs y) & 0 < (1 + (abs x)) + (abs y) implies (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) )
proof
assume that
A13: 0 < 1 + (abs y) and
A14: 0 < (1 + (abs x)) + (abs y) ; ::_thesis: (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y))
 0 + (abs y) <= ((abs x) * (abs y)) + (abs y) by A5, A6, XREAL_1:6;
then  ((abs y) * 1) + ((abs y) * (abs y)) <= ((1 + (abs x)) * (abs y)) + ((abs y) * (abs y)) by XREAL_1:6;
then  ((abs y) * (1 + (abs y))) * ((1 + (abs y)) ") <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") by A13, XREAL_1:64;
then  (abs y) * ((1 + (abs y)) * ((1 + (abs y)) ")) <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") ;
then  (abs y) * 1 <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") by A11, XCMPLX_0:def_7;
then  (abs y) * (((1 + (abs x)) + (abs y)) ") <= (((abs y) * ((1 + (abs y)) ")) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) ") by A14, XREAL_1:64;
then  (abs y) * (((1 + (abs x)) + (abs y)) ") <= ((abs y) * ((1 + (abs y)) ")) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) ")) ;
then  (abs y) * (((1 + (abs x)) + (abs y)) ") <= ((abs y) * ((1 + (abs y)) ")) * 1 by A5, A6, XCMPLX_0:def_7;
then  (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) * ((1 + (abs y)) ") by XCMPLX_0:def_9;
hence  (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) by XCMPLX_0:def_9; ::_thesis: verum
end;
 0 + 0 < 1 + (abs (x + y)) by COMPLEX1:46, XREAL_1:8;
then A15: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) + (abs y)) / (1 + ((abs x) + (abs y))) by A5, A6, A1, COMPLEX1:56;
 ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) = ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) by XCMPLX_1:62;
then  ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A6, A7, A8, A12, XREAL_1:7;
hence  (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A15, XXREAL_0:2; ::_thesis: verum
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 b1 being real number st 0 < x & x < 0 holds
( b1 = 1 iff b1 = - 1 ) ;
projectivity
 for b1, b2 being real number 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 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
 ( x = 0 or x > 0 or x < 0 ) ;
hence  sgn x is integer by Def2; ::_thesis: verum
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
let x be real number ; ::_thesis: ( sgn x = 1 implies 0 < x )
assume that
A1: sgn x = 1 and
A2: 0 >= x ; ::_thesis: contradiction
 ( x < 0 or x = 0 ) by A2;
hence  contradiction by A1, Def2; ::_thesis: verum
end;

theorem :: ABSVALUE:15
for x being real number st sgn x = - 1 holds
x < 0
proof
let x be real number ; ::_thesis: ( sgn x = - 1 implies x < 0 )
assume that
A1: sgn x = - 1 and
A2: x >= 0 ; ::_thesis: contradiction
 ( 0 < x or x = 0 ) by A2;
hence  contradiction by A1, Def2; ::_thesis: verum
end;

theorem Th16: :: ABSVALUE:16
for x being real number st sgn x = 0 holds
x = 0
proof
let x be real number ; ::_thesis: ( sgn x = 0 implies x = 0 )
assume that
A1: sgn x = 0 and
A2: x <> 0 ; ::_thesis: contradiction
 ( 0 < x or x < 0 ) by A2;
hence  contradiction by A1, Def2; ::_thesis: verum
end;

theorem :: ABSVALUE:17
for x being real number holds x = (abs x) * (sgn x)
proof
let x be real number ; ::_thesis: x = (abs x) * (sgn x)
A1: ( 0 < x implies x = (abs x) * (sgn x) )
proof
assume A2: 0 < x ; ::_thesis: x = (abs x) * (sgn x)
then  abs x = x by Def1;
then  (abs x) * (sgn x) = x * 1 by A2, Def2;
hence  x = (abs x) * (sgn x) ; ::_thesis: verum
end;
A3: ( x < 0 implies x = (abs x) * (sgn x) )
proof
assume A4: x < 0 ; ::_thesis: x = (abs x) * (sgn x)
then  abs x = - x by Def1;
then (abs x) * (sgn x) = (- x) * (- 1) by A4, Def2
.= x ;
hence  x = (abs x) * (sgn x) ; ::_thesis: verum
end;
 ( x = 0 implies x = (abs x) * (sgn x) )
proof
assume A5: x = 0 ; ::_thesis: x = (abs x) * (sgn x)
then  sgn x = 0 by Def2;
hence  x = (abs x) * (sgn x) by A5; ::_thesis: verum
end;
hence  x = (abs x) * (sgn x) by A1, A3; ::_thesis: verum
end;

theorem Th18: :: ABSVALUE:18
for x, y being real number holds sgn (x * y) = (sgn x) * (sgn y)
proof
let x, y be real number ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
A1: ( 0 < x & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A2: 0 < x and
A3: 0 < y ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
A4: sgn y = 1 by A3, Def2;
 ( 0 * y < x * y & sgn x = 1 ) by A2, A3, Def2, XREAL_1:68;
hence  sgn (x * y) = (sgn x) * (sgn y) by A4, Def2; ::_thesis: verum
end;
A5: ( 0 < x & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A6: 0 < x and
A7: y < 0 ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
 sgn y = - 1 by A7, Def2;
then A8: (sgn x) * (sgn y) = 1 * (- 1) by A6, Def2
.= - 1 ;
 x * y < 0 * y by A6, A7, XREAL_1:69;
hence  sgn (x * y) = (sgn x) * (sgn y) by A8, Def2; ::_thesis: verum
end;
A9: ( x < 0 & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A10: x < 0 and
A11: y < 0 ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
 sgn y = - 1 by A11, Def2;
then A12: (sgn x) * (sgn y) = (- 1) * (- 1) by A10, Def2
.= 1 ;
 x * 0 < x * y by A10, A11, XREAL_1:69;
hence  sgn (x * y) = (sgn x) * (sgn y) by A12, Def2; ::_thesis: verum
end;
A13: ( x < 0 & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A14: x < 0 and
A15: 0 < y ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
 sgn y = 1 by A15, Def2;
then A16: (sgn x) * (sgn y) = - 1 by A14, Def2;
 x * y < 0 * y by A14, A15, XREAL_1:68;
hence  sgn (x * y) = (sgn x) * (sgn y) by A16, Def2; ::_thesis: verum
end;
 ( ( x = 0 or y = 0 ) implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume A17: ( x = 0 or y = 0 ) ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y)
then  ( sgn x = 0 or sgn y = 0 ) by Def2;
hence  sgn (x * y) = (sgn x) * (sgn y) by A17; ::_thesis: verum
end;
hence  sgn (x * y) = (sgn x) * (sgn y) by A1, A5, A13, A9; ::_thesis: verum
end;

theorem :: ABSVALUE:19
canceled;

theorem :: ABSVALUE:20
for x, y being real number holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1
proof
let x, y be real number ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
A1: ( y = 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
assume A2: y = 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then ((sgn x) + (sgn y)) + 1 = ((sgn x) + 0) + 1 by Def2
.= (sgn x) + 1 ;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A2, XREAL_1:29; ::_thesis: verum
end;
A3: ( 0 < x & 0 < y implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
 sgn x < (sgn x) + 1 by XREAL_1:29;
then A4: (sgn x) + 0 < ((sgn x) + 1) + 1 by XREAL_1:8;
assume A5: ( 0 < x & 0 < y ) ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then  ( sgn x = 1 & sgn y = 1 ) by Def2;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A5, A4, Def2; ::_thesis: verum
end;
A6: ( x < 0 & 0 < y implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
assume that
A7: x < 0 and
A8: 0 < y ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
 sgn x = - 1 by A7, Def2;
then A9: ((sgn x) + (sgn y)) + 1 = 1 by A8, Def2;
 ( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A9, Def2; ::_thesis: verum
end;
A10: ( 0 < x & y < 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
assume that
A11: 0 < x and
A12: y < 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
 sgn x = 1 by A11, Def2;
then A13: ((sgn x) + (sgn y)) + 1 = (1 + (- 1)) + 1 by A12, Def2
.= 1 ;
 ( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A13, Def2; ::_thesis: verum
end;
A14: ( x < 0 & y < 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
assume that
A15: x < 0 and
A16: y < 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
 sgn y = - 1 by A16, Def2;
then  ((sgn x) + (sgn y)) + 1 = - 1 by A15, Def2;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A15, A16, Def2; ::_thesis: verum
end;
 ( x = 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )
proof
assume A17: x = 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then ((sgn x) + (sgn y)) + 1 = (0 + (sgn y)) + 1 by Def2
.= (sgn y) + 1 ;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A17, XREAL_1:29; ::_thesis: verum
end;
hence  sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A3, A10, A6, A14, A1; ::_thesis: verum
end;

theorem Th21: :: ABSVALUE:21
for x being real number st x <> 0 holds
(sgn x) * (sgn (1 / x)) = 1
proof
let x be real number ; ::_thesis: ( x <> 0 implies (sgn x) * (sgn (1 / x)) = 1 )
assume  x <> 0 ; ::_thesis: (sgn x) * (sgn (1 / x)) = 1
then  sgn (x * (1 / x)) = sgn 1 by XCMPLX_1:106;
then  sgn (x * (1 / x)) = 1 by Def2;
hence  (sgn x) * (sgn (1 / x)) = 1 by Th18; ::_thesis: verum
end;

theorem Th22: :: ABSVALUE:22
for x being real number holds 1 / (sgn x) = sgn (1 / x)
proof
let x be real number ; ::_thesis: 1 / (sgn x) = sgn (1 / x)
percases ( x = 0 or x <> 0 ) ;
supposeA1: x = 0 ; ::_thesis: 1 / (sgn x) = sgn (1 / x)
hence 1 / (sgn x) = 1 / 0 by Def2
.= sgn (1 / x) by A1, Def2 ;
::_thesis: verum
end;
supposeA2: x <> 0 ; ::_thesis: 1 / (sgn x) = sgn (1 / x)
then  ((sgn x) * (sgn (1 / x))) * (1 / (sgn x)) = 1 * (1 / (sgn x)) by Th21;
then  (sgn (1 / x)) * ((sgn x) * (1 / (sgn x))) = 1 / (sgn x) ;
then  (sgn (1 / x)) * 1 = 1 / (sgn x) by A2, Th16, XCMPLX_1:106;
hence  1 / (sgn x) = sgn (1 / x) ; ::_thesis: verum
end;
end;
end;

theorem :: ABSVALUE:23
for x, y being real number holds ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
proof
let x, y be real number ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A1: ( ( x = 0 or y = 0 ) implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
A2: ( y = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
A3: (sgn x) - 1 < ((sgn x) + (- 1)) + 1 by XREAL_1:29;
assume A4: y = 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then ((sgn x) + (sgn y)) - 1 = ((sgn x) + 0) - 1 by Def2
.= (sgn x) - 1 ;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A4, A3; ::_thesis: verum
end;
A5: ( x = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
A6: (sgn y) - 1 < ((sgn y) + (- 1)) + 1 by XREAL_1:29;
assume A7: x = 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then ((sgn x) + (sgn y)) - 1 = (0 + (sgn y)) - 1 by Def2
.= (sgn y) - 1 ;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A7, A6; ::_thesis: verum
end;
assume  ( x = 0 or y = 0 ) ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A5, A2; ::_thesis: verum
end;
A8: ( x < 0 & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
assume that
A9: x < 0 and
A10: y < 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
 sgn x = - 1 by A9, Def2;
then A11: sgn x = sgn (x + y) by A9, A10, Def2;
A12: ( ((sgn (x + y)) + (- 1)) - 1 < (((sgn (x + y)) + (- 1)) - 1) + 1 & (sgn (x + y)) + (- 1) < ((sgn (x + y)) + (- 1)) + 1 ) by XREAL_1:29;
 sgn y = - 1 by A10, Def2;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A11, A12, XXREAL_0:2; ::_thesis: verum
end;
A13: ( 0 < x & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
assume that
A14: 0 < x and
A15: y < 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
 sgn x = 1 by A14, Def2;
then A16: (sgn x) + (sgn y) = 1 + (- 1) by A15, Def2
.= 0 ;
 ( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A16, Def2; ::_thesis: verum
end;
A17: ( x < 0 & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
assume that
A18: x < 0 and
A19: 0 < y ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
 sgn x = - 1 by A18, Def2;
then A20: (sgn x) + (sgn y) = (- 1) + 1 by A19, Def2
.= 0 ;
 ( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A20, Def2; ::_thesis: verum
end;
 ( 0 < x & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )
proof
assume that
A21: 0 < x and
A22: 0 < y ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
 sgn y = 1 by A22, Def2;
then  ((sgn x) + (sgn y)) - 1 = 1 by A21, Def2;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A21, A22, Def2; ::_thesis: verum
end;
hence  ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A8, A17, A13, A1; ::_thesis: verum
end;

theorem :: ABSVALUE:24
for x being real number holds sgn x = sgn (1 / x)
proof
let x be real number ; ::_thesis: sgn x = sgn (1 / x)
A1: ( 0 < x implies sgn x = sgn (1 / x) )
proof
assume A2: 0 < x ; ::_thesis: sgn x = sgn (1 / x)
 sgn (1 / x) = 1 / (sgn x) by Th22;
then  sgn (1 / x) = 1 / 1 by A2, Def2
.= 1 ;
hence  sgn x = sgn (1 / x) by A2, Def2; ::_thesis: verum
end;
 ( x < 0 implies sgn x = sgn (1 / x) )
proof
assume A3: x < 0 ; ::_thesis: sgn x = sgn (1 / x)
then  sgn x = - 1 by Def2;
then  sgn (1 / x) = 1 / (- 1) by Th22;
hence  sgn x = sgn (1 / x) by A3, Def2; ::_thesis: verum
end;
hence  sgn x = sgn (1 / x) by A1; ::_thesis: verum
end;

theorem :: ABSVALUE:25
for x, y being real number holds sgn (x / y) = (sgn x) / (sgn y)
proof
let x, y be real number ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y)
percases ( y = 0 or y <> 0 ) ;
supposeA1: y = 0 ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y)
hence  sgn (x / y) = sgn (x * (0 ")) by XCMPLX_0:def_9
.= (sgn x) * (0 ") by Def2
.= (sgn x) / 0 by XCMPLX_0:def_9
.= (sgn x) / (sgn y) by A1, Def2 ;
::_thesis: verum
end;
supposeA2: y <> 0 ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y)
x / y = (x / y) * 1
.= (x / y) * (y * (1 / y)) by A2, XCMPLX_1:106
.= ((x / y) * y) * (1 / y)
.= x * (1 / y) by A2, XCMPLX_1:87 ;
then  sgn (x / y) = (sgn x) * (sgn (1 / y)) by Th18
.= ((sgn x) / 1) * (1 / (sgn y)) by Th22
.= ((sgn x) * 1) / (1 * (sgn y)) by XCMPLX_1:76
.= (sgn x) / (1 * (sgn y)) ;
hence  sgn (x / y) = (sgn x) / (sgn y) ; ::_thesis: verum
end;
end;
end;


theorem :: ABSVALUE:26
for r being real number holds 0 <= r + (abs r)
proof
let r be real number ; ::_thesis: 0 <= r + (abs r)
A1: 0 <= abs r by COMPLEX1:46;
 ( (abs r) + (abs r) = r + (abs r) or (abs r) + r = (- r) + r ) by Def1;
hence  0 <= r + (abs r) by A1; ::_thesis: verum
end;

theorem :: ABSVALUE:27
for r being real number holds 0 <= (- r) + (abs r)
proof
let r be real number ; ::_thesis: 0 <= (- r) + (abs r)
 r <= abs r by COMPLEX1:76;
then  - r >= - (abs r) by XREAL_1:24;
then  (- r) + (abs r) >= (- (abs r)) + (abs r) by XREAL_1:7;
hence  0 <= (- r) + (abs r) ; ::_thesis: verum
end;

theorem :: ABSVALUE:28
for r, s being real number holds
( not abs r = abs s or r = s or r = - s )
proof
let r, s be real number ; ::_thesis: ( not abs r = abs s or r = s or r = - s )
assume A1: abs r = abs s ; ::_thesis: ( r = s or r = - s )
assume A2: r <> s ; ::_thesis: r = - s
percases ( ( abs r = r & abs s = s ) or ( abs r = r & abs s = - s ) or ( abs r = - r & abs s = s ) or ( abs r = - r & abs s = - s ) ) by Def1;
suppose ( abs r = r & abs s = s ) ; ::_thesis: r = - s
hence  r = - s by A1, A2; ::_thesis: verum
end;
suppose ( abs r = r & abs s = - s ) ; ::_thesis: r = - s
hence  r = - s by A1; ::_thesis: verum
end;
suppose ( abs r = - r & abs s = s ) ; ::_thesis: r = - s
hence  r = - s by A1; ::_thesis: verum
end;
suppose ( abs r = - r & abs s = - s ) ; ::_thesis: r = - s
hence  r = - s by A1, A2; ::_thesis: verum
end;
end;
end;

theorem :: ABSVALUE:29
for m being Nat holds m = abs m
proof
let m be Nat; ::_thesis: m = abs m
 m >= 0 by NAT_1:2;
hence  abs m = m by Def1; ::_thesis: verum
end;

theorem :: ABSVALUE:30
for r being real number st r <= 0 holds
abs r = - r
proof
let r be real number ; ::_thesis: ( r <= 0 implies abs r = - r )
assume A1: r <= 0 ; ::_thesis: abs r = - r
percases ( r < 0 or r = 0 ) by A1;
suppose r < 0 ; ::_thesis: abs r = - r
hence  abs r = - r by Def1; ::_thesis: verum
end;
suppose r = 0 ; ::_thesis: abs r = - r
hence  abs r = - r by Th2; ::_thesis: verum
end;
end;
end;