let a, b be Nat; :: 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 12;
defpred S₁[ Nat] means p divides a |^ ($1 + 1);
A3: 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
A4: k <> 0 and
A5: S₁[k] ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
A6: p divides (a |^ k) * a by A5, NEWTON:6;
take k -' 1 ; :: thesis: ( k -' 1 < k & S₁[k -' 1] )
A7: k >= 0 + 1 by A4, NAT_1:13;
then k - 1 >= (0 + 1) - 1 by XREAL_1:13;
then k -' 1 = k - 1 by XREAL_0:def 2;
then k -' 1 < k - 0 by XREAL_1:15;
hence k -' 1 < k ; :: thesis: S₁[k -' 1]
(k -' 1) + 1 = k by A7, XREAL_1:235;
hence S₁[k -' 1] by A2, A6, NEWTON:80; :: thesis: verum

end;

now :: thesis: not 0 + 1 > b

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

end;

then b = (b -' 1) + 1 by XREAL_1:235;
then A8: ex k being Nat st S₁[k] by A1;
S₁[ 0 ] from NAT_1:sch 7(A8, A3);
hence contradiction by A2; :: thesis: verum