let a, b be positive Real; :: thesis: for m being non negative Real
for n being positive Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1
let m be non negative Real; :: thesis: for n being positive Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1
let n be positive Real; :: thesis: ( (a to_power m) + (b to_power m) <= 1 implies (a to_power (m + n)) + (b to_power (m + n)) < 1 )
assume A1: (a to_power m) + (b to_power m) <= 1 ; :: thesis: (a to_power (m + n)) + (b to_power (m + n)) < 1
( a to_power 0 = 1 & b to_power 0 = 1 ) by POWER:24;
then not m = 0 by A1;
then reconsider m = m as positive Real ;
A2: (a to_power m) + 0 < (a to_power m) + (b to_power m) by XREAL_1:6;
( ( a > 1 implies a to_power m >= 1 ) & ( a = 1 implies a to_power m = 1 ) ) by POWER:35;
then ( a >= 1 implies a to_power m >= 1 ) by XXREAL_0:1;
then reconsider a = a as positive light Real by A1, A2, TA1, XXREAL_0:2;
A3: (b to_power m) + 0 < (b to_power m) + (a to_power m) by XREAL_1:6;
( ( b > 1 implies b to_power m >= 1 ) & ( b = 1 implies b to_power m = 1 ) ) by POWER:35;
then ( b >= 1 implies b to_power m >= 1 ) by XXREAL_0:1;
then reconsider b = b as positive light Real by A1, A3, TA1, XXREAL_0:2;
( 0 < a & a < 1 & 0 < b & b < 1 & m + 0 < m + n ) by TA1, XREAL_1:6;
then ( a to_power m > a to_power (m + n) & b to_power m > b to_power (m + n) ) by POWER:40;
then (a to_power (m + n)) + (b to_power (m + n)) < (a to_power m) + (b to_power m) by XREAL_1:8;
hence (a to_power (m + n)) + (b to_power (m + n)) < 1 by A1, XXREAL_0:2; :: thesis: verum