let a, b, k be Real; :: thesis: ( a >= 0 & b >= 0 & k > 0 implies (max (a,b)) to_power k <= (a to_power k) + (b to_power k) )
assume A1: ( a >= 0 & b >= 0 & k > 0 ) ; :: thesis: (max (a,b)) to_power k <= (a to_power k) + (b to_power k)
per cases ( ( a <> 0 & b <> 0 ) or a = 0 or b = 0 ) ;
suppose ( a <> 0 & b <> 0 ) ; :: thesis: (max (a,b)) to_power k <= (a to_power k) + (b to_power k)
then A2: ( a to_power k >= 0 & b to_power k >= 0 ) by ;
( max (a,b) = a or max (a,b) = b ) by XXREAL_0:def 10;
hence (max (a,b)) to_power k <= (a to_power k) + (b to_power k) by ; :: thesis: verum
end;
suppose A3: a = 0 ; :: thesis: (max (a,b)) to_power k <= (a to_power k) + (b to_power k)
then a to_power k = 0 by ;
hence (max (a,b)) to_power k <= (a to_power k) + (b to_power k) by ; :: thesis: verum
end;
suppose A4: b = 0 ; :: thesis: (max (a,b)) to_power k <= (a to_power k) + (b to_power k)
then b to_power k = 0 by ;
hence (max (a,b)) to_power k <= (a to_power k) + (b to_power k) by ; :: thesis: verum
end;
end;