let d, k, p be Nat; :: thesis: ( p is prime & d > 1 & d divides p |^ k & not d divides (p |^ k) div p implies d = p |^ k )
assume that
A1: p is prime and
A2: d > 1 and
A3: d divides p |^ k and
A4: not d divides (p |^ k) div p ; :: thesis: d = p |^ k
A5: k <> 0
proof
assume k = 0 ; :: thesis: contradiction
then p |^ k = 1 by NEWTON:4;
hence contradiction by A2, A3, NAT_D:7; :: thesis: verum
end;
then k >= 1 by NAT_1:14;
then A6: k - 1 >= 1 - 1 by XREAL_1:9;
consider t being Element of NAT such that
A7: d = p |^ t and
A8: t <= k by A1, A3, Th34;
A9: p <> 0 by A1, INT_2:def 4;
not t < k
proof
assume t < k ; :: thesis: contradiction
then t < (k + (- 1)) + 1 ;
then t < (k -' 1) + 1 by A6, XREAL_0:def 2;
then t <= k -' 1 by NAT_1:13;
then d divides p |^ (k -' 1) by A7, Lm6;
hence contradiction by A4, A9, A5, Th28, NAT_1:14; :: thesis: verum
end;
hence d = p |^ k by A7, A8, XXREAL_0:1; :: thesis: verum