let n be Nat; :: thesis: ( n is odd implies for r, s being negative Real st r <= s holds
r |^ n <= s |^ n )
assume A1: n is odd ; :: thesis: for r, s being negative Real st r <= s holds
r |^ n <= s |^ n
let r, s be negative Real; :: thesis: ( r <= s implies r |^ n <= s |^ n )
assume r <= s ; :: thesis: r |^ n <= s |^ n
then (- 1) * r >= (- 1) * s by XREAL_1:65;
then A2: (- r) |^ n >= (- s) |^ n by NEWTON02:41;
( (- r) |^ n = - (r |^ n) & (- s) |^ n = - (s |^ n) ) by A1, POWER:2;
then (- 1) * (- (r |^ n)) <= (- 1) * (- (s |^ n)) by A2, XREAL_1:65;
hence r |^ n <= s |^ n ; :: thesis: verum