let x be real number ; :: thesis: sgn x = sgn (1 / x)

per cases ( x = 0 or x <> 0 ) ;

suppose A1: x = 0 ; :: thesis: sgn x = sgn (1 / x)

thus sgn x = sgn (1 / x) by A1; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: sgn x = sgn (1 / x)

A3: ( x < 0 implies sgn x = sgn (1 / x) )

proof

assume A4: x < 0 ; :: thesis: sgn x = sgn (1 / x)
then sgn x = - 1 by Def2;
then sgn (1 / x) = 1 / (- 1) by Th39;
hence sgn x = sgn (1 / x) by A4, Def2; :: thesis: verum

end;

( 0 < x implies sgn x = sgn (1 / x) )

proof

assume A5: 0 < x ; :: thesis: sgn x = sgn (1 / x)
sgn (1 / x) = 1 / (sgn x) by Th39;
then sgn (1 / x) = 1 / 1 by A5, Def2
.= 1 ;
hence sgn x = sgn (1 / x) by A5, Def2; :: thesis: verum

end;

hence sgn x = sgn (1 / x) by A3; :: thesis: verum

end;

end;