let n, m be Nat; 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; ( m is odd & n >= m & r < 0 & r > - 1 implies r to_power n >= r to_power m )
assume A1:
m is odd
; ( not n >= m or not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A2:
n >= m
; ( not r < 0 or not r > - 1 or r to_power n >= r to_power m )
assume A3:
( r < 0 & r > - 1 )
; 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 A5:
n > m
;
r to_power n >= r to_power mthen 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
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
;
verum end; end;