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 S₁[ Nat] means not a |^ $1 in p;
A2: S₁[1] by A1, BINOM:8;
A3: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: a |^ (k + 1) = (a |^ k) * (a |^ 1) by BINOM:10;
not a |^ 1 in p by A1, BINOM:8;
hence S₁[k + 1] by A4, A5, RING_1:def 1; :: thesis: verum

end;

for k being non zero Nat holds S₁[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