let A be non degenerated commutative Ring; :: thesis: for a being Element of A
for p being prime Ideal of A
for k being non zero Nat st not a in p holds
not a |^ k in p
let a be Element of A; :: thesis: for p being prime Ideal of A
for k being non zero Nat st not a in p holds
not a |^ k in p
let p be prime Ideal of A; :: thesis: for k being non zero Nat st not a in p holds
not a |^ k in p
let k be non zero Nat; :: thesis: ( not a in p implies not a |^ k in p )
assume A1: not a in p ; :: thesis: not a |^ k in p
not a |^ k in p
proof
defpred S1[ Nat] means not a |^ $1 in p;
A2: S1[1] by A1, BINOM:8;
A3: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
A5: a |^ (k + 1) = (a |^ k) * (a |^ 1) by BINOM:10;
not a |^ 1 in p by A1, BINOM:8;
hence S1[k + 1] by A4, A5, RING_1:def 1; :: thesis: verum
end;
for k being non zero Nat holds S1[k] from NAT_1:sch 10(A2, A3);
 hence not a |^ k in p ; :: thesis: verum
end;
hence not a |^ k in p ; :: thesis: verum