let x be Real; :: thesis: for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
let a be Nat; :: thesis: ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
A1: (- x) |^ (2 * a) = ((- x) |^ 2) |^ a by NEWTON:9
.= (x |^ 2) |^ a by Th1
.= x |^ (2 * a) by NEWTON:9 ;
(- x) |^ ((2 * a) + 1) = ((- x) |^ (2 * a)) * (- x) by NEWTON:6
.= - ((x |^ (2 * a)) * x) by A1
.= - (x |^ ((2 * a) + 1)) by NEWTON:6 ;
hence ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) by A1; :: thesis: verum