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

proof

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

now

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

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
A5: n = p * i ;
consider u being Nat such that
A6: p |^ (k + 1) = (p * i) * u by A4, A5, NAT_D:def 3;
p * (p |^ k) = p * (i * u) by A6, NEWTON:11;
then A7: p |^ k = (p * (i * u)) div p by A2, NAT_D:18;
then A8: p |^ k = i * u by A2, NAT_D:18;
then A9: u divides p |^ k by NAT_D:def 3;
u <> 1 by A1, A5, A8, NEWTON:11;
then consider j being Element of NAT such that
A10: u = p * j by A1, A9, Th33;
p |^ k = n * j by A2, A5, A7, A10, NAT_D:18;
hence n divides p |^ k by NAT_D:def 3; :: 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:11; :: thesis: verum

end;

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