let a, b, c, n be Nat; :: thesis: ( a,b are_coprime & a * b = c |^ n implies ex k being Nat st k |^ n = a )
assume A1: ( a,b are_coprime & a * b = c |^ n ) ; :: thesis: ex k being Nat st k |^ n = a
consider k being Nat such that
A3: k = a gcd c ;
per cases ( n = 0 or ( n > 0 & a = 0 ) or b = 0 or ( n > 0 & a > 0 & b > 0 ) ) ;
suppose B1: n = 0 ; :: thesis: ex k being Nat st k |^ n = a
then a = 1 |^ 0 by A1, NAT_1:15, NEWTON:4;
hence ex k being Nat st k |^ n = a by B1; :: thesis: verum
end;
suppose ( n > 0 & a = 0 ) ; :: thesis: ex k being Nat st k |^ n = a
then a = a |^ n by NEWTON:11, NAT_1:14;
hence ex k being Nat st k |^ n = a ; :: thesis: verum
end;
suppose b = 0 ; :: thesis: ex k being Nat st k |^ n = a
then a = 1 |^ n by A1;
hence ex k being Nat st k |^ n = a ; :: thesis: verum
end;
suppose B1: ( n > 0 & a > 0 & b > 0 ) ; :: thesis: ex k being Nat st k |^ n = a
then consider m being Nat such that
B2: n = 1 + m by NAT_1:10, NAT_1:14;
B3: a |^ m,b are_coprime by A1, WSIERP_1:10;
k |^ n = (a |^ n) gcd (c |^ n) by A3, Th7
.= ((a |^ m) * a) gcd (a * b) by A1, B2, NEWTON:6
.= a * 1 by B3, B1, EULER_1:15 ;
hence ex k being Nat st k |^ n = a ; :: thesis: verum
end;
end;