let a, b, m be Nat; :: thesis: (a - b) * ((a |^ m) - (b |^ m)) >= 0
A0: ( a |^ 0 = 1 & b |^ 0 = 1 ) by NEWTON:4;
per cases ( (a |^ m) - (b |^ m) >= 0 or (a |^ m) - (b |^ m) < 0 ) ;
suppose A1: (a |^ m) - (b |^ m) >= 0 ; :: thesis: (a - b) * ((a |^ m) - (b |^ m)) >= 0
then ((a |^ m) - (b |^ m)) + (b |^ m) >= 0 + (b |^ m) by XREAL_1:7;
then ( a >= b or m < 1 ) by PREPOWER:10;
then ( a - b >= b - b or m = 0 ) by XREAL_1:9, NAT_1:14;
hence (a - b) * ((a |^ m) - (b |^ m)) >= 0 by A0, A1; :: thesis: verum
end;
suppose A2: (a |^ m) - (b |^ m) < 0 ; :: thesis: (a - b) * ((a |^ m) - (b |^ m)) >= 0
then ((a |^ m) - (b |^ m)) + (b |^ m) < 0 + (b |^ m) by XREAL_1:8;
then a - b < b - b by Lm3a, XREAL_1:9;
hence (a - b) * ((a |^ m) - (b |^ m)) >= 0 by A2; :: thesis: verum
end;
end;