let q be G_INTEG; :: thesis: ( Norm q is Prime & Norm q <> 2 implies ( Re q <> 0 & Im q <> 0 & Re q <> Im q & - (Re q) <> Im q ) )
assume A1: ( Norm q is Prime & Norm q <> 2 ) ; :: thesis: ( Re q <> 0 & Im q <> 0 & Re q <> Im q & - (Re q) <> Im q )
A2: (Re q) * (Re q) = (Re q) ^2
.= |.(Re q).| ^2 by COMPLEX1:75
.= |.(Re q).| * |.(Re q).| ;
A3: Norm q = ((Re q) + ((Im q) * <i>)) * ((Re q) - ((Im q) * <i>)) by COMPLEX1:13
.= ((Re q) ^2) + ((Im q) ^2) ;
assume A4: ( not Re q <> 0 or not Im q <> 0 or not Re q <> Im q or not - (Re q) <> Im q ) ; :: thesis: contradiction

per cases ( Re q = 0 or Im q = 0 or Re q = Im q or - (Re q) = Im q ) by A4;

suppose Re q = 0 ; :: thesis: contradiction

hence contradiction by A1, A3, Lm11; :: thesis: verum

end;

suppose Im q = 0 ; :: thesis: contradiction

hence contradiction by A1, A3, Lm11; :: thesis: verum

end;

suppose A5: Re q = Im q ; :: thesis: contradiction

then A6: Norm q = (2 * (Re q)) * (Re q) by A3;
|.(Re q).| <> 1 by A1, A3, A5, A2;
hence contradiction by A1, A6, Lm12; :: thesis: verum

end;

suppose A7: - (Re q) = Im q ; :: thesis: contradiction

then A8: Norm q = (2 * (Re q)) * (Re q) by A3;
|.(Re q).| <> 1 by A1, A3, A7, A2;
hence contradiction by A1, A8, Lm12; :: thesis: verum

end;

end;