let x, y be Real; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
A1: ( 0 < x & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A2: 0 < x and
A3: 0 < y ; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
A4: sgn y = 1 by A3, Def2;
( 0 * y < x * y & sgn x = 1 ) by A2, A3, Def2, XREAL_1:68;
hence sgn (x * y) = (sgn x) * (sgn y) by A4, Def2; :: thesis: verum
end;
A5: ( 0 < x & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A6: 0 < x and
A7: y < 0 ; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
sgn y = - 1 by A7, Def2;
then A8: (sgn x) * (sgn y) = 1 * (- 1) by A6, Def2
.= - 1 ;
x * y < 0 * y by A6, A7, XREAL_1:69;
hence sgn (x * y) = (sgn x) * (sgn y) by A8, Def2; :: thesis: verum
end;
A9: ( x < 0 & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A10: x < 0 and
A11: y < 0 ; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
sgn y = - 1 by A11, Def2;
then A12: (sgn x) * (sgn y) = (- 1) * (- 1) by A10, Def2
.= 1 ;
x * 0 < x * y by A10, A11, XREAL_1:69;
hence sgn (x * y) = (sgn x) * (sgn y) by A12, Def2; :: thesis: verum
end;
A13: ( x < 0 & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume that
A14: x < 0 and
A15: 0 < y ; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
sgn y = 1 by A15, Def2;
then A16: (sgn x) * (sgn y) = - 1 by A14, Def2;
x * y < 0 * y by A14, A15, XREAL_1:68;
hence sgn (x * y) = (sgn x) * (sgn y) by A16, Def2; :: thesis: verum
end;
( ( x = 0 or y = 0 ) implies sgn (x * y) = (sgn x) * (sgn y) )
proof
assume A17: ( x = 0 or y = 0 ) ; :: thesis: sgn (x * y) = (sgn x) * (sgn y)
then ( sgn x = 0 or sgn y = 0 ) by Def2;
hence sgn (x * y) = (sgn x) * (sgn y) by A17; :: thesis: verum
end;
hence sgn (x * y) = (sgn x) * (sgn y) by A1, A5, A13, A9; :: thesis: verum