let p, d, n be Nat; :: thesis: ( p is prime & d divides p |^ n & d <> 0 implies ex t being Element of NAT st
( d = p |^ t & t <= n ) )
assume A1: ( p is prime & d divides p |^ n & d <> 0 ) ; :: thesis: ex t being Element of NAT st
( d = p |^ t & t <= n )
then A2: p > 0 by INT_2:def 5;
defpred S₁[ Nat] means ( d divides p |^ $1 implies ex t being Element of NAT st
( d = p |^ t & t <= $1 ) );
A3: S₁[ 0 ]

proof

assume A4: d divides p |^ 0 ; :: thesis: ex t being Element of NAT st
( d = p |^ t & t <= 0 )
d = p |^ 0

proof

consider t being Nat such that
A5: p |^ 0 = d * t by A4, NAT_D:def 3;
d = 1 by A5, NAT_1:15, NEWTON:9;
hence d = p |^ 0 by NEWTON:9; :: thesis: verum

end;

hence ex t being Element of NAT st
( d = p |^ t & t <= 0 ) ; :: thesis: verum

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]

now

assume A8: d divides p |^ (n + 1) ; :: thesis: S₁[n + 1]
p |^ (n + 1) > 0 by A2, PREPOWER:13;
then A9: d <= p |^ (n + 1) by A8, NAT_D:7;

now

per cases ( d < p |^ (n + 1) or d = p |^ (n + 1) ) by A9, XXREAL_0:1;

suppose d < p |^ (n + 1) ; :: thesis: S₁[n + 1]

then consider t being Element of NAT such that
A10: ( d = p |^ t & t <= n ) by A1, A7, A8, Th34;
thus S₁[n + 1] by A10, NAT_1:12; :: thesis: verum

end;

suppose d = p |^ (n + 1) ; :: thesis: S₁[n + 1]

hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
hence ex t being Element of NAT st
( d = p |^ t & t <= n ) by A1; :: thesis: verum