theorem :: NEWTON02:30

for a, b, c, n being Nat st a,b are_coprime & a * b = c |^ n holds
ex k being Nat st k |^ n = a