let n be non zero Nat; :: thesis: for a, b being Nat st a,b are_coprime & n -root (a * b) is Nat holds
n -root a is Nat
let a, b be Nat; :: thesis: ( a,b are_coprime & n -root (a * b) is Nat implies n -root a is Nat )
assume A1: a,b are_coprime ; :: thesis: ( not n -root (a * b) is Nat or n -root a is Nat )
assume n -root (a * b) is Nat ; :: thesis: n -root a is Nat
then reconsider k = n -root (a * b) as Nat ;
( k |^ n = (n -root (a * b)) |^ n & (n -root (a * b)) |^ n = a * b ) ;
then n -root a in NAT by A1, NEWTON03:14;
hence n -root a is Nat ; :: thesis: verum