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

proof

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

end;