:: ABSVALUE semantic presentation

definition
let c1 be real number ;
redefine func |.c1.| -> set equals :E1: :: ABSVALUE:def 1
a1 if 0 <= a1
otherwise - a1;
correctness
compatibility
for b1 being set holds
( ( 0 <= c1 implies ( b1 = |.c1.| iff b1 = c1 ) ) & ( not 0 <= c1 implies ( b1 = |.c1.| iff b1 = - c1 ) ) );
consistency
for b1 being set holds
verum;
by COMPLEX1:129, COMPLEX1:156;
end;

:: deftheorem E1 defines |. ABSVALUE:def 1 :
for b1 being real number holds
( ( 0 <= b1 implies |.b1.| = b1 ) & ( not 0 <= b1 implies |.b1.| = - b1 ) );

theorem :: ABSVALUE:1
for b1 being real number holds
( abs b1 = b1 or abs b1 = - b1 )
proof
let c1 be real number ;
per cases not ( not c1 >= 0 & not c1 < 0 ) ;
suppose c1 >= 0 ;
hence ( abs c1 = c1 or abs c1 = - c1 ) by E1;
end;
suppose c1 < 0 ;
hence ( abs c1 = c1 or abs c1 = - c1 ) by E1;
end;
end;
end;

E2: for b1 being real number holds 0 <= abs b1
by COMPLEX1:132;

E3: for b1 being real number holds
not ( b1 <> 0 & not 0 < abs b1 )
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 b1 being real number holds
( b1 = 0 iff abs b1 = 0 ) by E1, COMPLEX1:133;

theorem :: ABSVALUE:8
canceled;

theorem :: ABSVALUE:9
for b1 being real number holds
not ( abs b1 = - b1 & b1 <> 0 & not b1 < 0 )
proof
let c1 be real number ;
assume that
E4: abs c1 = - c1 and
E5: c1 <> 0 and
E6: c1 >= 0 ;
0 < c1 by E5, E6, REAL_1:def 5;
then - c1 < - 0 by XREAL_1:26;
hence not verum by E4, E6, E1;
end;

E4: for b1, b2 being real number holds abs (b1 * b2) = (abs b1) * (abs b2)
by COMPLEX1:151;

theorem :: ABSVALUE:10
canceled;

theorem :: ABSVALUE:11
for b1 being real number holds
( - (abs b1) <= b1 & b1 <= abs b1 )
proof
let c1 be real number ;
per cases not ( not c1 < 0 & not 0 <= c1 ) ;
suppose E5: c1 < 0 ;
then E6: abs c1 = - c1 by E1;
0 < - c1 by E5, XREAL_1:60;
hence ( - (abs c1) <= c1 & c1 <= abs c1 ) by E5, E6, XXREAL_0:2;
end;
suppose E5: 0 <= c1 ;
then E6: abs c1 = c1 by E1;
- c1 <= - 0 by E5, XREAL_1:26;
hence ( - (abs c1) <= c1 & c1 <= abs c1 ) by E5, E6, XXREAL_0:2;
end;
end;
end;

theorem :: ABSVALUE:12
for b1, b2 being real number holds
( ( - b1 <= b2 & b2 <= b1 ) iff abs b2 <= b1 )
proof
let c1, c2 be real number ;
hereby
assume that
E5: - c1 <= c2 and
E6: c2 <= c1 ;
- c2 <= - (- c1) by E5, XREAL_1:26;
then ( c2 < 0 implies abs c2 <= c1 ) by E1;
hence abs c2 <= c1 by E6, E1;
end;
assume E5: abs c2 <= c1 ;
0 <= abs c2 by E2;
then E6: 0 <= c1 by E5, XXREAL_0:2;
per cases not ( not 0 < c2 & not c2 < 0 & not c2 = - 0 ) by XXREAL_0:1;
suppose E7: 0 < c2 ;
- c1 <= - 0 by E6, XREAL_1:26;
hence ( - c1 <= c2 & c2 <= c1 ) by E5, E7, E1, XXREAL_0:2;
end;
suppose E7: c2 < 0 ;
then - c2 <= c1 by E5, E1;
then - c1 <= - (- c2) by XREAL_1:26;
hence ( - c1 <= c2 & c2 <= c1 ) by E6, E7, XXREAL_0:2;
end;
suppose c2 = - 0 ;
hence ( - c1 <= c2 & c2 <= c1 ) by E6, XREAL_1:26;
end;
end;
end;

