let a, b, c be positive Real; (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c)
A1: 1 =
((a / a) * 1) * 1
by XCMPLX_1:60
.=
((a / a) * (b / b)) * 1
by XCMPLX_1:60
.=
((a / a) * (b / b)) * (c / c)
by XCMPLX_1:60
.=
((a / b) * (b / a)) * (c / c)
.=
(a / b) * ((b / a) * (c / c))
.=
(a / b) * ((b / c) * (c / a))
.=
((a / b) * (b / c)) * (c / a)
;
c / b =
(c / b) * 1
.=
(c / b) * (a / a)
by XCMPLX_1:60
.=
((a / b) * (c / a)) * 1
;
then A2:
c / b <= ((((a / b) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3
by Th13;
a / c =
(a / c) * 1
.=
(a / c) * (b / b)
by XCMPLX_1:60
.=
((a / b) * (b / c)) * 1
;
then A3:
a / c <= ((((a / b) |^ 3) + ((b / c) |^ 3)) + (1 |^ 3)) / 3
by Th13;
b / a =
(b / a) * 1
.=
(b / a) * (c / c)
by XCMPLX_1:60
.=
((b / c) * (c / a)) * 1
;
then
b / a <= ((((b / c) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3
by Th13;
then
(b / a) + (c / b) <= (((((b / c) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3)) + (((((a / b) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3))
by A2, XREAL_1:7;
then A4:
((b / a) + (c / b)) + (a / c) <= ((((((b / c) |^ 3) / 3) + (((a / b) |^ 3) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + (2 / 3)) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (1 / 3))
by A3, XREAL_1:7;
((a / b) * (b / c)) * (c / a) <= ((((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3)) / 3
by Th13;
then
(((b / a) + (c / b)) + (a / c)) + 1 <= (((((2 * ((b / c) |^ 3)) / 3) + ((2 * ((a / b) |^ 3)) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + 1) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (((c / a) |^ 3) / 3))
by A1, A4, XREAL_1:7;
then
((((b / a) + (c / b)) + (a / c)) + 1) - 1 <= (((((b / c) |^ 3) + ((a / b) |^ 3)) + ((c / a) |^ 3)) + 1) - 1
by XREAL_1:9;
hence
(((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c)
; verum