let x be Element of R; :: thesis: ( x is prime implies x is irreducible )
assume A: x is prime ; :: thesis: x is irreducible
now :: thesis: for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x )
let a be Element of R; :: thesis: ( not a divides x or a is Unit of R or a is_associated_to x )
assume C: a divides x ; :: thesis: ( a is Unit of R or a is_associated_to x )
then consider b being Element of R such that
D: a * b = x ;
b <> 0. R by A, D;
then H: b is right_mult-cancelable by ALGSTR_0:def 37;
now :: thesis: ( ( x divides a & a is_associated_to x ) or ( x divides b & a is Unit of R ) )
per cases ( x divides a or x divides b ) by A, D;
case x divides b ; :: thesis: a is Unit of R
then consider c being Element of R such that
F: x * c = b ;
(a * c) * b = x * c by D, GROUP_1:def 3
.= (1. R) * b by F ;
then a divides 1. R by H;
hence a is Unit of R by GCD_1:def 2; :: thesis: verum
end;
end;
end;
hence ( a is Unit of R or a is_associated_to x ) ; :: thesis: verum
end;
hence x is irreducible by A; :: thesis: verum