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