let p be Prime; :: thesis: for j, m, k being Nat st m = p |^ k & not p divides j holds
j gcd m = 1
let j, m, k be Nat; :: thesis: ( m = p |^ k & not p divides j implies j gcd m = 1 )
assume AS: ( m = p |^ k & not p divides j ) ; :: thesis: j gcd m = 1
assume A1: j gcd m <> 1 ; :: thesis: contradiction
set q = j gcd m;
j gcd m divides j by NAT_D:def 5;
then A4: j = (j gcd m) * (j div (j gcd m)) by NAT_D:3;
j gcd m divides m by NAT_D:def 5;
then consider n being Nat such that
A5: j gcd m = p |^ (n + 1) by A1, LM204K1, AS;
j = ((p |^ n) * p) * (j div (j gcd m)) by A4, A5, NEWTON:6
.= ((p |^ n) * (j div (j gcd m))) * p ;
hence contradiction by AS, INT_1:def 3; :: thesis: verum