let x, y be Real; :: thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )
hereby :: thesis: ( |.x.| <= y implies ( - y <= x & x <= y ) )
assume that
A1: - y <= x and
A2: x <= y ; :: thesis: |.x.| <= y
- x <= - (- y) by A1, XREAL_1:24;
hence |.x.| <= y by A2, Def1; :: thesis: verum
end;
assume A3: |.x.| <= y ; :: thesis: ( - y <= x & x <= y )
then A4: 0 <= y by COMPLEX1:46;
per cases ( 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;
suppose A5: 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 A3; :: thesis: verum
end;
end;