let q be G_INTEG; :: thesis: ( Norm q is Prime implies q is g_prime )
assume A1: Norm q is Prime ; :: thesis: q is g_prime
for z being G_INTEG holds
( not z Divides q or z is g_int_unit or z is_associated_to q )

proof

let z be G_INTEG; :: thesis: ( not z Divides q or z is g_int_unit or z is_associated_to q )

per cases ( z is g_int_unit or ( not z is g_int_unit & z is_associated_to q ) or ( not z is g_int_unit & not z is_associated_to q ) ) ;

suppose z is g_int_unit ; :: thesis: ( not z Divides q or z is g_int_unit or z is_associated_to q )

hence ( not z Divides q or z is g_int_unit or z is_associated_to q ) ; :: thesis: verum

end;

suppose ( not z is g_int_unit & z is_associated_to q ) ; :: thesis: ( not z Divides q or z is g_int_unit or z is_associated_to q )

hence ( not z Divides q or z is g_int_unit or z is_associated_to q ) ; :: thesis: verum

end;

suppose A2: ( not z is g_int_unit & not z is_associated_to q ) ; :: thesis: ( not z Divides q or z is g_int_unit or z is_associated_to q )

not z Divides q

proof

assume A3: z Divides q ; :: thesis: contradiction
consider c being G_INTEG such that
A4: q = z * c by A3;
A5: Norm q = (Norm z) * (Norm c) by A4, Th34;
then A6: Norm z divides Norm q by INT_1:def 3;
A7: Norm z > 1

proof

Norm z <> 0

proof

assume Norm z = 0 ; :: thesis: contradiction
then Norm q = 0 * (Norm c) by A4, Th34
.= 0 ;
hence contradiction by A1; :: thesis: verum

end;

then Norm z >= 0 + 1 by NAT_1:13;
hence Norm z > 1 by A2, XXREAL_0:1; :: thesis: verum

end;

A8: Norm c <> 1 by A2, A4, Def20, Th40;
Norm q <> Norm z by A1, A5, A8, XCMPLX_1:7;
hence contradiction by A1, A6, A7, INT_2:def 4; :: thesis: verum

end;

hence ( not z Divides q or z is g_int_unit or z is_associated_to q ) ; :: thesis: verum

end;

end;

end;

hence q is g_prime by A1, INT_2:def 4; :: thesis: verum