let n be Element of NAT ; :: thesis: abs ((- 1) |^ n) = 1

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

suppose A1: n is even ; :: thesis: abs ((- 1) |^ n) = 1

(- 1) |^ n = (- 1) to_power n by POWER:41
.= 1 to_power n by A1, POWER:47
.= 1 by POWER:26 ;
hence abs ((- 1) |^ n) = 1 by ABSVALUE:def 1; :: thesis: verum

end;

suppose A2: not n is even ; :: thesis: abs ((- 1) |^ n) = 1

(- 1) |^ n = (- 1) to_power n by POWER:41
.= - (1 to_power n) by A2, POWER:48
.= - 1 by POWER:26 ;
then abs ((- 1) |^ n) = - (- 1) by ABSVALUE:def 1;
hence abs ((- 1) |^ n) = 1 ; :: thesis: verum

end;

end;