let x, y be ExtReal; :: thesis: ( x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies min (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: min (x,y) = ((x + y) - |.(x - y).|) / 2
per cases ;
suppose A4: x = -infty ; :: thesis: min (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:14;
A6: min (x,y) = -infty by ;
thus min (x,y) = ((x + y) - |.(x - y).|) / 2 by ; :: thesis: verum
end;
suppose x <> -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / 2
then reconsider a = x as Element of REAL by ;
per cases ;
suppose A7: y = -infty ; :: thesis: min (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:14;
A9: min (x,y) = -infty by ;
thus min (x,y) = ((x + y) - |.(x - y).|) / 2 by ; :: thesis: verum
end;
suppose y <> -infty ; :: thesis: min (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:3;
((x + y) - |.(x - y).|) / 2 = ((a + b) - |.(a - b).|) / 2 by A10;
hence min (x,y) = ((x + y) - |.(x - y).|) / 2 by COMPLEX1:73; :: thesis: verum
end;
end;
end;
end;