let p be Prime; :: thesis: for m, k being Nat st m divides p |^ k & m <> 1 holds
ex j being Nat st m = p |^ (j + 1)
let m, k be Nat; :: thesis: ( m divides p |^ k & m <> 1 implies ex j being Nat st m = p |^ (j + 1) )
assume AS1: ( m divides p |^ k & m <> 1 ) ; :: thesis: ex j being Nat st m = p |^ (j + 1)
then consider r being Nat such that
P1: ( m = p |^ r & r <= k ) by GROUPP_1:2;
r <> 0 by P1, AS1, NEWTON:4;
then 1 <= r by NAT_1:14;
then r - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider j = r - 1 as Nat ;
take j ; :: thesis: m = p |^ (j + 1)
thus m = p |^ (j + 1) by P1; :: thesis: verum