let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for n being non zero Nat holds sqrt (p ||^ n) = p
let p be prime Ideal of A; :: thesis: for n being non zero Nat holds sqrt (p ||^ n) = p
let n be non zero Nat; :: thesis: sqrt (p ||^ n) = p
A1: p = sqrt p by TOPZARI1:25, TOPZARI1:20;
defpred S1[ Nat] means sqrt (p ||^ $1) = p;
A2: S1[1] by A1, Th8;
A3: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
A5: n > 0 ;
sqrt (p ||^ (n + 1)) = sqrt (p *' (p ||^ n)) by A5, Th10
.= sqrt (p /\ (p ||^ n)) by IDEAL_1:92
.= (sqrt p) /\ (sqrt (p ||^ n)) by Th12
.= p by A1, A4 ;
hence S1[n + 1] ; :: thesis: verum
end;
for i being non zero Nat holds S1[i] from NAT_1:sch 10(A2, A3);
 hence sqrt (p ||^ n) = p ; :: thesis: verum