let x, y be Real; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
A1: ( y = 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 )

proof

assume A2: y = 0 ; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then ((sgn x) + (sgn y)) + 1 = ((sgn x) + 0) + 1 by Def2
.= (sgn x) + 1 ;
hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A2, XREAL_1:29; :: thesis: verum

end;

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

proof

sgn x < (sgn x) + 1 by XREAL_1:29;
then A4: (sgn x) + 0 < ((sgn x) + 1) + 1 by XREAL_1:8;
assume A5: ( 0 < x & 0 < y ) ; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then ( sgn x = 1 & sgn y = 1 ) by Def2;
hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A5, A4, Def2; :: thesis: verum

end;

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

proof

assume that
A7: x < 0 and
A8: 0 < y ; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
sgn x = - 1 by A7, Def2;
then A9: ((sgn x) + (sgn y)) + 1 = 1 by A8, Def2;
( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A9, Def2; :: thesis: verum

end;

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

proof

assume that
A11: 0 < x and
A12: y < 0 ; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
sgn x = 1 by A11, Def2;
then A13: ((sgn x) + (sgn y)) + 1 = (1 + (- 1)) + 1 by A12, Def2
.= 1 ;
( x + y < 0 or x + y = 0 or 0 < x + y ) ;
hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A13, Def2; :: thesis: verum

end;

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

proof

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

end;

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

proof

assume A17: x = 0 ; :: thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1
then ((sgn x) + (sgn y)) + 1 = (0 + (sgn y)) + 1 by Def2
.= (sgn y) + 1 ;
hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A17, XREAL_1:29; :: thesis: verum

end;

hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A3, A10, A6, A14, A1; :: thesis: verum