let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds
( I is primary iff ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) )
let I be Ideal of A; :: thesis: ( I is primary iff ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) )
A1: ( I is primary implies ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) )
proof
assume I is primary ; :: thesis: ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) )
then ( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) ) by Th33;
hence ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) by Th34; :: thesis: verum
end;
( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) implies I is primary )
proof
assume ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) ; :: thesis: I is primary
then ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) ) by Th34;
hence I is primary by Th33; :: thesis: verum
end;
hence ( I is primary iff ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds
x is nilpotent ) ) ) by A1; :: thesis: verum