let a, b, c, d be positive Real; :: thesis: for n being Real st a + b = c + d & a * b = c * d holds
(a to_power n) + (b to_power n) = (c to_power n) + (d to_power n)
let n be Real; :: thesis: ( a + b = c + d & a * b = c * d implies (a to_power n) + (b to_power n) = (c to_power n) + (d to_power n) )
assume A1: ( a + b = c + d & a * b = c * d ) ; :: thesis: (a to_power n) + (b to_power n) = (c to_power n) + (d to_power n)
A2: max (a,b) = max (c,d) by A1, ISM;
( ( ( max (a,b) = a & min (a,b) = b ) or ( max (a,b) = b & min (a,b) = a ) ) & ( ( max (c,d) = c & min (c,d) = d ) or ( max (c,d) = d & min (c,d) = c ) ) ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (a to_power n) + (b to_power n) = (c to_power n) + (d to_power n) by A1, A2; :: thesis: verum