Metamath Proof Explorer


Theorem xrred

Description: An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses xrred.1
|- ( ph -> A e. RR* )
xrred.2
|- ( ph -> A =/= -oo )
xrred.3
|- ( ph -> A =/= +oo )
Assertion xrred
|- ( ph -> A e. RR )

Proof

Step Hyp Ref Expression
1 xrred.1
 |-  ( ph -> A e. RR* )
2 xrred.2
 |-  ( ph -> A =/= -oo )
3 xrred.3
 |-  ( ph -> A =/= +oo )
4 1 2 jca
 |-  ( ph -> ( A e. RR* /\ A =/= -oo ) )
5 xrnemnf
 |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
6 4 5 sylib
 |-  ( ph -> ( A e. RR \/ A = +oo ) )
7 3 neneqd
 |-  ( ph -> -. A = +oo )
8 pm2.53
 |-  ( ( A e. RR \/ A = +oo ) -> ( -. A e. RR -> A = +oo ) )
9 8 con1d
 |-  ( ( A e. RR \/ A = +oo ) -> ( -. A = +oo -> A e. RR ) )
10 6 7 9 sylc
 |-  ( ph -> A e. RR )