let n be Nat; :: thesis: for th, th1, th2, th3 being Real holds
( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
let th, th1, th2, th3 be Real; :: thesis: ( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
reconsider 2n = 2 * n as Element of NAT by ORDINAL1:def 12;
thus th |^ (2 * n) = (th |^ n) |^ 2 by NEWTON:9; :: thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
(- 1) |^ 2n = 1 |^ 2n by POWER:1
.= 1 ;
hence A1: (- 1) |^ (2 * n) = 1 ; :: thesis: (- 1) |^ ((2 * n) + 1) = - 1
thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:6
.= - 1 by A1 ; :: thesis: verum