let a, b, c be positive Real; :: thesis: (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c
A1: ((a * c) / b) + ((a * b) / c) = (a * (c / b)) + ((a * b) / c) by XCMPLX_1:74
.= (a * (c / b)) + (a * (b / c)) by XCMPLX_1:74
.= a * ((c / b) + (b / c)) ;
A2: ((a * b) / c) + ((b * c) / a) = (b * (a / c)) + ((b * c) / a) by XCMPLX_1:74
.= (b * (a / c)) + (b * (c / a)) by XCMPLX_1:74
.= b * ((a / c) + (c / a)) ;
A3: b * ((a / c) + (c / a)) >= b * 2 by SERIES_3:3, XREAL_1:64;
A4: c * ((b / a) + (a / b)) >= c * 2 by SERIES_3:3, XREAL_1:64;
a * ((c / b) + (b / c)) >= a * 2 by SERIES_3:3, XREAL_1:64;
then (a * ((c / b) + (b / c))) + (b * ((a / c) + (c / a))) >= (a * 2) + (b * 2) by A3, XREAL_1:7;
then A5: ((a * ((c / b) + (b / c))) + (b * ((a / c) + (c / a)))) + (c * ((b / a) + (a / b))) >= ((a * 2) + (b * 2)) + (c * 2) by A4, XREAL_1:7;
((b * c) / a) + ((a * c) / b) = (c * (b / a)) + ((a * c) / b) by XCMPLX_1:74
.= (c * (b / a)) + (c * (a / b)) by XCMPLX_1:74
.= c * ((b / a) + (a / b)) ;
then (2 * ((((b * c) / a) + ((a * c) / b)) + ((a * b) / c))) / 2 >= (2 * ((a + b) + c)) / 2 by A1, A2, A5, XREAL_1:72;
hence (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c ; :: thesis: verum