let n be Element of NAT ; :: thesis: for th, th1, th2, th3 being real number holds
( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
let th, th1, th2, th3 be real number ; :: thesis: ( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ (2 * n) = (th |^ n) |^ 2 by NEWTON:9; :: thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A1: (- 1) |^ (2 * n) = 1 |^ (2 * n) by POWER:1
.= 1 by NEWTON:10 ; :: thesis: (- 1) |^ ((2 * n) + 1) = - 1
thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:6
.= - 1 by A1 ; :: thesis: verum