let x be ExtReal; :: thesis: ( -infty < x & x < +infty & x <> 0 implies |.x.| * |.(1. / x).| = 1. )
assume that
A1: ( -infty < x & x < +infty ) and
A2: x <> 0 ; :: thesis: |.x.| * |.(1. / x).| = 1.
reconsider a = x as Element of REAL by A1, XXREAL_0:14;
A3: 1. / x = 1 / a ;
per cases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; :: thesis: |.x.| * |.(1. / x).| = 1.
then ( |.x.| = a & |.(1. / x).| = 1 / a ) by Def1;
then |.x.| * |.(1. / x).| = a * (1 / a) by XXREAL_3:def 5;
hence |.x.| * |.(1. / x).| = 1. by A2, XCMPLX_1:106; :: thesis: verum
end;
suppose A4: not 0 <= x ; :: thesis: |.x.| * |.(1. / x).| = 1.
then A5: |.x.| = - x by Def1
.= - a by SUPINF_2:2 ;
|.(1. / x).| = - (1. / x) by A3, A4, Def1
.= - (1 / a) ;
then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, XXREAL_3:def 5
.= a * (1 / a) ;
hence |.x.| * |.(1. / x).| = 1. by A4, XCMPLX_1:106; :: thesis: verum
end;
end;