let n, m be Nat; :: thesis: for r being Real st m is odd & n >= m & r < 0 & r > - 1 holds
r to_power n >= r to_power m
let r be Real; :: thesis: ( m is odd & n >= m & r < 0 & r > - 1 implies r to_power n >= r to_power m )
assume A1: m is odd ; :: thesis: ( not n >= m or not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A2: n >= m ; :: thesis: ( not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A3: ( r < 0 & r > - 1 ) ; :: thesis: r to_power n >= r to_power m
A4: n + 1 > m + 0 by A2, XREAL_1:8;

per cases ( n = m or n > m ) by A4, 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 A5: n > m ; :: thesis: r to_power n >= r to_power m

then reconsider t = n - m as Nat by NAT_1:21;
A6: (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 Th2, A3
.= ((r to_power t) - 1) * (r to_power m) ;
A7: r to_power m <= 0 by Th7, A3, A1;
A8: t <> 0 by A5;
A9: |.r.| <= 1 by A3, ABSVALUE:5;
|.r.| <> 1

proof

assume |.r.| = 1 ; :: thesis: contradiction
then |.r.| = |.1.| ;
hence contradiction by A3, ABSVALUE:28; :: thesis: verum

end;

then A10: |.r.| < 1 by A9, XXREAL_0:1;
( |.r.| > 0 & t > 0 ) by A8, A3;
then |.r.| to_power t < 1 to_power t by A10, POWER:37;
then |.r.| to_power t < 1 ;
then ( |.(r to_power t).| < 1 & r to_power t <= |.(r to_power t).| ) by ABSVALUE:4, SERIES_1:2;
then r to_power t < 1 by XXREAL_0:2;
then (r to_power t) - 1 <= 1 - 1 by XREAL_1:9;
then ((r to_power n) - (r to_power m)) + (r to_power m) >= 0 + (r to_power m) by A6, A7, XREAL_1:6;
hence r to_power n >= r to_power m ; :: thesis: verum

end;

end;