let n, m be natural number ; :: thesis: for r being real number st not m is even & n >= m & r < 0 & r > - 1 holds
r to_power n >= r to_power m
let r be real number ; :: thesis: ( not m is even & n >= m & r < 0 & r > - 1 implies r to_power n >= r to_power m )
assume A0: not m is even ; :: thesis: ( not n >= m or not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A1: n >= m ; :: thesis: ( not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A2: ( r < 0 & r > - 1 ) ; :: thesis: r to_power n >= r to_power m
zz: n + 1 > m + 0 by A1, XREAL_1:10;

per cases ( n = m or n > m ) by zz, NAT_1:22;

suppose n = m ; :: thesis: r to_power n >= r to_power m

hence r to_power n >= r to_power m ; :: thesis: verum

end;

suppose D2: n > m ; :: thesis: r to_power n >= r to_power m

then reconsider t = n - m as natural number by NAT_1:21;
C2: (r to_power n) - (r to_power m) = (r to_power (t + m)) - (r to_power m)
.= ((r to_power t) * (r to_power m)) - (1 * (r to_power m)) by JakPower32, A2
.= ((r to_power t) - 1) * (r to_power m) ;
C3: r to_power m <= 0 by pom2, A2, A0;
D1: t <> 0 by D2;
X: abs r <= 1 by A2, ABSVALUE:12;
abs r <> 1

proof

assume abs r = 1 ; :: thesis: contradiction
then abs r = abs 1 ;
hence contradiction by A2, ABSVALUE:45; :: thesis: verum

end;

then H3: abs r < 1 by X, XXREAL_0:1;
( abs r > 0 & t > 0 ) by D1, A2;
then (abs r) to_power t < 1 to_power t by H3, POWER:42;
then (abs r) to_power t < 1 by POWER:31;
then ( abs (r to_power t) < 1 & r to_power t <= abs (r to_power t) ) by ABSVALUE:11, SERIES_1:2;
then r to_power t < 1 by XXREAL_0:2;
then (r to_power t) - 1 <= 1 - 1 by XREAL_1:11;
then ((r to_power n) - (r to_power m)) + (r to_power m) >= 0 + (r to_power m) by C2, C3, XREAL_1:8;
hence r to_power n >= r to_power m ; :: thesis: verum

end;

end;