let A be non degenerated commutative Ring; :: thesis: for I, J being proper Ideal of A st I c= J & J c= sqrt I & ( for x, y being Element of A st x * y in I & not x in I holds
y in J ) holds
( I is primary & sqrt I = J & J is prime )
let I, J be proper Ideal of A; :: thesis: ( I c= J & J c= sqrt I & ( for x, y being Element of A st x * y in I & not x in I holds
y in J ) implies ( I is primary & sqrt I = J & J is prime ) )
assume that
A1: ( I c= J & J c= sqrt I ) and
A2: for x, y being Element of A st x * y in I & not x in I holds
y in J ; :: thesis: ( I is primary & sqrt I = J & J is prime )
for x, y being Element of A st x * y in I & not x in I holds
y in sqrt I by A1, A2;
then A3: I is primary by Def4;
sqrt I c= J

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sqrt I or x in J )
assume x in sqrt I ; :: thesis: x in J
then reconsider x0 = x as Element of sqrt I ;
consider m being Nat such that
A5: ( m in { n where n is Element of NAT : not x0 |^ n in I } & x0 |^ (m + 1) in I ) by Th43;
consider m0 being Element of NAT such that
A6: ( m0 = m & not x0 |^ m0 in I ) by A5;

per cases ( m = 0 or 1 <= m ) by NAT_1:25;

suppose m = 0 ; :: thesis: x in J

then x0 |^ (m + 1) = x0 by BINOM:8;
hence x in J by A1, A5; :: thesis: verum

end;

suppose 1 <= m ; :: thesis: x in J

reconsider x0 = x0 as Element of A ;
x0 |^ (m + 1) = (x0 |^ m) * (x0 |^ 1) by BINOM:10
.= (x0 |^ m) * x0 by BINOM:8 ;
hence x in J by A2, A5, A6; :: thesis: verum

end;

end;

end;

then sqrt I = J by A1;
hence ( I is primary & sqrt I = J & J is prime ) by A3; :: thesis: verum