let a, b be non zero Real; :: thesis: ( sgn ((1 / a) - (1 / b)) = sgn (b - a) iff sgn b = sgn a )
A1: ( sgn b = sgn a implies sgn ((1 / a) - (1 / b)) = sgn (b - a) )

proof

assume sgn a = sgn b ; :: thesis: sgn ((1 / a) - (1 / b)) = sgn (b - a)
then ( ( a is positive & b is positive ) or ( a is negative & b is negative ) ) ;
hence sgn ((1 / a) - (1 / b)) = sgn (b - a) by OPR, NPR; :: thesis: verum

end;

( sgn b <> sgn a implies sgn ((1 / a) - (1 / b)) <> sgn (b - a) )

proof

assume sgn b <> sgn a ; :: thesis: sgn ((1 / a) - (1 / b)) <> sgn (b - a)

per cases then ( sgn b > sgn a or sgn b < sgn a ) by XXREAL_0:1;

suppose sgn b > sgn a ; :: thesis: sgn ((1 / a) - (1 / b)) <> sgn (b - a)

then ( b is positive & a is negative ) by SGNZ;
hence sgn ((1 / a) - (1 / b)) <> sgn (b - a) ; :: thesis: verum

end;

suppose sgn b < sgn a ; :: thesis: sgn ((1 / a) - (1 / b)) <> sgn (b - a)

then ( b is negative & a is positive ) by SGNZ;
hence sgn ((1 / a) - (1 / b)) <> sgn (b - a) ; :: thesis: verum

end;

end;

end;

hence ( sgn ((1 / a) - (1 / b)) = sgn (b - a) iff sgn b = sgn a ) by A1; :: thesis: verum