let n, m be non zero Nat; :: thesis: ppf (n |^ m) = (ppf n) |^ m
now :: thesis: for i being object st i in SetPrimes holds
(ppf (n |^ m)) . i = ((ppf n) |^ m) . i
let i be object ; :: thesis: ( i in SetPrimes implies (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1 )
A1: m >= 0 + 1 by NAT_1:13;
A2: ((ppf n) |^ m) . i = ((ppf n) . i) |^ m by Def6;
assume i in SetPrimes ; :: thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A3: p |-count (n |^ m) = m * (p |-count n) by Th32;
per cases ( p |-count n = 0 or p |-count n <> 0 ) ;
suppose A4: p |-count n = 0 ; :: thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1
hence (ppf (n |^ m)) . i = 0 by A3, Th55
.= 0 |^ m by A1, NEWTON:11
.= ((ppf n) |^ m) . i by A2, A4, Th55 ;
:: thesis: verum
end;
suppose A5: p |-count n <> 0 ; :: thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1
hence (ppf (n |^ m)) . i = p |^ (p |-count (n |^ m)) by A3, Th56
.= (p |^ (p |-count n)) |^ m by A3, NEWTON:9
.= ((ppf n) |^ m) . i by A2, A5, Th56 ;
:: thesis: verum
end;
end;
end;
hence ppf (n |^ m) = (ppf n) |^ m ; :: thesis: verum