let p, d, k be Nat; :: thesis: ( p is prime & d > 1 & d divides p |^ k & not d divides (p |^ k) div p implies d = p |^ k )
assume A1: ( p is prime & d > 1 & d divides p |^ k & not d divides (p |^ k) div p ) ; :: thesis: d = p |^ k
then A2: p <> 0 by INT_2:def 5;
A3: k <> 0

proof

assume k = 0 ; :: thesis: contradiction
then p |^ k = 1 by NEWTON:9;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

then k >= 1 by NAT_1:14;
then A4: k - 1 >= 1 - 1 by XREAL_1:11;
consider t being Element of NAT such that
A5: ( d = p |^ t & t <= k ) by A1, Th35;
not t < k

proof

assume t < k ; :: thesis: contradiction
then t < (k + (- 1)) + 1 ;
then t < (k -' 1) + 1 by A4, XREAL_0:def 2;
then t <= k -' 1 by NAT_1:13;
then d divides p |^ (k -' 1) by A5, Lm6;
hence contradiction by A1, A2, A3, Th29, NAT_1:14; :: thesis: verum

end;

hence d = p |^ k by A5, XXREAL_0:1; :: thesis: verum