let x be real number ; :: 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:14
.= (x |^ 2) |^ a by Th2
.= x |^ (2 * a) by NEWTON:14 ;
(- x) |^ ((2 * a) + 1) = ((- x) |^ (2 * a)) * (- x) by NEWTON:11
.= - ((x |^ (2 * a)) * x) by A1
.= - (x |^ ((2 * a) + 1)) by NEWTON:11 ;
hence ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) by A1; :: thesis: verum