let a be real number ; :: thesis: for n being Element of NAT st n is odd holds
(- a) |^ n = - (a |^ n)
let n be Element of NAT ; :: thesis: ( n is odd implies (- a) |^ n = - (a |^ n) )
assume n is odd ; :: 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:6
.= (a |^ (2 * m)) * (- a) by Th1
.= - ((a |^ (2 * m)) * a)
.= - (a |^ n) by A1, NEWTON:6 ; :: thesis: verum