let p be prime Nat; :: thesis: for a being non trivial Nat
for b being non zero Nat holds a |-count (p |^ b) <= b
let a be non trivial Nat; :: thesis: for b being non zero Nat holds a |-count (p |^ b) <= b
let b be non zero Nat; :: thesis: a |-count (p |^ b) <= b
A1: a > 1 by Def0;

per cases ( p = a or p <> a ) ;

suppose p = a ; :: thesis: a |-count (p |^ b) <= b

hence a |-count (p |^ b) <= b by Def0, NAT_3:25; :: thesis: verum

end;

suppose p <> a ; :: thesis: a |-count (p |^ b) <= b

then a |-count p = 0 by A1, NAT_3:24;
then not a |^ (0 + b) divides p |^ b by MOB16, WSIERP_1:26;
hence a |-count (p |^ b) <= b by Count1; :: thesis: verum

end;

end;