let x, y be G_INTEG; :: thesis: ( Re y <> 0 & Im y <> 0 & Re y <> Im y & - (Re y) <> Im y & x *' is_associated_to y implies ( not x Divides y & not y Divides x ) )
assume that
A1: ( Re y <> 0 & Im y <> 0 & Re y <> Im y & - (Re y) <> Im y ) and
A2: x *' is_associated_to y ; :: thesis: ( not x Divides y & not y Divides x )
A3: ( x *' is_associated_to x implies y *' is_associated_to y )
proof
assume A4: x *' is_associated_to x ; :: thesis: y *' is_associated_to y
then A5: x is_associated_to y by A2, Th42;
then x *' is_associated_to y *' by Th43;
then x is_associated_to y *' by A4, Th42;
hence y *' is_associated_to y by A5, Th42; :: thesis: verum
end;
A6: Norm (x *') <> 0
proof
assume Norm (x *') = 0 ; :: thesis: contradiction
then Norm y = 0 by A2, Lm10;
hence contradiction by A1, Th36, COMPLEX1:4; :: thesis: verum
end;
hereby :: thesis: not y Divides x
consider c being G_INTEG such that
A7: c is g_int_unit and
A8: x *' = c * y by A2, Th40;
assume x Divides y ; :: thesis: contradiction
then consider d being G_INTEG such that
A9: y = x * d ;
A10: x *' = (c * d) * x by A8, A9;
reconsider e = c * d as G_INTEG ;
A11: Norm e = (Norm c) * (Norm d) by Th34
.= Norm d by A7 ;
per cases ( d is g_int_unit or not d is g_int_unit ) ;
end;
end;
consider c being G_INTEG such that
A13: c is g_int_unit and
A14: y = c * (x *') by A2, Th40;
assume y Divides x ; :: thesis: contradiction
then consider d being G_INTEG such that
A15: x = y * d ;
A16: x = (c * d) * (x *') by A14, A15;
reconsider e = c * d as G_INTEG ;
A17: Norm e = (Norm c) * (Norm d) by Th34
.= Norm d by A13 ;
per cases ( d is g_int_unit or not d is g_int_unit ) ;
suppose d is g_int_unit ; :: thesis: contradiction
hence contradiction by A3, A1, A16, A17, Def20, Th40, Th41; :: thesis: verum
end;
suppose A18: not d is g_int_unit ; :: thesis: contradiction
Norm x = (Norm e) * (Norm (x *')) by A16, Th34;
hence contradiction by A17, A18, A6, XCMPLX_1:7; :: thesis: verum
end;
end;