let a, b be Nat; :: thesis: ( a mod 2 = b mod 2 implies (- 1) |^ a = (- 1) |^ b )
assume a mod 2 = b mod 2 ; :: thesis: (- 1) |^ a = (- 1) |^ b
then a,b are_congruent_mod 2 by NAT_D:64;
then A1: 2 divides a - b ;

per cases ( a >= b or a < b ) ;

suppose a >= b ; :: thesis: (- 1) |^ a = (- 1) |^ b

then reconsider l = a - b as Element of NAT by NAT_1:21;
consider n being Nat such that
A2: l = 2 * n by A1, NAT_D:def 3;
(- 1) |^ a = (- 1) |^ (b + (2 * n)) by A2
.= ((- 1) |^ b) * ((- 1) |^ (2 * n)) by NEWTON:8
.= ((- 1) |^ b) * (((- 1) |^ 2) |^ n) by NEWTON:9
.= ((- 1) |^ b) * ((1 |^ 2) |^ n) by WSIERP_1:1
.= ((- 1) |^ b) * 1 ;
hence (- 1) |^ a = (- 1) |^ b ; :: thesis: verum

end;

suppose a < b ; :: thesis: (- 1) |^ a = (- 1) |^ b

then reconsider l = b - a as Element of NAT by NAT_1:21;
2 divides - (a - b) by A1, INT_2:10;
then consider n being Nat such that
A3: l = 2 * n by NAT_D:def 3;
(- 1) |^ b = (- 1) |^ (a + (2 * n)) by A3
.= ((- 1) |^ a) * ((- 1) |^ (2 * n)) by NEWTON:8
.= ((- 1) |^ a) * (((- 1) |^ 2) |^ n) by NEWTON:9
.= ((- 1) |^ a) * ((1 |^ 2) |^ n) by WSIERP_1:1
.= ((- 1) |^ a) * 1 ;
hence (- 1) |^ a = (- 1) |^ b ; :: thesis: verum

end;

end;