let n be natural odd number ; :: thesis: (- 1) |^ n = - 1
defpred S1[ Nat] means ( $1 is odd implies (- 1) |^ $1 = - 1 );
A1: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[b1] )
assume A2: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[b1]
per cases ( k is even or k is odd ) ;
suppose A3: k is odd ; :: thesis: S1[b1]
now :: thesis: ( ( k = 0 & S1[k] ) or ( k = 1 & S1[k] ) or ( k >= 2 & S1[k] ) )
per cases ( k = 0 or k = 1 or k >= 2 ) by NAT_1:23;
case k >= 2 ; :: thesis: S1[k]
then k - 2 in NAT by INT_1:5;
then reconsider k2 = k - 2 as Nat ;
A4: k2 + 2 = k ;
then A5: k2 is odd by A3;
(- 1) |^ k = (- 1) |^ (k2 + 2)
.= ((- 1) |^ k2) * ((- 1) |^ 2) by NEWTON:8
.= (- 1) * ((- 1) |^ (1 + 1)) by A2, A5, A4, NAT_1:16
.= ((- 1) * ((- 1) |^ 1)) * (- 1) by NEWTON:6
.= ((- 1) * (- 1)) * (- 1) ;
hence S1[k] ; :: thesis: verum
end;
end;
end;
hence S1[k] ; :: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 4(A1);
 hence (- 1) |^ n = - 1 ; :: thesis: verum