let x, y be ExtReal; :: thesis: ( x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies max (x,y) = ((x + y) + |.(x - y).|) / 2 )
assume that
A1: x <> -infty and
A2: y <> -infty and
A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2
per cases ;
suppose A4: x = +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2
then ( x + y = +infty & x - y = +infty ) by ;
then A5: (x + y) + |.(x - y).| = +infty by XXREAL_3:def 2;
A6: max (x,y) = +infty by ;
thus max (x,y) = ((x + y) + |.(x - y).|) / 2 by ; :: thesis: verum
end;
suppose x <> +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2
then reconsider a = x as Element of REAL by ;
per cases ;
suppose A7: y = +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2
then ( x + y = +infty & x - y = -infty ) by ;
then A8: (x + y) + |.(x - y).| = +infty by XXREAL_3:def 2;
A9: max (x,y) = +infty by ;
thus max (x,y) = ((x + y) + |.(x - y).|) / 2 by ; :: thesis: verum
end;
suppose y <> +infty ; :: thesis: max (x,y) = ((x + y) + |.(x - y).|) / 2
then reconsider b = y as Element of REAL by ;
x - y = a - b by SUPINF_2:3;
then ( x + y = a + b & |.(x - y).| = |.(a - b).| ) by SUPINF_2:1;
then A10: (x + y) + |.(x - y).| = (a + b) + |.(a - b).| by SUPINF_2:1;
((x + y) + |.(x - y).|) / 2 = ((a + b) + |.(a - b).|) / 2 by A10;
hence max (x,y) = ((x + y) + |.(x - y).|) / 2 by COMPLEX1:74; :: thesis: verum
end;
end;
end;
end;