let A be non degenerated commutative Ring; :: thesis: for I being proper Ideal of A
for x being Element of sqrt I ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
let I be proper Ideal of A; :: thesis: for x being Element of sqrt I ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
let x be Element of sqrt I; :: thesis: ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
set C = { n where n is Element of NAT : not x |^ n in I } ;
x in sqrt I ;
then x in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by IDEAL_1:def 24;
then consider x1 being Element of A such that
A1: x1 = x and
A2: ex n being Element of NAT st x1 |^ n in I ;
consider n1 being Element of NAT such that
A3: x1 |^ n1 in I by A2;
reconsider n1 = n1 as Element of NAT ;
A4: not n1 in { n where n is Element of NAT : not x |^ n in I }
proof
assume n1 in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: contradiction
then consider n0 being Element of NAT such that
A6: ( n0 = n1 & not x |^ n0 in I ) ;
thus contradiction by A3, A1, A6; :: thesis: verum
end;
assume A7: for m being Nat holds
( not m in { n where n is Element of NAT : not x |^ n in I } or not x |^ (m + 1) in I ) ; :: thesis: contradiction
A8: 0 in { n where n is Element of NAT : not x |^ n in I }
proof
set n = 0 ;
x |^ 0 = 1_ A by BINOM:8
.= 1. A ;
then not x |^ 0 in I by IDEAL_1:19;
hence 0 in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: verum
end;
{ n where n is Element of NAT : not x |^ n in I } = NAT
proof
defpred S1[ Nat] means $1 in { n where n is Element of NAT : not x |^ n in I } ;
A12: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
then not x |^ (n + 1) in I by A7;
hence S1[n + 1] ; :: thesis: verum
end;
A15: S1[ 0 ] by A8;
for n being Nat holds S1[n] from NAT_1:sch 2(A15, A12);
 then H: NAT c= { n where n is Element of NAT : not x |^ n in I } ;
{ n where n is Element of NAT : not x |^ n in I } c= NAT
proof
now :: thesis: for o being object st o in { n where n is Element of NAT : not x |^ n in I } holds
o in NAT
let o be object ; :: thesis: ( o in { n where n is Element of NAT : not x |^ n in I } implies o in NAT )
assume o in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: o in NAT
then consider n being Element of NAT such that
I: ( n = o & not x |^ n in I ) ;
thus o in NAT by I; :: thesis: verum
end;
hence { n where n is Element of NAT : not x |^ n in I } c= NAT ; :: thesis: verum
end;
hence { n where n is Element of NAT : not x |^ n in I } = NAT by H; :: thesis: verum
end;
hence contradiction by A4; :: thesis: verum