let a, b, c be Nat; :: thesis: for p being non trivial Nat st not a divides b holds
(p |^ a) |^ c <> p |^ b
let p be non trivial Nat; :: thesis: ( not a divides b implies (p |^ a) |^ c <> p |^ b )
assume A1: not a divides b ; :: thesis: (p |^ a) |^ c <> p |^ b
A2: ( p |^ (a * c) = p |^ b iff (p |^ a) |^ c = p |^ b ) by NEWTON:9;
p > 1 by Def0;
hence (p |^ a) |^ c <> p |^ b by A1, A2, PEPIN:30; :: thesis: verum