let a be real number ; :: thesis: for k being Integer st a <> 0 & ex l being Integer st k = 2 * l holds
(- a) to_power k = a to_power k
let k be Integer; :: thesis: ( a <> 0 & ex l being Integer st k = 2 * l implies (- a) to_power k = a to_power k )
assume A1: a <> 0 ; :: thesis: ( for l being Integer holds not k = 2 * l or (- a) to_power k = a to_power k )
given l being Integer such that A2: k = 2 * l ; :: thesis: (- a) to_power k = a to_power k
reconsider l1 = 2 as Integer ;

now

per cases ( a > 0 or a < 0 ) by A1;

suppose A3: a > 0 ; :: thesis: a to_power k = (- a) to_power k

thus a to_power k = (a to_power 2) to_power l by A2, A3, Th38
.= (a ^2 ) to_power l by Th53
.= ((- a) ^2 ) to_power l
.= ((- a) to_power 2) to_power l by Th53
.= ((- a) #Z l1) to_power l by Def2
.= ((- a) #Z l1) #Z l by Def2
.= (- a) #Z (l1 * l) by PREPOWER:55
.= (- a) to_power k by A2, Def2 ; :: thesis: verum

end;

suppose a < 0 ; :: thesis: (- a) to_power k = a to_power k

then - a > 0 by XREAL_1:60;
hence (- a) to_power k = ((- a) to_power 2) to_power l by A2, Th38
.= ((- a) ^2 ) to_power l by Th53
.= (a ^2 ) to_power l
.= (a to_power 2) to_power l by Th53
.= (a #Z l1) to_power l by Def2
.= (a #Z l1) #Z l by Def2
.= a #Z (l1 * l) by PREPOWER:55
.= a to_power k by A2, Def2 ;
:: thesis: verum

end;

end;

end;

hence (- a) to_power k = a to_power k ; :: thesis: verum