let a, b be positive Real; ( a + b = 1 implies (a |^ 3) + (b |^ 3) < 1 )
assume A1:
a + b = 1
; (a |^ 3) + (b |^ 3) < 1
A2:
1 + ((a * b) * (- 3)) < 0 + 1
by XREAL_1:8;
(a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2))
by Lm6;
then (a |^ 3) + (b |^ 3) =
(((a ^2) + ((2 * a) * b)) + (b ^2)) - ((3 * a) * b)
by A1
.=
(1 ^2) - (3 * (a * b))
by A1, SQUARE_1:4
;
hence
(a |^ 3) + (b |^ 3) < 1
by A2; verum