let k, p, n be Nat; :: thesis: ( p is prime & n < p |^ (k + 1) implies ( n divides p |^ (k + 1) iff n divides p |^ k ) )
assume that
A1: p is prime and
A2: n < p |^ (k + 1) ; :: thesis: ( n divides p |^ (k + 1) iff n divides p |^ k )
A3: p <> 0 by A1, INT_2:def 4;
A4: ( n divides p |^ (k + 1) implies n divides p |^ k )

proof

assume A5: n divides p |^ (k + 1) ; :: thesis: n divides p |^ k

now :: thesis: n divides p |^ k

per cases ( n = 1 or ex i being Element of NAT st n = p * i ) by A1, A5, Th32;

suppose n = 1 ; :: thesis: n divides p |^ k

hence n divides p |^ k by NAT_D:6; :: thesis: verum

end;

suppose ex i being Element of NAT st n = p * i ; :: thesis: n divides p |^ k

then consider i being Element of NAT such that
A6: n = p * i ;
consider u being Nat such that
A7: p |^ (k + 1) = (p * i) * u by A5, A6, NAT_D:def 3;
p * (p |^ k) = p * (i * u) by A7, NEWTON:6;
then A8: p |^ k = (p * (i * u)) div p by A3, NAT_D:18;
then A9: p |^ k = i * u by A3, NAT_D:18;
then A10: u divides p |^ k ;
u <> 1 by A2, A6, A9, NEWTON:6;
then consider j being Element of NAT such that
A11: u = p * j by A1, A10, Th32;
p |^ k = n * j by A3, A6, A8, A11, NAT_D:18;
hence n divides p |^ k ; :: thesis: verum

end;

end;

end;

hence n divides p |^ k ; :: thesis: verum

end;

( n divides p |^ k implies n divides p |^ (k + 1) )

proof

assume n divides p |^ k ; :: thesis: n divides p |^ (k + 1)
then n divides (p |^ k) * p by NAT_D:9;
hence n divides p |^ (k + 1) by NEWTON:6; :: thesis: verum

end;

hence ( n divides p |^ (k + 1) iff n divides p |^ k ) by A4; :: thesis: verum