let b be Nat; :: thesis: for p being Prime
for a being non zero Nat holds p |-count (a |^ b) = b * (p |-count a)
let p be Prime; :: thesis: for a being non zero Nat holds p |-count (a |^ b) = b * (p |-count a)
let a be non zero Nat; :: thesis: p |-count (a |^ b) = b * (p |-count a)
A1: p <> 1 by INT_2:def 4;
defpred S₁[ Nat] means p |-count (a |^ $1) = $1 * (p |-count a);
A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A3: S₁[x] ; :: thesis: S₁[x + 1]
thus p |-count (a |^ (x + 1)) = p |-count ((a |^ x) * a) by NEWTON:6
.= (x * (p |-count a)) + (1 * (p |-count a)) by A3, Th28
.= (x + 1) * (p |-count a) ; :: thesis: verum

end;

p |-count (a |^ 0) = p |-count 1 by NEWTON:4
.= 0 * (p |-count a) by A1, Th21 ;
then A4: S₁[ 0 ] ;
for x being Nat holds S₁[x] from NAT_1:sch 2(A4, A2);
hence p |-count (a |^ b) = b * (p |-count a) ; :: thesis: verum