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 ) ) )