Metamath Proof Explorer


Theorem xrnpnfmnf

Description: An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

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