let A be non degenerated commutative Ring; :: thesis: for a being Element of A
for n being Nat
for p being prime Ideal of A st a |^ n in p holds
n <> 0
let a be Element of A; :: thesis: for n being Nat
for p being prime Ideal of A st a |^ n in p holds
n <> 0
let n be Nat; :: thesis: for p being prime Ideal of A st a |^ n in p holds
n <> 0
let p be prime Ideal of A; :: thesis: ( a |^ n in p implies n <> 0 )
assume A1: a |^ n in p ; :: thesis: n <> 0
assume n = 0 ; :: thesis: contradiction
then a |^ n = 1_ A by BINOM:8;
then A5: {(1. A)} c= p by A1, TARSKI:def 1;
p -Ideal = p by IDEAL_1:44;
then {(1. A)} -Ideal c= p by A5, IDEAL_1:57;
then the carrier of A = p by IDEAL_1:51;
then not p is proper ;
hence contradiction ; :: thesis: verum