let n be Nat; :: thesis: for p being Prime st n is positive & p is prime & p divides n holds
ex k, m being positive Nat st
( 0 < k & n = m * (p |^ k) & m,p are_coprime )
let p be Prime; :: thesis: ( n is positive & p is prime & p divides n implies ex k, m being positive Nat st
( 0 < k & n = m * (p |^ k) & m,p are_coprime ) )
assume A1: ( n is positive & p is prime & p divides n ) ; :: thesis: ex k, m being positive Nat st
( 0 < k & n = m * (p |^ k) & m,p are_coprime )
then 1 + 1 <= p by NAT_1:13;
then consider up being positive Nat such that
A2: n <= p |^ up by LIOUVIL2:1;
defpred S₁[ Nat] means p |^ $1 divides n;
A3: for k being Nat st S₁[k] holds
k <= up

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= up )
assume S₁[k] ; :: thesis: k <= up
then p |^ k <= n by A1, NAT_D:7;
then p |^ k <= p |^ up by A2, XXREAL_0:2;
then ( p |^ k < p |^ up or p |^ k = p |^ up ) by XXREAL_0:1;
hence k <= up by A1, PREPOWER:93, PEPIN:30; :: thesis: verum

end;

p = p |^ 1 ;
then A4: ex k being Nat st S₁[k] by A1;
consider k being Nat such that
A5: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A3, A4);
consider m being Nat such that
A6: n = (p |^ k) * m by A5, NAT_D:def 3;
S₁[1] by A1;
then reconsider k = k, m = m as positive Nat by A5, A6, A1;
take k ; :: thesis: ex m being positive Nat st
( 0 < k & n = m * (p |^ k) & m,p are_coprime )
take m ; :: thesis: ( 0 < k & n = m * (p |^ k) & m,p are_coprime )
thus ( 0 < k & n = m * (p |^ k) ) by A6; :: thesis: m,p are_coprime
assume not m,p are_coprime ; :: thesis: contradiction
then m gcd p = p by PEPIN:2;
then p divides m by NAT_D:def 5;
then consider m1 being Nat such that
A7: m = p * m1 by NAT_D:def 3;
p * (p |^ k) = p |^ (k + 1) by NEWTON:6;
then n = m1 * (p |^ (k + 1)) by A6, A7;
then p |^ (k + 1) divides n ;
then k + 1 <= k by A5;
hence contradiction by NAT_1:13; :: thesis: verum