let x be G_INTEG; :: thesis: ( Norm x = 1 iff ( x = 1 or x = - 1 or x = <i> or x = - <i> ) )

hereby :: thesis: ( ( x = 1 or x = - 1 or x = <i> or x = - <i> ) implies Norm x = 1 )

assume A1: Norm x = 1 ; :: thesis: ( x = 1 or x = - 1 or x = <i> or x = - <i> )
A2: x = (Re x) + ((Im x) * <i>) by COMPLEX1:13;
A3: Norm x = ((Re x) + ((Im x) * <i>)) * ((Re x) - ((Im x) * <i>)) by COMPLEX1:13
.= ((Re x) ^2) + ((Im x) ^2) ;
reconsider Rx = Re x, Ix = Im x as Element of INT by Def1;
( Rx ^2 in NAT & Ix ^2 in NAT ) by INT_1:3, XREAL_1:63;
then ( ( (Re x) ^2 = 1 & (Im x) ^2 = 0 ) or ( (Re x) ^2 = 0 & (Im x) ^2 = 1 ) ) by A1, A3, Th1;
then ( ( ( Rx = 1 or Rx = - 1 ) & Im x = 0 ) or ( Re x = 0 & ( Ix = 1 or Ix = - 1 ) ) ) by XCMPLX_1:182;
hence ( x = 1 or x = - 1 or x = <i> or x = - <i> ) by A2; :: thesis: verum

end;

assume A4: ( x = 1 or x = - 1 or x = <i> or x = - <i> ) ; :: thesis: Norm x = 1

per cases ( x = 1 or x = - 1 or x = <i> or x = - <i> ) by A4;

suppose x = 1 ; :: thesis: Norm x = 1

hence Norm x = 1 by COMPLEX1:30; :: thesis: verum

end;

suppose x = - 1 ; :: thesis: Norm x = 1

hence Norm x = (- 1) * (- (1 *')) by COMPLEX1:33
.= 1 by COMPLEX1:30 ;
:: thesis: verum

end;

suppose x = <i> ; :: thesis: Norm x = 1

hence Norm x = 1 by COMPLEX1:31; :: thesis: verum

end;

suppose x = - <i> ; :: thesis: Norm x = 1

hence Norm x = 1 by COMPLEX1:31; :: thesis: verum

end;

end;