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)
A: n in NAT by ORDINAL1:def 13;

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:133;

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:39;
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 ;
A4: ex k being Element of NAT st
( n = 2 * k or n = (2 * k) + 1 ) by A, SCHEME1:1;

now

per cases ( ex k being Integer st m = 2 * k or ex k being Integer st m = (2 * k) + 1 ) by A4;

suppose A5: ex k being Integer st m = 2 * k ; :: thesis: (abs a) to_power n = abs (a to_power n)

A6: (abs a) to_power n > 0 by A2, POWER:39;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= a to_power m by A1, A5, POWER:54 ;
hence (abs a) to_power n = abs (a to_power n) by A6, ABSVALUE:def 1; :: thesis: verum

end;

suppose A7: ex k being Integer st m = (2 * k) + 1 ; :: thesis: (abs a) to_power n = abs (a to_power n)

A8: (abs a) to_power n > 0 by A2, POWER:39;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= - (a to_power m) by A1, A7, POWER:55 ;
hence (abs a) to_power n = abs (- (a to_power n)) by A8, ABSVALUE:def 1
.= abs (a to_power n) by COMPLEX1:138 ;
:: 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 A9: 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:9;
hence (abs a) to_power n = abs (a to_power n) by A9, COMPLEX1:130, COMPLEX1:134; :: 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 A9, COMPLEX1:130, POWER:def 2;
hence (abs a) to_power n = abs (a to_power n) by A9, COMPLEX1:130; :: thesis: verum

end;

end;

end;

end;