let x be real number ; :: thesis: ( x <> 0 implies (abs x) * (abs (1 / x)) = 1 )
assume x <> 0 ; :: thesis: (abs x) * (abs (1 / x)) = 1
then ( (abs x) * (abs (1 / x)) = abs (x * (1 / x)) & abs (x * (1 / x)) = abs 1 ) by COMPLEX1:65, XCMPLX_1:106;
hence (abs x) * (abs (1 / x)) = 1 by Def1; :: thesis: verum