let a, b, k be Real; ( k > 0 implies ( (abs (a + b)) to_power k <= ((abs a) + (abs b)) to_power k & ((abs a) + (abs b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k & (abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k ) )
assume A0:
k > 0
; ( (abs (a + b)) to_power k <= ((abs a) + (abs b)) to_power k & ((abs a) + (abs b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k & (abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k )
A3:
abs (a + b) <= (abs a) + (abs b)
by ABSVALUE:21;
( abs a <= max ((abs a),(abs b)) & abs b <= max ((abs a),(abs b)) )
by XXREAL_0:25;
then A5:
(abs a) + (abs b) <= (max ((abs a),(abs b))) + (max ((abs a),(abs b)))
by XREAL_1:9;
then A6:
abs (a + b) <= 2 * (max ((abs a),(abs b)))
by A3, XXREAL_0:2;
0 <= abs (a + b)
by COMPLEX1:132;
hence
( (abs (a + b)) to_power k <= ((abs a) + (abs b)) to_power k & ((abs a) + (abs b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k & (abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k )
by A0, A3, A5, A6, HOLDER_1:3; verum