let a, b, n be Nat; ( n > 1 & b > 0 & a > b implies ((a |^ n) + (b |^ n)) * (a - b) < (a |^ (n + 1)) - (b |^ (n + 1)) )
assume A1:
( n > 1 & b > 0 & a > b )
; ((a |^ n) + (b |^ n)) * (a - b) < (a |^ (n + 1)) - (b |^ (n + 1))
A2:
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:10;
A3a:
m >= 1
by A3, A1, NAT_1:13;
a |^ m > b |^ m
by A1, A3a, PREPOWER:10;
then A3c:
(a |^ m) - (b |^ m) > (b |^ m) - (b |^ m)
by XREAL_1:9;
((a |^ n) + (b |^ n)) * (a - b) =
(((a |^ (n + 1)) - (b |^ (n + 1))) + (a * (b |^ n))) - (b * (a |^ n))
by A2
.=
(((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)))
;
hence
((a |^ n) + (b |^ n)) * (a - b) < (a |^ (n + 1)) - (b |^ (n + 1))
by A1, A3c, XREAL_1:44; verum