let y, x be ExtReal; :: thesis: ( ( x is real implies ex a being Complex st
( x = a & y = - a ) ) & ( x = +infty implies y = -infty ) & ( not x is real & not x = +infty implies y = +infty ) implies ( ( y is real implies ex a being Complex st
( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) ) )
assume that
A1: ( x is real implies ex a being Complex st
( x = a & y = - a ) ) and
A2: ( x = +infty implies y = -infty ) and
A3: ( not x is real & x <> +infty implies y = +infty ) ; :: thesis: ( ( y is real implies ex a being Complex st
( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) )
thus ( y is real implies ex a being Complex st
( y = a & x = - a ) ) :: thesis: ( ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) )
proof
assume y is real ; :: thesis: ex a being Complex st
( y = a & x = - a )
then consider a being Complex such that
A4: ( x = a & y = - a ) by A1, A2, A3;
take - a ; :: thesis: ( y = - a & x = - (- a) )
thus ( y = - a & x = - (- a) ) by A4; :: thesis: verum
end;
( x in REAL implies x is real ) ;
hence ( y = +infty implies x = -infty ) by A1, A2, XXREAL_0:14; :: thesis: ( not y is real & not y = +infty implies x = +infty )
thus ( not y is real & not y = +infty implies x = +infty ) by A1, A3; :: thesis: verum