let a, b, c, d be positive Real; :: thesis: ( a + b = c + d & a * b = c * d implies max (a,b) = max (c,d) )
assume A1: ( a + b = c + d & a * b = c * d ) ; :: thesis: max (a,b) = max (c,d)
reconsider x = max (a,b) as positive Real ;
reconsider y = min (a,b) as positive Real ;
reconsider z = max (c,d) as positive Real ;
reconsider t = min (c,d) as positive Real ;
( ( ( 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;
then x * ((z + t) - x) = z * ((x + y) - z) by A1;
then A3: x * (x - t) = z * (z - y) ;
A4: x - z = t - y by A1, SAD;
then ( x - t = 0 or x = z ) by A3, XCMPLX_1:5;
per cases then ( x = z or x = t ) ;
suppose x = z ; :: thesis: max (a,b) = max (c,d)
hence max (a,b) = max (c,d) ; :: thesis: verum
end;
suppose B1: x = t ; :: thesis: max (a,b) = max (c,d)
( x >= a & a >= y & z >= c & c >= t ) by XXREAL_0:17, XXREAL_0:25;
then ( x >= y & z >= t ) by XXREAL_0:2;
hence max (a,b) = max (c,d) by B1, A4, XXREAL_0:1; :: thesis: verum
end;
end;