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 A0:
k > 0
; (abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k))
then A3:
(abs (a + b)) to_power k <= (2 * (max (abs a),(abs b))) to_power k
by Lm003;
A4:
( abs a >= 0 & abs b >= 0 )
by COMPLEX1:132;
then A5:
(max (abs a),(abs b)) to_power k <= ((abs a) to_power k) + ((abs b) to_power k)
by A0, Lm004;
( max (abs a),(abs b) = abs a or max (abs a),(abs b) = abs b )
by XXREAL_0:16;
then A6:
(2 * (max (abs a),(abs b))) to_power k = (2 to_power k) * ((max (abs a),(abs b)) to_power k)
by A0, A4, LmPW003;
2 to_power k > 0
by POWER:39;
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 A5, XREAL_1:66;
hence
(abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k))
by A3, A6, XXREAL_0:2; verum