let a be negative Real; :: thesis: for b being positive Real holds ((a / b) + (b / a)) / 2 <= - 1
let b be positive Real; :: thesis: ((a / b) + (b / a)) / 2 <= - 1
A1: ( (a * a) / (a * b) = a / b & (b * b) / (a * b) = b / a ) by XCMPLX_1:91;
not (a + b) * (a + b) is negative ;
then (((a * a) + ((2 * a) * b)) + (b * b)) - ((2 * a) * b) >= 0 - ((2 * a) * b) by XREAL_1:6;
then ((a * a) + (b * b)) / ((2 * a) * b) <= (- ((2 * a) * b)) / ((2 * a) * b) by XREAL_1:73;
then ((a * a) + (b * b)) / ((2 * a) * b) <= - (((2 * a) * b) / ((2 * a) * b)) ;
then ((a * a) + (b * b)) / (2 * (a * b)) <= - 1 by XCMPLX_1:60;
then (((a * a) + (b * b)) / (a * b)) / 2 <= - 1 by XCMPLX_1:78;
hence ((a / b) + (b / a)) / 2 <= - 1 by A1; :: thesis: verum