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

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