let a be Real; :: thesis: for n being Nat st n is odd holds
(- a) |^ n = - (a |^ n)
let n be Nat; :: thesis: ( n is odd implies (- a) |^ n = - (a |^ n) )
assume n is odd ; :: thesis: (- a) |^ n = - (a |^ n)
then consider m being 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