1 / r <> 1

proof

assume 1 / r = 1 ; :: thesis: contradiction
then r * (1 / r) = r ;
hence contradiction by Def01, XCMPLX_1:106; :: thesis: verum

end;

hence 1 / r is non zero non unit Real by Def01; :: thesis: verum