let a, b, c be real positive number ; :: thesis: ( a >= 1 implies (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) )
assume A1: a >= 1 ; :: thesis: (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))
A2: (b + c) / 2 >= (2 * (sqrt (b * c))) / 2 by SIN_COS2:1, XREAL_1:74;
set o = a to_power b;
set p = a to_power c;
A3: a to_power (b + c) > 0 by POWER:39;
( a to_power b > 0 & a to_power c > 0 ) by POWER:39;
then (a to_power b) + (a to_power c) >= 2 * (sqrt ((a to_power b) * (a to_power c))) by SIN_COS2:1;
then (a to_power b) + (a to_power c) >= 2 * (sqrt (a to_power (b + c))) by POWER:32;
then (a to_power b) + (a to_power c) >= 2 * ((a to_power (b + c)) to_power (1 / 2)) by A3, ASYMPT_1:89;
then A4: (a to_power b) + (a to_power c) >= 2 * (a to_power ((1 / 2) * (b + c))) by POWER:38;
a #R ((b + c) / 2) >= a #R (sqrt (b * c)) by A1, A2, PREPOWER:96;
then a to_power ((b + c) / 2) >= a #R (sqrt (b * c)) by POWER:def 2;
then a to_power ((b + c) / 2) >= a to_power (sqrt (b * c)) by POWER:def 2;
then 2 * (a to_power ((b + c) / 2)) >= 2 * (a to_power (sqrt (b * c))) by XREAL_1:66;
hence (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) by A4, XXREAL_0:2; :: thesis: verum