let a, b, k be Real; ( k > 0 implies (abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k)) )
assume A1:
k > 0
; (abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k))
then A2:
(abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k
by Th16;
A3:
( abs a >= 0 & abs b >= 0 )
by COMPLEX1:46;
then A4:
(max ((abs a),(abs b))) to_power k <= ((abs a) to_power k) + ((abs b) to_power k)
by A1, Th17;
( max ((abs a),(abs b)) = abs a or max ((abs a),(abs b)) = abs b )
by XXREAL_0:16;
then A5:
(2 * (max ((abs a),(abs b)))) to_power k = (2 to_power k) * ((max ((abs a),(abs b))) to_power k)
by A1, A3, Th5;
2 to_power k > 0
by POWER:34;
then
(2 to_power k) * ((max ((abs a),(abs b))) to_power k) <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k))
by A4, XREAL_1:64;
hence
(abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k))
by A2, A5, XXREAL_0:2; verum