let x be real number ; :: thesis: ( x <> 0 implies (abs x) * (abs (1 / x)) = 1 )
assume A1: x <> 0 ; :: thesis: (abs x) * (abs (1 / x)) = 1
A2: (abs x) * (abs (1 / x)) = abs (x * (1 / x)) by COMPLEX1:151;
abs (x * (1 / x)) = abs 1 by A1, XCMPLX_1:107;
hence (abs x) * (abs (1 / x)) = 1 by A2, Def1; :: thesis: verum