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) )

A1: ( 0 < x & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )

proof

A5:
( 0 < x & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
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;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

proof

A9:
( x < 0 & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) )
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;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

proof

A13:
( x < 0 & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) )
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;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

proof

( ( x = 0 or y = 0 ) implies sgn (x * y) = (sgn x) * (sgn y) )
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;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

proof

hence
sgn (x * y) = (sgn x) * (sgn y)
by A1, A5, A13, A9; :: thesis: verum
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;then ( sgn x = 0 or sgn y = 0 ) by Def2;

hence sgn (x * y) = (sgn x) * (sgn y) by A17; :: thesis: verum