let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A
for f being Element of A st not f in sqrt J holds
J in Ideals (A,J,f)
let J be proper Ideal of A; :: thesis: for f being Element of A st not f in sqrt J holds
J in Ideals (A,J,f)
let f be Element of A; :: thesis: ( not f in sqrt J implies J in Ideals (A,J,f) )
assume A1: not f in sqrt J ; :: thesis: J in Ideals (A,J,f)
set I = J;
J /\ (multClSet (J,f)) = {}
proof
assume J /\ (multClSet (J,f)) <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in J /\ (multClSet (J,f)) by XBOOLE_0:def 1;
( x in J & x in multClSet (J,f) ) by A4, XBOOLE_0:def 4;
then consider n1 being Nat such that
A5: x = f |^ n1 ;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 12;
sqrt J = { a where a is Element of A : ex n being Element of NAT st a |^ n in J } by IDEAL_1:def 24;
then not f |^ n1 in J by A1;
hence contradiction by A4, A5, XBOOLE_0:def 4; :: thesis: verum
end;
hence J in Ideals (A,J,f) ; :: thesis: verum