let n be non zero Nat; :: thesis: for p being Prime ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )
let p be Prime; :: thesis: ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )

per cases ( p divides n or not p divides n ) ;

suppose AS: p divides n ; :: thesis: ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )

defpred S₁[ Nat] means p |^ $1 divides n;

A: now :: thesis: for k being Nat st S₁[k] holds
k <= n

let k be Nat; :: thesis: ( S₁[k] implies k <= n )
assume A0: S₁[k] ; :: thesis: k <= n
A2: p |^ k <= n by A0, NAT_D:7;

now :: thesis: not k > n

assume k > n ; :: thesis: contradiction
then A3: p |^ k > p |^ n by NAT_6:2;
p > 1 by INT_2:def 4;
then p >= 1 + 1 by INT_1:7;
then p |^ n > n by NEWTON:86;
hence contradiction by A2, A3, XXREAL_0:2; :: thesis: verum

end;

hence k <= n ; :: thesis: verum

end;

p |^ 1 = p ;
then B: ex k being Nat st S₁[k] by AS;
consider k being Nat such that
C: ( S₁[k] & ( for m being Nat st S₁[m] holds
m <= k ) ) from NAT_1:sch 6(A, B);
( p |^ k divides n & not p |^ k is zero ) by C, NEWTON:87;
then n / (p |^ k) is Nat by Lm3b;
then consider m being Nat such that
D: m = n / (p |^ k) ;
take k ; :: thesis: ex m being Nat st
( n = m * (p |^ k) & not p divides m )
take m ; :: thesis: ( n = m * (p |^ k) & not p divides m )
E: p |^ k > 0 by NEWTON:83;
thus F: n = n * 1
.= n * ((p |^ k) / (p |^ k)) by E, XCMPLX_1:60
.= m * (p |^ k) by D ; :: thesis: not p divides m

now :: thesis: not p divides m

assume p divides m ; :: thesis: contradiction
then consider l being Nat such that
G: p * l = m by NAT_D:def 3;
H: k + 0 < k + 1 by XREAL_1:8;
n = l * (p * (p |^ k)) by G, F
.= l * (p |^ (k + 1)) by NEWTON:6 ;
hence contradiction by C, H, NAT_D:def 3; :: thesis: verum

end;

hence not p divides m ; :: thesis: verum

end;

suppose AS: not p divides n ; :: thesis: ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )

take 0 ; :: thesis: ex m being Nat st
( n = m * (p |^ 0) & not p divides m )
take n ; :: thesis: ( n = n * (p |^ 0) & not p divides n )
thus n = n * 1
.= n * (p |^ 0) by NEWTON:4 ; :: thesis: not p divides n
thus not p divides n by AS; :: thesis: verum

end;

end;