let n be Nat; :: thesis: for p being Prime st n <> 0 holds
ex m, r being Nat st
( n = (p |^ r) * m & not p divides m )
let p be Prime; :: thesis: ( n <> 0 implies ex m, r being Nat st
( n = (p |^ r) * m & not p divides m ) )
set r = p |-count n;
A1: p <> 1 by NAT_4:12;
assume A2: n <> 0 ; :: thesis: ex m, r being Nat st
( n = (p |^ r) * m & not p divides m )
then p |^ (p |-count n) divides n by A1, NAT_3:def 7;
then consider m being Nat such that
A3: n = (p |^ (p |-count n)) * m by NAT_D:def 3;
take m ; :: thesis: ex r being Nat st
( n = (p |^ r) * m & not p divides m )
take p |-count n ; :: thesis: ( n = (p |^ (p |-count n)) * m & not p divides m )
thus n = (p |^ (p |-count n)) * m by A3; :: thesis: not p divides m
A4: not p |^ ((p |-count n) + 1) divides n by A2, A1, NAT_3:def 7;
thus not p divides m :: thesis: verum

proof

assume p divides m ; :: thesis: contradiction
then consider t being Nat such that
A5: m = p * t by NAT_D:def 3;
n = ((p |^ (p |-count n)) * p) * t by A3, A5
.= (p |^ ((p |-count n) + 1)) * t by NEWTON:6 ;
hence contradiction by A4, NAT_D:def 3; :: thesis: verum

end;