let a, b, c, n be positive Real; :: thesis: for m being non negative Real st (a to_power m) + (b to_power m) <= c to_power m holds
(a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n)
let m be non negative Real; :: thesis: ( (a to_power m) + (b to_power m) <= c to_power m implies (a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n) )
assume A1: (a to_power m) + (b to_power m) <= c to_power m ; :: thesis: (a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n)
reconsider x = a / c as positive Real ;
reconsider y = b / c as positive Real ;
A2: ( x * c = a & y * c = b ) by XCMPLX_1:87;
A3: ( (x * c) to_power m = (x to_power m) * (c to_power m) & (y * c) to_power m = (y to_power m) * (c to_power m) & (x * c) to_power (m + n) = (x to_power (m + n)) * (c to_power (m + n)) & (y * c) to_power (m + n) = (y to_power (m + n)) * (c to_power (m + n)) ) by POWER:30;
then (c to_power m) * ((x to_power m) + (y to_power m)) <= (c to_power m) * 1 by A1, A2;
then (x to_power m) + (y to_power m) <= 1 by XREAL_1:68;
then (x to_power (m + n)) + (y to_power (m + n)) < 1 by Pow;
then (c to_power (m + n)) * ((x to_power (m + n)) + (y to_power (m + n))) < (c to_power (m + n)) * 1 by XREAL_1:68;
hence (a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n) by A2, A3; :: thesis: verum