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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: ( d divides p |^ (n + 1) implies S1[n + 1] )
assume A6: d divides p |^ (n + 1) ; :: thesis: S1[n + 1]
p |^ (n + 1) > 0 by A3, PREPOWER:6;
then A7: d <= p |^ (n + 1) by A6, NAT_D:7;
now :: thesis: S1[n + 1]
per cases ( d < p |^ (n + 1) or d = p |^ (n + 1) ) by A7, XXREAL_0:1;
suppose d < p |^ (n + 1) ; :: thesis: S1[n + 1]
then ex t being Element of NAT st
( d = p |^ t & t <= n ) by A1, A5, A6, Th33;
hence S1[n + 1] by NAT_1:12; :: thesis: verum
end;
suppose d = p |^ (n + 1) ; :: thesis: S1[n + 1]
hence S1[n + 1] ; :: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A8: S1[ 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 S1[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