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

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