let c, a, b be Nat; :: thesis: ( a,b are_coprime implies for n being non zero Nat holds
( a * b = c |^ n iff ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) ) )
assume A1: a,b are_coprime ; :: thesis: for n being non zero Nat holds
( a * b = c |^ n iff ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) )
let n be non zero Nat; :: thesis: ( a * b = c |^ n iff ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) )
thus ( a * b = c |^ n implies ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) ) :: thesis: ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) implies a * b = c |^ n )

proof

assume B1: a * b = c |^ n ; :: thesis: ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) )
then consider k being Nat such that
B2: a = k |^ n by A1, NEWTON02:30;
consider l being Nat such that
B3: b = l |^ n by A1, B1, NEWTON02:30;
(n -root c) |^ n = n -root (a * b) by B1
.= (n -root a) * (n -root b) by POWER:11, NAT_1:14
.= ((n -root k) |^ n) * ((n -root l) |^ n) by B2, B3 ;
hence ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) by ORDINAL1:def 12, B2, B3; :: thesis: verum

end;

assume ( n -root a in NAT & n -root b in NAT & c = (n -root a) * (n -root b) ) ; :: thesis: a * b = c |^ n
then c |^ n = ((n -root a) |^ n) * ((n -root b) |^ n) by NEWTON:7;
hence a * b = c |^ n ; :: thesis: verum