E5: for b1, b2 being real number holds abs (b1 + b2) <= (abs b1) + (abs b2)
by COMPLEX1:142;

theorem :: ABSVALUE:13
canceled;

theorem E6: :: ABSVALUE:14
for b1 being real number holds
( b1 <> 0 implies (abs b1) * (abs (1 / b1)) = 1 )
proof
let c1 be real number ;
assume E7: c1 <> 0 ;
E8: (abs c1) * (abs (1 / c1)) = abs (c1 * (1 / c1)) by E4;
abs (c1 * (1 / c1)) = abs 1 by E7, XCMPLX_1:107;
hence (abs c1) * (abs (1 / c1)) = 1 by E8, E1;
end;

theorem :: ABSVALUE:15
for b1 being real number holds abs (1 / b1) = 1 / (abs b1)
proof
let c1 be real number ;
per cases not ( not c1 = 0 & not c1 <> 0 ) ;
suppose E7: c1 = 0 ;
hence abs (1 / c1) = abs (1 * (0 " )) by XCMPLX_0:def 9
.= abs (1 * 0) by XCMPLX_0:def 7
.= 0 by E1
.= 1 * (0 " ) by XCMPLX_0:def 7
.= 1 / 0 by XCMPLX_0:def 9
.= 1 / (abs c1) by E7, E1 ;

end;
suppose E7: c1 <> 0 ;
then ((abs c1) * (abs (1 / c1))) * (1 / (abs c1)) = 1 * (1 / (abs c1)) by E6;
then E8: (abs (1 / c1)) * ((abs c1) * (1 / (abs c1))) = 1 / (abs c1) ;
abs c1 <> 0 by E7, E3;
then (abs (1 / c1)) * 1 = 1 / (abs c1) by E8, XCMPLX_1:107;
hence abs (1 / c1) = 1 / (abs c1) ;
end;
end;
end;

E7: for b1, b2 being real number holds abs (b1 / b2) = (abs b1) / (abs b2)
by COMPLEX1:153;

theorem :: ABSVALUE:16
canceled;

theorem :: ABSVALUE:17
canceled;

theorem :: ABSVALUE:18
canceled;

theorem :: ABSVALUE:19
canceled;

theorem :: ABSVALUE:20
for b1, b2 being real number holds
( 0 <= b1 * b2 implies sqrt (b1 * b2) = (sqrt (abs b1)) * (sqrt (abs b2)) )
proof
let c1, c2 be real number ;
assume 0 <= c1 * c2 ;
then abs (c1 * c2) = c1 * c2 by E1;
then ( (abs c1) * (abs c2) = c1 * c2 & 0 <= abs c1 & 0 <= abs c2 ) by E2, E4;
hence sqrt (c1 * c2) = (sqrt (abs c1)) * (sqrt (abs c2)) by SQUARE_1:97;
end;

theorem :: ABSVALUE:21
for b1, b2, b3, b4 being real number holds
( ( abs b1 <= b2 & abs b3 <= b4 ) implies ( abs (b1 + b3) <= b2 + b4 ) )
proof
let c1, c2, c3, c4 be real number ;
assume that
E8: abs c1 <= c2 and
E9: abs c3 <= c4 ;
E10: abs (c1 + c3) <= (abs c1) + (abs c3) by E5;
(abs c1) + (abs c3) <= c2 + c4 by E8, E9, XREAL_1:9;
hence abs (c1 + c3) <= c2 + c4 by E10, XXREAL_0:2;
end;

theorem :: ABSVALUE:22
canceled;

theorem :: ABSVALUE:23
for b1, b2 being real number holds
( 0 < b1 / b2 implies sqrt (b1 / b2) = (sqrt (abs b1)) / (sqrt (abs b2)) )
proof
let c1, c2 be real number ;
assume 0 < c1 / c2 ;
then ( c1 / c2 = abs (c1 / c2) & 0 <= abs c2 ) by E1, E2;
then ( c1 / c2 = (abs c1) / (abs c2) & 0 <= abs c1 & 0 <= abs c2 ) by E2, E7;
hence sqrt (c1 / c2) = (sqrt (abs c1)) / (sqrt (abs c2)) by SQUARE_1:99;
end;

theorem :: ABSVALUE:24
for b1, b2 being real number holds
( 0 <= b1 * b2 implies abs (b1 + b2) = (abs b1) + (abs b2) )
proof
let c1, c2 be real number ;
assume E8: 0 <= c1 * c2 ;
per cases not ( not c1 * c2 = 0 & not 0 < c1 * c2 ) by E8, REAL_1:def 5;
suppose E9: c1 * c2 = 0 ;
per cases ( c1 = 0 or c2 = 0 ) by E9, XCMPLX_1:6;
suppose E10: c1 = 0 ;
then (abs c1) + (abs c2) = 0 + (abs c2) by E1
.= abs c2 ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E10;
end;
suppose E10: c2 = 0 ;
then (abs c1) + (abs c2) = (abs c1) + 0 by E1
.= abs c1 ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E10;
end;
end;
end;
suppose E9: 0 < c1 * c2 ;
E10: ( ( c1 < 0 & c2 < 0 ) or ( 0 < c1 & 0 < c2 ) )
proof
E11: ( c1 <> 0 & c2 <> 0 ) by E9;
E12: not ( c1 < 0 & 0 < c2 & not c1 * c2 < c1 * 0 ) by XREAL_1:71;
not ( 0 < c1 & c2 < 0 & not c1 * c2 < c1 * 0 ) by XREAL_1:70;
hence ( ( c1 < 0 & c2 < 0 ) or ( 0 < c1 & 0 < c2 ) ) by E9, E11, E12, XXREAL_0:1;
end;
per cases ( ( 0 < c1 & 0 < c2 ) or ( c1 < 0 & c2 < 0 ) ) by E10;
suppose that E11: 0 < c1 and
E12: 0 < c2 ;
E13: 0 + 0 < c1 + c2 by E11, E12, XREAL_1:10;
( abs c1 = c1 & abs c2 = c2 ) by E11, E12, E1;
then (abs c1) + (abs c2) = c1 + c2 ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E13, E1;
end;
suppose that E11: c1 < 0 and
E12: c2 < 0 ;
E13: c1 + c2 < 0 + 0 by E11, E12, XREAL_1:10;
abs c1 = - c1 by E11, E1;
then (abs c1) + (abs c2) = ((- 1) * c1) + (- (1 * c2)) by E12, E1
.= - (c1 + c2) ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E13, E1;
end;
end;
end;
end;
end;

theorem :: ABSVALUE:25
for b1, b2 being real number holds
( abs (b1 + b2) = (abs b1) + (abs b2) implies 0 <= b1 * b2 )
proof
let c1, c2 be real number ;
assume that
E8: abs (c1 + c2) = (abs c1) + (abs c2) and
E9: 0 > c1 * c2 ;
E10: not ( c1 * c2 < 0 & not ( c1 < 0 & 0 < c2 ) & not ( 0 < c1 & c2 < 0 ) )
proof
assume E11: c1 * c2 < 0 ;
then E12: ( c1 <> 0 & c2 <> 0 ) ;
E13: not ( c1 < 0 & c2 < 0 & not 0 * c1 < c1 * c2 ) by XREAL_1:71;
not ( 0 < c1 & 0 < c2 & not c1 * 0 < c1 * c2 ) by XREAL_1:70;
hence not ( not ( c1 < 0 & 0 < c2 ) & not ( 0 < c1 & c2 < 0 ) ) by E11, E12, E13, XXREAL_0:1;
end;
E11: not ( c1 < 0 & 0 < c2 & c1 + c2 < 0 & not abs (c1 + c2) <> (abs c1) + (abs c2) )
proof
assume that
E12: c1 < 0 and
E13: 0 < c2 and
E14: c1 + c2 < 0 ;
- c2 < - 0 by E13, XREAL_1:26;
then (- c2) + 0 < 0 + c2 by E13, XREAL_1:10;
then (- (1 * c1)) + (- c2) < (- c1) + c2 by XREAL_1:8;
then E15: - (1 * (c1 + c2)) < (- c1) + c2 ;
E16: abs c1 = - c1 by E12, E1;
abs c2 = c2 by E13, E1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E14, E15, E16, E1;
end;
E12: not ( c1 < 0 & 0 < c2 & 0 <= c1 + c2 & not abs (c1 + c2) <> (abs c1) + (abs c2) )
proof
assume that
E13: c1 < 0 and
E14: 0 < c2 and
E15: 0 <= c1 + c2 ;
0 < - c1 by E13, XREAL_1:60;
then c1 + 0 < 0 + (- c1) by E13, XREAL_1:10;
then E16: c1 + c2 < (- c1) + c2 by XREAL_1:8;
E17: abs c1 = - c1 by E13, E1;
abs c2 = c2 by E14, E1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E15, E16, E17, E1;
end;
E13: not ( 0 < c1 & c2 < 0 & c1 + c2 < 0 & not abs (c1 + c2) <> (abs c1) + (abs c2) )
proof
assume that
E14: 0 < c1 and
E15: c2 < 0 and
E16: c1 + c2 < 0 ;
- c1 < - 0 by E14, XREAL_1:26;
then (- c1) + 0 < 0 + c1 by E14, XREAL_1:10;
then (- (1 * c1)) + (- c2) < c1 + (- c2) by XREAL_1:8;
then E17: - (1 * (c1 + c2)) < c1 + (- c2) ;
E18: abs c1 = c1 by E14, E1;
abs c2 = - c2 by E15, E1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E16, E17, E18, E1;
end;
not ( 0 < c1 & c2 < 0 & 0 <= c1 + c2 & not abs (c1 + c2) <> (abs c1) + (abs c2) )
proof
assume that
E14: 0 < c1 and
E15: c2 < 0 and
E16: 0 <= c1 + c2 ;
0 < - c2 by E15, XREAL_1:60;
then 0 + c2 < (- c2) + 0 by E15, XREAL_1:10;
then E17: c1 + c2 < c1 + (- c2) by XREAL_1:8;
E18: abs c1 = c1 by E14, E1;
abs c2 = - c2 by E15, E1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E16, E17, E18, E1;
end;
hence not verum by E8, E9, E10, E11, E12, E13;
end;

theorem :: ABSVALUE:26
for b1, b2 being real number holds (abs (b1 + b2)) / (1 + (abs (b1 + b2))) <= ((abs b1) / (1 + (abs b1))) + ((abs b2) / (1 + (abs b2)))
proof
let c1, c2 be real number ;
set c3 = abs c1;
set c4 = abs c2;
set c5 = abs (c1 + c2);
E8: abs (c1 + c2) <= (abs c1) + (abs c2) by E5;
E9: 0 <= abs c1 by E2;
E10: 0 <= abs c2 by E2;
E11: 0 <= abs (c1 + c2) by E2;
E12: 0 + 0 <= (abs c1) + (abs c2) by E9, E10, XREAL_1:9;
then E13: 0 + 0 < 1 + ((abs c1) + (abs c2)) by XREAL_1:10;
E14: 0 < 1 + ((abs c1) + (abs c2)) by E12, XREAL_1:10;
E15: 0 + 0 < 1 + (abs (c1 + c2)) by E11, XREAL_1:10;
E16: 0 + 0 < 1 + (abs c1) by E9, XREAL_1:10;
E17: 0 + 0 < 1 + (abs c2) by E10, XREAL_1:10;
for b1, b2 being real number holds
( ( b1 <= b2 ) implies ( not 0 < 1 + b1 or not 0 < 1 + b2 or b1 / (1 + b1) <= b2 / (1 + b2) ) )
proof
let c6, c7 be real number ;
assume that
E18: c6 <= c7 and
E19: 0 < 1 + c6 and
E20: 0 < 1 + c7 ;
E21: (c6 * 1) + (c6 * c7) <= c7 + (c6 * c7) by E18, XREAL_1:8;
E22: 0 < (1 + c6) " by E19, XREAL_1:124;
E23: 0 < (1 + c7) " by E20, XREAL_1:124;
(c6 * (1 + c7)) * ((1 + c6) " ) <= (c7 * (1 + c6)) * ((1 + c6) " ) by E21, E22, XREAL_1:66;
then (c6 * (1 + c7)) * ((1 + c6) " ) <= c7 * ((1 + c6) * ((1 + c6) " )) ;
then (c6 * (1 + c7)) * ((1 + c6) " ) <= c7 * 1 by E19, XCMPLX_0:def 7;
then ((c6 * ((1 + c6) " )) * (1 + c7)) * ((1 + c7) " ) <= c7 * ((1 + c7) " ) by E23, XREAL_1:66;
then (c6 * ((1 + c6) " )) * ((1 + c7) * ((1 + c7) " )) <= c7 * ((1 + c7) " ) ;
then (c6 * ((1 + c6) " )) * 1 <= c7 * ((1 + c7) " ) by E20, XCMPLX_0:def 7;
then c6 / (1 + c6) <= c7 * ((1 + c7) " ) by XCMPLX_0:def 9;
hence c6 / (1 + c6) <= c7 / (1 + c7) by XCMPLX_0:def 9;
end;
then E18: (abs (c1 + c2)) / (1 + (abs (c1 + c2))) <= ((abs c1) + (abs c2)) / (1 + ((abs c1) + (abs c2))) by E8, E14, E15;
((abs c1) + (abs c2)) / ((1 + (abs c1)) + (abs c2)) <= ((abs c1) / (1 + (abs c1))) + ((abs c2) / (1 + (abs c2)))
proof
E19: ((abs c1) + (abs c2)) / ((1 + (abs c1)) + (abs c2)) = ((abs c1) / ((1 + (abs c1)) + (abs c2))) + ((abs c2) / ((1 + (abs c1)) + (abs c2))) by XCMPLX_1:63;
E20: ( ( ) implies ( not 0 < 1 + (abs c1) or not 0 < (1 + (abs c1)) + (abs c2) or (abs c1) / ((1 + (abs c1)) + (abs c2)) <= (abs c1) / (1 + (abs c1)) ) )
proof
assume that
E21: 0 < 1 + (abs c1) and
E22: 0 < (1 + (abs c1)) + (abs c2) ;
0 * (abs c2) <= (abs c1) * (abs c2) by E9, E10, XREAL_1:66;
then 0 + (abs c1) <= ((abs c1) * (abs c2)) + (abs c1) by XREAL_1:8;
then E23: ((abs c1) * 1) + ((abs c1) * (abs c1)) <= ((abs c1) * (1 + (abs c2))) + ((abs c1) * (abs c1)) by XREAL_1:8;
E24: 0 <= (1 + (abs c1)) " by E21, XREAL_1:124;
E25: 0 <= ((1 + (abs c1)) + (abs c2)) " by E22, XREAL_1:124;
((abs c1) * (1 + (abs c1))) * ((1 + (abs c1)) " ) <= ((abs c1) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c1)) " ) by E23, E24, XREAL_1:66;
then (abs c1) * ((1 + (abs c1)) * ((1 + (abs c1)) " )) <= ((abs c1) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c1)) " ) ;
then (abs c1) * 1 <= ((abs c1) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c1)) " ) by E16, XCMPLX_0:def 7;
then (abs c1) * (((1 + (abs c1)) + (abs c2)) " ) <= (((abs c1) * ((1 + (abs c1)) " )) * ((1 + (abs c1)) + (abs c2))) * (((1 + (abs c1)) + (abs c2)) " ) by E25, XREAL_1:66;
then (abs c1) * (((1 + (abs c1)) + (abs c2)) " ) <= ((abs c1) * ((1 + (abs c1)) " )) * (((1 + (abs c1)) + (abs c2)) * (((1 + (abs c1)) + (abs c2)) " )) ;
then (abs c1) * (((1 + (abs c1)) + (abs c2)) " ) <= ((abs c1) * ((1 + (abs c1)) " )) * 1 by E13, XCMPLX_0:def 7;
then (abs c1) / ((1 + (abs c1)) + (abs c2)) <= (abs c1) * ((1 + (abs c1)) " ) by XCMPLX_0:def 9;
hence (abs c1) / ((1 + (abs c1)) + (abs c2)) <= (abs c1) / (1 + (abs c1)) by XCMPLX_0:def 9;
end;
( ( ) implies ( not 0 < 1 + (abs c2) or not 0 < (1 + (abs c1)) + (abs c2) or (abs c2) / ((1 + (abs c1)) + (abs c2)) <= (abs c2) / (1 + (abs c2)) ) )
proof
assume that
E21: 0 < 1 + (abs c2) and
E22: 0 < (1 + (abs c1)) + (abs c2) ;
0 * (abs c2) <= (abs c1) * (abs c2) by E9, E10, XREAL_1:66;
then 0 + (abs c2) <= ((abs c1) * (abs c2)) + (abs c2) by XREAL_1:8;
then E23: ((abs c2) * 1) + ((abs c2) * (abs c2)) <= ((1 + (abs c1)) * (abs c2)) + ((abs c2) * (abs c2)) by XREAL_1:8;
E24: 0 <= (1 + (abs c2)) " by E21, XREAL_1:124;
E25: 0 <= ((1 + (abs c1)) + (abs c2)) " by E22, XREAL_1:124;
((abs c2) * (1 + (abs c2))) * ((1 + (abs c2)) " ) <= ((abs c2) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c2)) " ) by E23, E24, XREAL_1:66;
then (abs c2) * ((1 + (abs c2)) * ((1 + (abs c2)) " )) <= ((abs c2) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c2)) " ) ;
then (abs c2) * 1 <= ((abs c2) * ((1 + (abs c1)) + (abs c2))) * ((1 + (abs c2)) " ) by E17, XCMPLX_0:def 7;
then (abs c2) * (((1 + (abs c1)) + (abs c2)) " ) <= (((abs c2) * ((1 + (abs c2)) " )) * ((1 + (abs c1)) + (abs c2))) * (((1 + (abs c1)) + (abs c2)) " ) by E25, XREAL_1:66;
then (abs c2) * (((1 + (abs c1)) + (abs c2)) " ) <= ((abs c2) * ((1 + (abs c2)) " )) * (((1 + (abs c1)) + (abs c2)) * (((1 + (abs c1)) + (abs c2)) " )) ;
then (abs c2) * (((1 + (abs c1)) + (abs c2)) " ) <= ((abs c2) * ((1 + (abs c2)) " )) * 1 by E13, XCMPLX_0:def 7;
then (abs c2) / ((1 + (abs c1)) + (abs c2)) <= (abs c2) * ((1 + (abs c2)) " ) by XCMPLX_0:def 9;
hence (abs c2) / ((1 + (abs c1)) + (abs c2)) <= (abs c2) / (1 + (abs c2)) by XCMPLX_0:def 9;
end;
hence ((abs c1) + (abs c2)) / ((1 + (abs c1)) + (abs c2)) <= ((abs c1) / (1 + (abs c1))) + ((abs c2) / (1 + (abs c2))) by E10, E16, E19, E20, XREAL_1:9, XREAL_1:10;
end;
hence (abs (c1 + c2)) / (1 + (abs (c1 + c2))) <= ((abs c1) / (1 + (abs c1))) + ((abs c2) / (1 + (abs c2))) by E18, XXREAL_0:2;
end;

definition
let c1 be real number ;
func sgn c1 -> set equals :E8: :: ABSVALUE:def 2
1 if 0 < a1
- 1 if a1 < 0
otherwise 0;
coherence
( ( 0 < c1 implies 1 is set ) & ( c1 < 0 implies - 1 is set ) & ( ( not 0 < c1 & not c1 < 0 ) implies ( 0 is set ) ) ) ;
consistency
for b1 being set holds
( ( ) implies ( not 0 < c1 or not c1 < 0 or ( b1 = 1 iff b1 = - 1 ) ) ) ;
end;

:: deftheorem E8 defines sgn ABSVALUE:def 2 :
for b1 being real number holds
( ( 0 < b1 implies sgn b1 = 1 ) & ( b1 < 0 implies sgn b1 = - 1 ) & ( ( not 0 < b1 & not b1 < 0 ) implies ( sgn b1 = 0 ) ) );

registration
let c1 be real number ;
cluster sgn a1 -> real ;
coherence
sgn c1 is real
proof
not ( not 0 < c1 & not 0 > c1 & not c1 = 0 ) by REAL_1:def 5;
hence sgn c1 is real by E8;
end;
end;

definition
let c1 be Real;
redefine func sgn as sgn c1 -> Real;
coherence
sgn c1 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 b1 being real number holds
not ( sgn b1 = 1 & not 0 < b1 )
proof
let c1 be real number ;
assume that
E9: sgn c1 = 1 and
E10: 0 >= c1 ;
not ( not c1 < 0 & not c1 = 0 ) by E10, REAL_1:def 5;
hence not verum by E9, E8;
end;

theorem :: ABSVALUE:32
for b1 being real number holds
not ( sgn b1 = - 1 & not b1 < 0 )
proof
let c1 be real number ;
assume that
E9: sgn c1 = - 1 and
E10: c1 >= 0 ;
not ( not 0 < c1 & not c1 = 0 ) by E10, REAL_1:def 5;
hence not verum by E9, E8;
end;

theorem E9: :: ABSVALUE:33
for b1 being real number holds
( sgn b1 = 0 implies b1 = 0 )
proof
let c1 be real number ;
assume that
E10: sgn c1 = 0 and
E11: c1 <> 0 ;
not ( not 0 < c1 & not c1