let a be real number ; :: thesis: for n being natural number holds (abs a) to_power n = abs (a to_power n)
let n be natural number ; :: thesis: (abs a) to_power n = abs (a to_power n)

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

suppose A1: a <> 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

then A2: abs a > 0 by COMPLEX1:47;

now

per cases ( a > 0 or a < 0 ) by A1;

suppose a > 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

then ( a to_power n = (abs a) to_power n & a to_power n > 0 ) by ABSVALUE:def 1, POWER:34;
hence (abs a) to_power n = abs (a to_power n) by ABSVALUE:def 1; :: thesis: verum

end;

suppose A3: a < 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

reconsider m = n as Integer ;

now

per cases ( m is even or not m is even ) ;

suppose A4: m is even ; :: thesis: (abs a) to_power n = abs (a to_power n)

A5: (abs a) to_power n > 0 by A2, POWER:34;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= a to_power m by A4, POWER:47 ;
hence (abs a) to_power n = abs (a to_power n) by A5, ABSVALUE:def 1; :: thesis: verum

end;

suppose A6: not m is even ; :: thesis: (abs a) to_power n = abs (a to_power n)

A7: (abs a) to_power n > 0 by A2, POWER:34;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= - (a to_power m) by A6, POWER:48 ;
hence (abs a) to_power n = abs (- (a to_power n)) by A7, ABSVALUE:def 1
.= abs (a to_power n) by COMPLEX1:52 ;
:: thesis: verum

end;

end;

end;

hence (abs a) to_power n = abs (a to_power n) ; :: thesis: verum

end;

end;

end;

hence (abs a) to_power n = abs (a to_power n) ; :: thesis: verum

end;

suppose A8: a = 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

then a to_power n = 1 by NEWTON:4;
hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44, COMPLEX1:48; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (abs a) to_power n = abs (a to_power n)

then (abs a) to_power n = 0 by A8, COMPLEX1:44, POWER:def 2;
hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44; :: thesis: verum

end;

end;

end;

end;