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 ;
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 ;
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 ;
B3: a |^ m,b are_coprime by ;
k |^ n = (a |^ n) gcd (c |^ n) by
.= ((a |^ m) * a) gcd (a * b) by
.= a * 1 by ;
hence ex k being Nat st k |^ n = a ; :: thesis: verum
end;
end;