let a, b be Nat; :: thesis: ( ex q being Rational st a = q |^ b implies ex k being Integer st a = k |^ b )
given q being Rational such that A1: a = q |^ b ; :: thesis: ex k being Integer st a = k |^ b
now :: thesis: ex k being Integer st a = k |^ b
A2: now :: thesis: ( b <> 0 implies ex k being Integer st a = k |^ b )
set d = denominator q;
set k = numerator q;
assume b <> 0 ; :: thesis: ex k being Integer st a = k |^ b
then consider e being Nat such that
A3: e + 1 = b by NAT_1:6;
A4: (denominator q) |^ b <> 0 by CARD_4:3;
(numerator q) |^ b, denominator q are_coprime by Th10, Th22;
then A5: ((numerator q) |^ b) gcd (denominator q) = 1 by INT_2:def 3;
A6: q = (numerator q) / (denominator q) by RAT_1:15;
then a = ((numerator q) |^ b) / ((denominator q) |^ b) by A1, PREPOWER:8;
then a * ((denominator q) |^ b) = (numerator q) |^ b by A4, XCMPLX_1:87;
then (numerator q) |^ b = a * (((denominator q) |^ e) * (denominator q)) by A3, NEWTON:6
.= (a * ((denominator q) |^ e)) * (denominator q) ;
then denominator q divides (numerator q) |^ b ;
then ( denominator q = 1 or denominator q = - 1 ) by A5, INT_2:13, INT_2:22;
hence ex k being Integer st a = k |^ b by A1, A6; :: thesis: verum
end;
now :: thesis: ( b = 0 implies ex k being Integer st a = k |^ b )
assume A7: b = 0 ; :: thesis: ex k being Integer st a = k |^ b
then a = 1 by A1, NEWTON:4;
then a = 1 |^ 0 ;
hence ex k being Integer st a = k |^ b by A7; :: thesis: verum
end;
hence ex k being Integer st a = k |^ b by A2; :: thesis: verum
end;
hence ex k being Integer st a = k |^ b ; :: thesis: verum