let a, b, k be Real; :: thesis: ( 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 A1: k > 0 ; :: thesis: ( (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 )
A2: abs (a + b) <= (abs a) + (abs b) by ABSVALUE:9;
( abs a <= max ((abs a),(abs b)) & abs b <= max ((abs a),(abs b)) ) by XXREAL_0:25;
then A3: (abs a) + (abs b) <= (max ((abs a),(abs b))) + (max ((abs a),(abs b))) by XREAL_1:7;
then A4: abs (a + b) <= 2 * (max ((abs a),(abs b))) by A2, XXREAL_0:2;
0 <= abs (a + b) by COMPLEX1:46;
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 A1, A2, A3, A4, HOLDER_1:3; :: thesis: verum