let a, b be natural number ; :: thesis: for p being Prime st p divides a |^ b holds
p divides a
let p be Prime; :: thesis: ( p divides a |^ b implies p divides a )
assume that
A1: p divides a |^ b and
A2: not p divides a ; :: thesis: contradiction
reconsider p = p, a = a as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat] means p divides a |^ ($1 + 1);

now

assume 0 + 1 > b ; :: thesis: contradiction
then b <= 0 by NAT_1:13;
then b = 0 ;
then p divides 1 by A1, NEWTON:9;
then p = 1 by WSIERP_1:20;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

then b = (b -' 1) + 1 by XREAL_1:237;
then A3: ex k being Nat st S₁[k] by A1;
A4: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex n being Nat st
( n < k & S₁[n] ) )
assume that
A5: k <> 0 and
A6: S₁[k] ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
take k -' 1 ; :: thesis: ( k -' 1 < k & S₁[k -' 1] )
k > 0 by A5;
then A7: k >= 0 + 1 by NAT_1:13;
then k - 1 >= (0 + 1) - 1 by XREAL_1:15;
then k -' 1 = k - 1 by XREAL_0:def 2;
then k -' 1 < k - 0 by XREAL_1:17;
hence k -' 1 < k ; :: thesis: S₁[k -' 1]
A8: (k -' 1) + 1 = k by A7, XREAL_1:237;
p divides (a |^ k) * a by A6, NEWTON:11;
hence S₁[k -' 1] by A2, A8, NEWTON:98; :: thesis: verum

end;

S₁[ 0 ] from NAT_1:sch 7(A3, A4);
hence contradiction by A2, NEWTON:10; :: thesis: verum