# 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}\in {ℝ}^{*}\to \left({A}\in ℝ↔\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)\right)$

### Proof

Step Hyp Ref Expression
1 mnflt ${⊢}{A}\in ℝ\to \mathrm{-\infty }<{A}$
2 ltpnf ${⊢}{A}\in ℝ\to {A}<\mathrm{+\infty }$
3 1 2 jca ${⊢}{A}\in ℝ\to \left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)$
4 nltpnft ${⊢}{A}\in {ℝ}^{*}\to \left({A}=\mathrm{+\infty }↔¬{A}<\mathrm{+\infty }\right)$
5 ngtmnft ${⊢}{A}\in {ℝ}^{*}\to \left({A}=\mathrm{-\infty }↔¬\mathrm{-\infty }<{A}\right)$
6 4 5 orbi12d ${⊢}{A}\in {ℝ}^{*}\to \left(\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)↔\left(¬{A}<\mathrm{+\infty }\vee ¬\mathrm{-\infty }<{A}\right)\right)$
7 ianor ${⊢}¬\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)↔\left(¬\mathrm{-\infty }<{A}\vee ¬{A}<\mathrm{+\infty }\right)$
8 orcom ${⊢}\left(¬\mathrm{-\infty }<{A}\vee ¬{A}<\mathrm{+\infty }\right)↔\left(¬{A}<\mathrm{+\infty }\vee ¬\mathrm{-\infty }<{A}\right)$
9 7 8 bitr2i ${⊢}\left(¬{A}<\mathrm{+\infty }\vee ¬\mathrm{-\infty }<{A}\right)↔¬\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)$
10 6 9 syl6bb ${⊢}{A}\in {ℝ}^{*}\to \left(\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)↔¬\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)\right)$
11 10 con2bid ${⊢}{A}\in {ℝ}^{*}\to \left(\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)↔¬\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\right)$
12 elxr ${⊢}{A}\in {ℝ}^{*}↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
13 3orass ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)↔\left({A}\in ℝ\vee \left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\right)$
14 orcom ${⊢}\left({A}\in ℝ\vee \left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\right)↔\left(\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\vee {A}\in ℝ\right)$
15 13 14 bitri ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)↔\left(\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\vee {A}\in ℝ\right)$
16 12 15 sylbb ${⊢}{A}\in {ℝ}^{*}\to \left(\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\vee {A}\in ℝ\right)$
17 16 ord ${⊢}{A}\in {ℝ}^{*}\to \left(¬\left({A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\to {A}\in ℝ\right)$
18 11 17 sylbid ${⊢}{A}\in {ℝ}^{*}\to \left(\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)\to {A}\in ℝ\right)$
19 3 18 impbid2 ${⊢}{A}\in {ℝ}^{*}\to \left({A}\in ℝ↔\left(\mathrm{-\infty }<{A}\wedge {A}<\mathrm{+\infty }\right)\right)$