let a, b, c be positive Real; sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c)
A1:
(((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2)
by Lm13;
A2:
(((c * a) / b) ^2) + (((a * b) / c) ^2) >= 2 * (a ^2)
by Lm13;
(((b * c) / a) ^2) + (((a * b) / c) ^2) >= 2 * (b ^2)
by Lm13;
then
((((c * a) / b) ^2) + (((a * b) / c) ^2)) + ((((b * c) / a) ^2) + (((a * b) / c) ^2)) >= (2 * (a ^2)) + (2 * (b ^2))
by A2, XREAL_1:7;
then
((((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (((a * b) / c) ^2)) + ((((b * c) / a) ^2) + (((c * a) / b) ^2)) >= ((2 * (a ^2)) + (2 * (b ^2))) + (2 * (c ^2))
by A1, XREAL_1:7;
then
((((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) * 2) / 2 >= ((((a ^2) + (b ^2)) + (c ^2)) * 2) / 2
by XREAL_1:72;
then
(((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) >= (((a ^2) + (b ^2)) + (c ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2)))
by XREAL_1:6;
then
((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 >= 3 * (((a ^2) + (b ^2)) + (c ^2))
by Lm16;
then
sqrt (((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2) >= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2)))
by SQUARE_1:26;
hence
sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c)
by SQUARE_1:22; verum