let a, d be Nat; :: thesis: ( ex q being Rational st a = q |^ d implies ex b being Nat st a = b |^ d )
assume ex q being Rational st a = q |^ d ; :: thesis: ex b being Nat st a = b |^ d
then consider k being Integer such that
A1: a = k |^ d by Th24;
A2: now :: thesis: ( a = 0 implies ex b being Nat st a = b |^ d )
assume A3: a = 0 ; :: thesis: ex b being Nat st a = b |^ d
then d <> 0 by A1, NEWTON:4;
then a = 0 |^ d by A3, NAT_1:14, NEWTON:11;
hence ex b being Nat st a = b |^ d ; :: thesis: verum
end;
per cases ( d <> 0 or d = 0 ) ;
suppose d <> 0 ; :: thesis: ex b being Nat st a = b |^ d
now :: thesis: ( k is not Nat implies ex b being Nat st a = b |^ d )
consider e being Nat such that
A4: ( d = 2 * e or d = (2 * e) + 1 ) by Lm4;
consider c being Nat such that
A5: ( k = c or k = - c ) by INT_1:2;
assume A6: k is not Nat ; :: thesis: ex b being Nat st a = b |^ d
A7: now :: thesis: ( d = (2 * e) + 1 implies ex b being Nat st a = b |^ d )
assume d = (2 * e) + 1 ; :: thesis: ex b being Nat st a = b |^ d
then - (c |^ d) = a by A1, A6, A5, Th2;
hence ex b being Nat st a = b |^ d by A2; :: thesis: verum
end;
now :: thesis: ( d = 2 * e implies ex b being Nat st a = b |^ d )
assume d = 2 * e ; :: thesis: ex b being Nat st a = b |^ d
then a = c |^ d by A1, A5, Th2;
hence ex b being Nat st a = b |^ d ; :: thesis: verum
end;
hence ex b being Nat st a = b |^ d by A4, A7; :: thesis: verum
end;
hence ex b being Nat st a = b |^ d by A1; :: thesis: verum
end;
suppose A8: d = 0 ; :: thesis: ex b being Nat st a = b |^ d
then a = 1 by A1, NEWTON:4;
then a = 1 |^ 0 ;
hence ex b being Nat st a = b |^ d by A8; :: thesis: verum
end;
end;