# 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 syl6bb
` |-  ( 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 ) ) )`