let a, b be Real; :: thesis: ( ( - b <= a & a <= b ) iff |.a.| <= b )
A1: ( |.a.| <= b implies ( - b <= a & a <= b ) )
proof
assume A2: |.a.| <= b ; :: thesis: ( - b <= a & a <= b )
( a < - 0 implies ( - b <= a & a <= b ) )
proof
assume A3: a < - 0 ; :: thesis: ( - b <= a & a <= b )
then - a <= b by A2, Lm27;
then - b <= - (- a) by XREAL_1:24;
hence ( - b <= a & a <= b ) by A3; :: thesis: verum
end;
hence ( - b <= a & a <= b ) by A2, Th43; :: thesis: verum
end;
( - b <= a & a <= b implies |.a.| <= b )
proof
assume that
A4: - b <= a and
A5: a <= b ; :: thesis: |.a.| <= b
- a <= - (- b) by A4, XREAL_1:24;
then ( a < 0 implies |.a.| <= b ) by Lm27;
hence |.a.| <= b by A5, Th43; :: thesis: verum
end;
hence ( ( - b <= a & a <= b ) iff |.a.| <= b ) by A1; :: thesis: verum