:: ABSVALUE semantic presentation

definition
let c1 be real number ;
redefine func |.c1.| -> set equals :Def1: :: 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 Def1 defines |. ABSVALUE:def 1 :
for b1 being real number holds
( ( 0 <= b1 implies |.b1.| = b1 ) & ( not 0 <= b1 implies |.b1.| = - b1 ) );

theorem Th1: :: 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 Def1;
end;
suppose c1 < 0 ;
hence ( abs c1 = c1 or abs c1 = - c1 ) by Def1;
end;
end;
end;

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

Lemma3: for b1 being real number holds
not ( b1 <> 0 & not 0 < abs b1 )
by COMPLEX1:133;

theorem Th2: :: ABSVALUE:2
canceled;

theorem Th3: :: ABSVALUE:3
canceled;

theorem Th4: :: ABSVALUE:4
canceled;

theorem Th5: :: ABSVALUE:5
canceled;

theorem Th6: :: ABSVALUE:6
canceled;

theorem Th7: :: ABSVALUE:7
for b1 being real number holds
( b1 = 0 iff abs b1 = 0 ) by Def1, COMPLEX1:133;

theorem Th8: :: ABSVALUE:8
canceled;

theorem Th9: :: 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, Def1;
end;

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

theorem Th10: :: ABSVALUE:10
canceled;

theorem Th11: :: 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 Def1;
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 Def1;
- c1 <= - 0 by E5, XREAL_1:26;
hence ( - (abs c1) <= c1 & c1 <= abs c1 ) by E5, E6, XXREAL_0:2;
end;
end;
end;

theorem Th12: :: 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 Def1;
hence abs c2 <= c1 by E6, Def1;
end;
assume E5: abs c2 <= c1 ;
0 <= abs c2 by Lemma2;
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, Def1, XXREAL_0:2;
end;
suppose E7: c2 < 0 ;
then - c2 <= c1 by E5, Def1;
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;

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

theorem Th13: :: ABSVALUE:13
canceled;

theorem Th14: :: 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 Lemma4;
abs (c1 * (1 / c1)) = abs 1 by E7, XCMPLX_1:107;
hence (abs c1) * (abs (1 / c1)) = 1 by E8, Def1;
end;

theorem Th15: :: 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 Def1
.= 1 * (0 " ) by XCMPLX_0:def 7
.= 1 / 0 by XCMPLX_0:def 9
.= 1 / (abs c1) by E7, Def1 ;

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

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

theorem Th16: :: ABSVALUE:16
canceled;

theorem Th17: :: ABSVALUE:17
canceled;

theorem Th18: :: ABSVALUE:18
canceled;

theorem Th19: :: ABSVALUE:19
canceled;

theorem Th20: :: 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 Def1;
then ( (abs c1) * (abs c2) = c1 * c2 & 0 <= abs c1 & 0 <= abs c2 ) by Lemma2, Lemma4;
hence sqrt (c1 * c2) = (sqrt (abs c1)) * (sqrt (abs c2)) by SQUARE_1:97;
end;

theorem Th21: :: 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 Lemma5;
(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 Th22: :: ABSVALUE:22
canceled;

theorem Th23: :: 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 Def1, Lemma2;
then ( c1 / c2 = (abs c1) / (abs c2) & 0 <= abs c1 & 0 <= abs c2 ) by Lemma2, Lemma7;
hence sqrt (c1 / c2) = (sqrt (abs c1)) / (sqrt (abs c2)) by SQUARE_1:99;
end;

theorem Th24: :: 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 Def1
.= 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 Def1
.= 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, Def1;
then (abs c1) + (abs c2) = c1 + c2 ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E13, Def1;
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, Def1;
then (abs c1) + (abs c2) = ((- 1) * c1) + (- (1 * c2)) by E12, Def1
.= - (c1 + c2) ;
hence abs (c1 + c2) = (abs c1) + (abs c2) by E13, Def1;
end;
end;
end;
end;
end;

theorem Th25: :: 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, Def1;
abs c2 = c2 by E13, Def1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E14, E15, E16, Def1;
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, Def1;
abs c2 = c2 by E14, Def1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E15, E16, E17, Def1;
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, Def1;
abs c2 = - c2 by E15, Def1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E16, E17, E18, Def1;
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, Def1;
abs c2 = - c2 by E15, Def1;
hence abs (c1 + c2) <> (abs c1) + (abs c2) by E16, E17, E18, Def1;
end;
hence not verum by E8, E9, E10, E11, E12, E13;
end;

theorem Th26: :: 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 Lemma5;
E9: 0 <= abs c1 by Lemma2;
E10: 0 <= abs c2 by Lemma2;
E11: 0 <= abs (c1 + c2) by Lemma2;
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 & 0 < 1 + b1 & 0 < 1 + b2 implies 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: ( 0 < 1 + (abs c1) & 0 < (1 + (abs c1)) + (abs c2) implies (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;
( 0 < 1 + (abs c2) & 0 < (1 + (abs c1)) + (abs c2) implies (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;