This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrrebnd

Description: An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 mnflt 
 |-  ( A e. RR -> -oo < A )
2 ltpnf 
 |-  ( A e. RR -> A < +oo )
3 1 2 jca 
 |-  ( A e. RR -> ( -oo < A /\ A < +oo ) )
4 nltpnft 
 |-  ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
5 ngtmnft 
 |-  ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
6 4 5 orbi12d 
 |-  ( A e. RR* -> ( ( A = +oo \/ A = -oo ) <-> ( -. A < +oo \/ -. -oo < A ) ) )
7 ianor 
 |-  ( -. ( -oo < A /\ A < +oo ) <-> ( -. -oo < A \/ -. A < +oo ) )
8 orcom 
 |-  ( ( -. -oo < A \/ -. A < +oo ) <-> ( -. A < +oo \/ -. -oo < A ) )
9 7 8 bitr2i 
 |-  ( ( -. A < +oo \/ -. -oo < A ) <-> -. ( -oo < A /\ A < +oo ) )
10 6 9 bitrdi 
 |-  ( A e. RR* -> ( ( A = +oo \/ A = -oo ) <-> -. ( -oo < A /\ A < +oo ) ) )
11 10 con2bid 
 |-  ( A e. RR* -> ( ( -oo < A /\ A < +oo ) <-> -. ( A = +oo \/ A = -oo ) ) )
12 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
13 3orass 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( A e. RR \/ ( A = +oo \/ A = -oo ) ) )
14 orcom 
 |-  ( ( A e. RR \/ ( A = +oo \/ A = -oo ) ) <-> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
15 13 14 bitri 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
16 12 15 sylbb 
 |-  ( A e. RR* -> ( ( A = +oo \/ A = -oo ) \/ A e. RR ) )
17 16 ord 
 |-  ( A e. RR* -> ( -. ( A = +oo \/ A = -oo ) -> A e. RR ) )
18 11 17 sylbid 
 |-  ( A e. RR* -> ( ( -oo < A /\ A < +oo ) -> A e. RR ) )
19 3 18 impbid2 
 |-  ( A e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )