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 ( x = -infty or x <> -infty ) ;
suppose A4: x = -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / 2
then ( x + y = -infty & x - y = -infty ) by A2, A3, XXREAL_3:14, XXREAL_3:def 2;
then A5: (x + y) - |.(x - y).| = -infty by XXREAL_3:14;
A6: min (x,y) = -infty by A4, XXREAL_0:44;
thus min (x,y) = ((x + y) - |.(x - y).|) / 2 by A6, A5, XXREAL_3:86; :: thesis: verum
end;
suppose x <> -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / 2
then reconsider a = x as Element of REAL by A1, XXREAL_0:14;
per cases ( y = -infty or y <> -infty ) ;
suppose A7: y = -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / 2
then ( x + y = -infty & x - y = +infty ) by A1, A3, XXREAL_3:14, XXREAL_3:def 2;
then A8: (x + y) - |.(x - y).| = -infty by XXREAL_3:14;
A9: min (x,y) = -infty by A7, XXREAL_0:44;
thus min (x,y) = ((x + y) - |.(x - y).|) / 2 by A9, A8, XXREAL_3:86; :: thesis: verum
end;
suppose y <> -infty ; :: thesis: min (x,y) = ((x + y) - |.(x - y).|) / 2
then reconsider b = y as Element of REAL by A2, XXREAL_0:14;
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;