let a, b be positive Real; :: thesis: for n, m being positive Real holds (a to_power (n + m)) + (b to_power (n + m)) >= (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2
let n, m be positive Real; :: thesis: (a to_power (n + m)) + (b to_power (n + m)) >= (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2
((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0

proof

per cases ( a = b or a > b or a < b ) by XXREAL_0:1;

suppose a = b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0

hence ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0 ; :: thesis: verum

end;

suppose a > b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0

then ( a to_power n > b to_power n & a to_power m > b to_power m ) by POWER:37;
then ( (a to_power n) - (b to_power n) > (b to_power n) - (b to_power n) & (a to_power m) - (b to_power m) > (b to_power m) - (b to_power m) ) by XREAL_1:9;
hence ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0 ; :: thesis: verum

end;

suppose a < b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0

then ( a to_power n < b to_power n & a to_power m < b to_power m ) by POWER:37;
then ( (a to_power n) - (b to_power n) < (b to_power n) - (b to_power n) & (a to_power m) - (b to_power m) < (b to_power m) - (b to_power m) ) by XREAL_1:9;
hence ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) >= 0 ; :: thesis: verum

end;

end;

end;

then (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m))) >= (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + 0 by XREAL_1:6;
then ((((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)))) / 2 >= (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) / 2 by XREAL_1:72;
hence (a to_power (n + m)) + (b to_power (n + m)) >= (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2 by N158; :: thesis: verum