Metamath Proof Explorer

Theorem xrre4

Description: An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion xrre4 
|- ( A e. RR* -> ( A e. RR <-> ( A =/= -oo /\ A =/= +oo ) ) )

Proof

Step Hyp Ref Expression
1 renemnf 
 |-  ( A e. RR -> A =/= -oo )
2 1 adantl 
 |-  ( ( A e. RR* /\ A e. RR ) -> A =/= -oo )
3 renepnf 
 |-  ( A e. RR -> A =/= +oo )
4 3 adantl 
 |-  ( ( A e. RR* /\ A e. RR ) -> A =/= +oo )
5 2 4 jca 
 |-  ( ( A e. RR* /\ A e. RR ) -> ( A =/= -oo /\ A =/= +oo ) )
6 5 ex 
 |-  ( A e. RR* -> ( A e. RR -> ( A =/= -oo /\ A =/= +oo ) ) )
7 simpl 
 |-  ( ( A e. RR* /\ ( A =/= -oo /\ A =/= +oo ) ) -> A e. RR* )
8 simprl 
 |-  ( ( A e. RR* /\ ( A =/= -oo /\ A =/= +oo ) ) -> A =/= -oo )
9 simprr 
 |-  ( ( A e. RR* /\ ( A =/= -oo /\ A =/= +oo ) ) -> A =/= +oo )
10 7 8 9 xrred 
 |-  ( ( A e. RR* /\ ( A =/= -oo /\ A =/= +oo ) ) -> A e. RR )
11 10 ex 
 |-  ( A e. RR* -> ( ( A =/= -oo /\ A =/= +oo ) -> A e. RR ) )
12 6 11 impbid 
 |-  ( A e. RR* -> ( A e. RR <-> ( A =/= -oo /\ A =/= +oo ) ) )