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 S1[ Nat] means p |-count (a |^ $1) = $1 * (p |-count a);
A2: for x being Nat st S1[x] holds
S1[x + 1]
proof
let x be Nat; :: thesis: ( S1[x] implies S1[x + 1] )
assume A3: S1[x] ; :: thesis: S1[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: S1[ 0 ] ;
for x being Nat holds S1[x] from NAT_1:sch 2(A4, A2);
 hence p |-count (a |^ b) = b * (p |-count a) ; :: thesis: verum