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

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

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

proof

( x < 0 implies sgn x = sgn (1 / x) )
assume A2:
0 < x
; :: thesis: sgn x = sgn (1 / x)

sgn (1 / x) = 1 / (sgn x) by Th21;

then sgn (1 / x) = 1 / 1 by A2, Def2

.= 1 ;

hence sgn x = sgn (1 / x) by A2, Def2; :: thesis: verum

end;sgn (1 / x) = 1 / (sgn x) by Th21;

then sgn (1 / x) = 1 / 1 by A2, Def2

.= 1 ;

hence sgn x = sgn (1 / x) by A2, Def2; :: thesis: verum

proof

hence
sgn x = sgn (1 / x)
by A1; :: thesis: verum
assume A3:
x < 0
; :: thesis: sgn x = sgn (1 / x)

then sgn x = - 1 by Def2;

then sgn (1 / x) = 1 / (- 1) by Th21;

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

end;then sgn x = - 1 by Def2;

then sgn (1 / x) = 1 / (- 1) by Th21;

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