let m be non zero Real; :: thesis: for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
let n be Integer; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
per cases ( n is odd or n is even ) ;
suppose A1: n is odd ; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
then (- m) to_power n = - (m to_power n) by POWER:48
.= (- 1) * (m to_power n)
.= ((- 1) to_power n) * (m to_power n) by A1, Th2 ;
hence ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; :: thesis: verum
end;
suppose A2: n is even ; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
then (- m) to_power n = 1 * (m to_power n) by POWER:47
.= ((- 1) to_power n) * (m to_power n) by A2, Th3 ;
hence ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; :: thesis: verum
end;
end;