let a, b, n be Nat; :: thesis: ( n > 0 & a > b implies ((a |^ n) + (b |^ n)) * (a - b) <= (a |^ (n + 1)) - (b |^ (n + 1)) )
assume A1: ( n > 0 & a > b ) ; :: thesis: ((a |^ n) + (b |^ n)) * (a - b) <= (a |^ (n + 1)) - (b |^ (n + 1))
then A2: for m being Nat holds 0 <= (a |^ m) - (b |^ m) by Lm3a, XREAL_1:48;
A2b: for m being Nat holds
( a |^ (n + 1) = a * (a |^ n) & b |^ (n + 1) = b * (b |^ n) & a |^ (m + 1) = a * (a |^ m) & b |^ (m + 1) = b * (b |^ m) ) by NEWTON:6;
consider m being Nat such that
A3: n = 1 + m by A1, NAT_1:14, NAT_1:10;
A4: ((a |^ n) + (b |^ n)) * (a - b) = (((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ n))) - (b * (a |^ n)) by A2b
.= (((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ (m + 1)))) - (b * (a * (a |^ m))) by NEWTON:6, A3
.= (((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b * (b |^ m)))) - (b * (a * (a |^ m))) by NEWTON:6
.= ((a |^ (n + 1)) - (b |^ (n + 1))) - ((a * b) * ((a |^ m) - (b |^ m))) ;
(a |^ m) - (b |^ m) in NAT by A2, INT_1:3;
hence ((a |^ n) + (b |^ n)) * (a - b) <= (a |^ (n + 1)) - (b |^ (n + 1)) by A4, XREAL_1:43; :: thesis: verum