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

A5: - a <> - 0 by A3;
a to_power k = (a to_power (2 * l)) * (a to_power 1) by A2, A3, Th32
.= (a to_power (2 * l)) * a by Th30
.= ((- a) to_power (2 * l)) * a by A1, Th54
.= - (((- a) to_power (2 * l)) * (- a))
.= - (((- a) #Z (2 * l)) * (- a)) by Def2
.= - (((- a) #Z (2 * l)) * ((- a) #Z l1)) by PREPOWER:45
.= - ((- a) #Z k) by A2, A5, PREPOWER:54
.= - ((- a) to_power k) by Def2 ;
hence (- a) to_power k = - (a to_power k) ; :: thesis: verum

end;

suppose A6: 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 * l)) * ((- a) to_power 1) by A2, Th32
.= ((- a) to_power (2 * l)) * (- a) by Th30
.= (a to_power (2 * l)) * (- a) by A1, Th54
.= - ((a to_power (2 * l)) * a)
.= - ((a #Z (2 * l)) * a) by Def2
.= - ((a #Z (2 * l)) * (a #Z l1)) by PREPOWER:45
.= - (a #Z k) by A2, A6, PREPOWER:54
.= - (a to_power k) by Def2 ;
:: thesis: verum

end;

end;

end;

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