let n be non zero Nat; :: thesis: for a, b being Nat st a,b are_coprime & n -root (a * b) is rational holds
n -root a is rational
let a, b be Nat; :: thesis: ( a,b are_coprime & n -root (a * b) is rational implies n -root a is rational )
assume A1: a,b are_coprime ; :: thesis: ( not n -root (a * b) is rational or n -root a is rational )
assume n -root (a * b) is rational ; :: thesis: n -root a is rational
then consider p being Integer, q being Nat such that
A3: ( q <> 0 & p / q = n -root (a * b) & ( for u being Integer
for w being Nat st w <> 0 & n -root (a * b) = u / w holds
q <= w ) ) by RAT_1:9;
p >= 0 by A3, POWER:7, NAT_1:14;
then p in NAT by INT_1:3;
then reconsider p = p as Nat ;
p |^ n = ((p |^ n) / (q |^ n)) * (q |^ n) by A3, XCMPLX_1:87
.= ((n -root (a * b)) |^ n) * (q |^ n) by A3, PREPOWER:8
.= (a * b) * (q |^ n) ;
then q |^ n divides p |^ n ;
then consider x being Nat such that
A4: p = q * x by NAT_D:def 3, NEWTON03:15;
n -root (a * b) = x by A3, A4, XCMPLX_1:89;
hence n -root a is rational by A1, Th7; :: thesis: verum