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

proof

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

now :: thesis: ( d divides p |^ (n + 1) implies S₁[n + 1] )

assume A6: d divides p |^ (n + 1) ; :: thesis: S₁[n + 1]
p |^ (n + 1) > 0 by A3, PREPOWER:6;
then A7: d <= p |^ (n + 1) by A6, NAT_D:7;

now :: thesis: S₁[n + 1]

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

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

then ex t being Element of NAT st
( d = p |^ t & t <= n ) by A1, A5, A6, Th33;
hence S₁[n + 1] by 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;

A8: S₁[ 0 ]

proof

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

proof

ex t being Nat st p |^ 0 = d * t by A9, NAT_D:def 3;
then d = 1 by NAT_1:15, NEWTON:4;
hence d = p |^ 0 by NEWTON:4; :: thesis: verum

end;

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

end;

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