let a, b, k be Real; :: thesis: ( k > 0 implies ( |.(a + b).| to_power k <= (|.a.| + |.b.|) to_power k & (|.a.| + |.b.|) to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k & |.(a + b).| to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k ) )
assume A1: k > 0 ; :: thesis: ( |.(a + b).| to_power k <= (|.a.| + |.b.|) to_power k & (|.a.| + |.b.|) to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k & |.(a + b).| to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k )
A2: |.(a + b).| <= |.a.| + |.b.| by ABSVALUE:9;
( |.a.| <= max (|.a.|,|.b.|) & |.b.| <= max (|.a.|,|.b.|) ) by XXREAL_0:25;
then A3: |.a.| + |.b.| <= (max (|.a.|,|.b.|)) + (max (|.a.|,|.b.|)) by XREAL_1:7;
then A4: |.(a + b).| <= 2 * (max (|.a.|,|.b.|)) by A2, XXREAL_0:2;
0 <= |.(a + b).| by COMPLEX1:46;
hence ( |.(a + b).| to_power k <= (|.a.| + |.b.|) to_power k & (|.a.| + |.b.|) to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k & |.(a + b).| to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k ) by A1, A2, A3, A4, HOLDER_1:3; :: thesis: verum