let a, b, c be positive Real; ( a >= 1 implies (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) )
A1:
(b + c) / 2 >= (2 * (sqrt (b * c))) / 2
by SIN_COS2:1, XREAL_1:72;
set p = a to_power c;
set o = a to_power b;
( a to_power b > 0 & a to_power c > 0 )
by POWER:34;
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 + c) > 0 & (a to_power b) + (a to_power c) >= 2 * (sqrt (a to_power (b + c))) )
by POWER:27, POWER:34;
then
(a to_power b) + (a to_power c) >= 2 * ((a to_power (b + c)) to_power (1 / 2))
by ASYMPT_1:83;
then A2:
(a to_power b) + (a to_power c) >= 2 * (a to_power ((1 / 2) * (b + c)))
by POWER:33;
assume
a >= 1
; (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))
then
a #R ((b + c) / 2) >= a #R (sqrt (b * c))
by A1, PREPOWER:82;
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:64;
hence
(a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))
by A2, XXREAL_0:2; verum