let a, b, c be real positive number ; :: thesis: 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: (((b * c) / a) ^2 ) + (((a * b) / c) ^2 ) >= 2 * (b ^2 ) by Lm13;
(((c * a) / b) ^2 ) + (((a * b) / c) ^2 ) >= 2 * (a ^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:9;
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:9;
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:74;
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:8;
then A3: ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 >= 3 * (((a ^2 ) + (b ^2 )) + (c ^2 )) by Lm16;
sqrt (((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 ) >= sqrt (3 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) by A3, SQUARE_1:94;
hence sqrt (3 * (((a ^2 ) + (b ^2 )) + (c ^2 ))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c) by SQUARE_1:89; :: thesis: verum