let a, b be positive Real; :: thesis: for m being non positive Real
for n being negative 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 positive Real; :: thesis: for n being negative 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 negative Real; :: thesis: ( (a to_power m) + (b to_power m) <= 1 implies (a to_power (m + n)) + (b to_power (m + n)) < 1 )
reconsider k = a to_power (- 1) as positive Real ;
reconsider l = b to_power (- 1) as positive Real ;
( k to_power (- m) = a to_power ((- 1) * (- m)) & k to_power ((- m) - n) = a to_power ((- 1) * ((- m) - n)) & l to_power (- m) = b to_power ((- 1) * (- m)) & l to_power ((- m) - n) = b to_power ((- 1) * ((- m) - n)) ) by POWER:33;
hence ( (a to_power m) + (b to_power m) <= 1 implies (a to_power (m + n)) + (b to_power (m + n)) < 1 ) by Pow; :: thesis: verum