let n be non zero Nat; :: thesis: for p being Nat st p in dom (Euler_factorization n) holds
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) )
let p be Nat; :: thesis: ( p in dom (Euler_factorization n) implies ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) ) )
set f = Euler_factorization n;
assume p in dom (Euler_factorization n) ; :: thesis: ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) )
then consider c being non zero Nat such that
A1: ( c = p |-count n & (Euler_factorization n) . p = (p |^ c) - (p |^ (c - 1)) ) by Def1;
take c ; :: thesis: ( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) )
p |^ c = p |^ ((c - 1) + 1)
.= (p |^ (c - 1)) * p by NEWTON:6 ;
hence ( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) ) by A1; :: thesis: verum