per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: a to_power b is integer

then a in NAT by INT_1:3;
then reconsider aa = a as Nat ;
aa to_power b is Integer ;
hence a to_power b is integer ; :: thesis: verum

end;

suppose a < 0 ; :: thesis: a to_power b is integer

then reconsider aa = - a as Element of NAT by INT_1:3;

per cases ( b is odd or b is even ) ;

suppose b is odd ; :: thesis: a to_power b is integer

then (- aa) |^ b = - (aa |^ b) by POWER:2;
hence a to_power b is integer ; :: thesis: verum

end;

suppose b is even ; :: thesis: a to_power b is integer

then (- aa) |^ b = aa |^ b by POWER:1;
hence a to_power b is integer ; :: thesis: verum

end;

end;

end;

end;