let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds
( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
let I be Ideal of A; :: thesis: ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )
A1: ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) implies ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) )

proof

assume A2: ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) ) ; :: thesis: ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) )
A3: I is proper by A2;
for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent

proof

let z be Element of (A / I); :: thesis: ( z is zero_divisible implies z is nilpotent )
assume z is zero_divisible ; :: thesis: z is nilpotent
then consider y being Element of (A / I) such that
A5: ( y <> 0. (A / I) & y * z = 0. (A / I) ) ;
consider z0 being Element of A such that
A6: z = Class ((EqRel (A,I)),z0) by RING_1:11;
consider y0 being Element of A such that
A7: y = Class ((EqRel (A,I)),y0) by RING_1:11;
A8: not y0 in I

proof

assume y0 in I ; :: thesis: contradiction
then A10: y0 - (0. A) in I ;
y = Class ((EqRel (A,I)),(0. A)) by A7, A10, RING_1:6
.= 0. (A / I) by RING_1:def 6 ;
hence contradiction by A5; :: thesis: verum

end;

Class ((EqRel (A,I)),(0. A)) = 0. (A / I) by RING_1:def 6
.= Class ((EqRel (A,I)),(y0 * z0)) by A5, A6, A7, RING_1:14 ;
then (y0 * z0) - (0. A) in I by RING_1:6;
then A12: z0 in sqrt I by A8, A2;
z0 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by A12, IDEAL_1:def 24;
then consider z1 being Element of A such that
A13: z1 = z0 and
A14: ex n being Element of NAT st z1 |^ n in I ;
consider n1 being Element of NAT such that
A15: z1 |^ n1 in I by A14;
(z0 |^ n1) - (0. A) in I by A15, A13;
then A16: Class ((EqRel (A,I)),(z0 |^ n1)) = Class ((EqRel (A,I)),(0. A)) by RING_1:6
.= 0. (A / I) by RING_1:def 6 ;
n1 <> 0

proof

assume n1 = 0 ; :: thesis: contradiction
then A18: z0 |^ n1 = 1_ A by BINOM:8
.= 1. A ;
not I is proper by A15, A13, A18, IDEAL_1:19;
hence contradiction by A2; :: thesis: verum

end;

then reconsider n1 = n1 as non zero Nat ;
z |^ n1 = 0. (A / I) by A16, A6, FIELD_1:2;
hence z is nilpotent ; :: thesis: verum

end;

hence ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) by A3; :: thesis: verum

end;

( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) implies ( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) ) )

proof

assume A19: ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) ; :: thesis: ( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) )
for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I

proof

let x1, y1 be Element of A; :: thesis: ( x1 * y1 in I & not x1 in I implies y1 in sqrt I )
assume A20: ( x1 * y1 in I & not x1 in I ) ; :: thesis: y1 in sqrt I
then A21: (y1 * x1) - (0. A) in I ;
reconsider z = Class ((EqRel (A,I)),x1) as Element of (A / I) by RING_1:12;
reconsider y = Class ((EqRel (A,I)),y1) as Element of (A / I) by RING_1:12;
A22: z <> 0. (A / I)

proof

assume z = 0. (A / I) ; :: thesis: contradiction
then Class ((EqRel (A,I)),x1) = Class ((EqRel (A,I)),(0. A)) by RING_1:def 6;
then x1 - (0. A) in I by RING_1:6;
hence contradiction by A20; :: thesis: verum

end;

y * z = Class ((EqRel (A,I)),(y1 * x1)) by RING_1:14
.= Class ((EqRel (A,I)),(0. A)) by A21, RING_1:6
.= 0. (A / I) by RING_1:def 6 ;
then y is zero_divisible by A22;
then y is nilpotent by A19;
then consider n being non zero Nat such that
A25: y |^ n = 0. (A / I) ;
Class ((EqRel (A,I)),(y1 |^ n)) = 0. (A / I) by A25, FIELD_1:2
.= Class ((EqRel (A,I)),(0. A)) by RING_1:def 6 ;
then A26: (y1 |^ n) - (0. A) in I by RING_1:6;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider I = I as Subset of A ;
y1 |^ n1 in I by A26;
then y1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } ;
hence y1 in sqrt I by IDEAL_1:def 24; :: thesis: verum

end;

hence ( I <> [#] A & ( for x1, y1 being Element of A st x1 * y1 in I & not x1 in I holds
y1 in sqrt I ) ) by A19; :: thesis: verum

end;

hence ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds
z is nilpotent ) ) ) by A1; :: thesis: verum