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

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 )
;

end;

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;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

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;

end;per cases
( y = -infty or y <> -infty )
;

end;

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;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

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;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