let a be real number ; :: thesis: for n being Element of NAT st not n is even holds
(- a) |^ n = - (a |^ n)
let n be Element of NAT ; :: thesis: ( not n is even implies (- a) |^ n = - (a |^ n) )
assume not n is even ; :: thesis: (- a) |^ n = - (a |^ n)
then consider m being Element of NAT such that
A1: n = (2 * m) + 1 by ABIAN:9;
thus (- a) |^ n = ((- a) |^ (2 * m)) * (- a) by A1, NEWTON:11
.= (a |^ (2 * m)) * (- a) by Th1
.= - ((a |^ (2 * m)) * a)
.= - (a |^ n) by A1, NEWTON:11 ; :: thesis: verum