let x, y be real number ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A1: ( x < 0 & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A2: x < 0 and
A3: y < 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A4: x + y < 0 + 0 by A2, A3;
A5: sgn x = - 1 by A2, Def2;
A6: sgn y = - 1 by A3, Def2;
A7: sgn x = sgn (x + y) by A4, A5, Def2;
A8: ((sgn (x + y)) + (- 1)) - 1 < (((sgn (x + y)) + (- 1)) - 1) + 1 by XREAL_1:31;
(sgn (x + y)) + (- 1) < ((sgn (x + y)) + (- 1)) + 1 by XREAL_1:31;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A6, A7, A8, XXREAL_0:2; :: thesis: verum

end;

A9: ( x < 0 & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A10: x < 0 and
A11: 0 < y ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
sgn x = - 1 by A10, Def2;
then A12: (sgn x) + (sgn y) = (- 1) + 1 by A11, Def2
.= 0 ;
( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A12, Def2; :: 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: ( 0 < x & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume that
A18: 0 < x and
A19: 0 < y ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A20: 0 + 0 < x + y by A18, A19;
sgn y = 1 by A19, Def2;
then ((sgn x) + (sgn y)) - 1 = 1 by A18, Def2;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A20, Def2; :: thesis: verum

end;

( ( x = 0 or y = 0 ) implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume A21: ( x = 0 or y = 0 ) ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
A22: ( x = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume A23: x = 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then A24: ((sgn x) + (sgn y)) - 1 = (0 + (sgn y)) - 1 by Def2
.= (sgn y) - 1 ;
(sgn y) - 1 < ((sgn y) + (- 1)) + 1 by XREAL_1:31;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A23, A24; :: thesis: verum

end;

( y = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) )

proof

assume A25: y = 0 ; :: thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y)
then A26: ((sgn x) + (sgn y)) - 1 = ((sgn x) + 0 ) - 1 by Def2
.= (sgn x) - 1 ;
(sgn x) - 1 < ((sgn x) + (- 1)) + 1 by XREAL_1:31;
hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A25, A26; :: thesis: verum

end;

hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A21, A22; :: thesis: verum

end;

hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A1, A9, A13, A17; :: thesis: verum