let a be real number ; :: thesis: for n being Element of NAT st ex m being Element of NAT st n = (2 * m) + 1 holds
(- a) |^ n = - (a |^ n)
let n be Element of NAT ; :: thesis: ( ex m being Element of NAT st n = (2 * m) + 1 implies (- a) |^ n = - (a |^ n) )
given m being Element of NAT such that A1: n = (2 * m) + 1 ; :: thesis: (- a) |^ n = - (a |^ n)
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