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 ∈ ℝ * → A ∈ ℝ ↔ −∞ < A ∧ A < +∞

Proof

Step Hyp Ref Expression
1 mnflt ⊢ A ∈ ℝ → −∞ < A
2 ltpnf ⊢ A ∈ ℝ → A < +∞
3 1 2 jca ⊢ A ∈ ℝ → −∞ < A ∧ A < +∞
4 nltpnft ⊢ A ∈ ℝ * → A = +∞ ↔ ¬ A < +∞
5 ngtmnft ⊢ A ∈ ℝ * → A = −∞ ↔ ¬ −∞ < A
6 4 5 orbi12d ⊢ A ∈ ℝ * → A = +∞ ∨ A = −∞ ↔ ¬ A < +∞ ∨ ¬ −∞ < A
7 ianor ⊢ ¬ −∞ < A ∧ A < +∞ ↔ ¬ −∞ < A ∨ ¬ A < +∞
8 orcom ⊢ ¬ −∞ < A ∨ ¬ A < +∞ ↔ ¬ A < +∞ ∨ ¬ −∞ < A
9 7 8 bitr2i ⊢ ¬ A < +∞ ∨ ¬ −∞ < A ↔ ¬ −∞ < A ∧ A < +∞
10 6 9 bitrdi ⊢ A ∈ ℝ * → A = +∞ ∨ A = −∞ ↔ ¬ −∞ < A ∧ A < +∞
11 10 con2bid ⊢ A ∈ ℝ * → −∞ < A ∧ A < +∞ ↔ ¬ A = +∞ ∨ A = −∞
12 elxr ⊢ A ∈ ℝ * ↔ A ∈ ℝ ∨ A = +∞ ∨ A = −∞
13 3orass ⊢ A ∈ ℝ ∨ A = +∞ ∨ A = −∞ ↔ A ∈ ℝ ∨ A = +∞ ∨ A = −∞
14 orcom ⊢ A ∈ ℝ ∨ A = +∞ ∨ A = −∞ ↔ A = +∞ ∨ A = −∞ ∨ A ∈ ℝ
15 13 14 bitri ⊢ A ∈ ℝ ∨ A = +∞ ∨ A = −∞ ↔ A = +∞ ∨ A = −∞ ∨ A ∈ ℝ
16 12 15 sylbb ⊢ A ∈ ℝ * → A = +∞ ∨ A = −∞ ∨ A ∈ ℝ
17 16 ord ⊢ A ∈ ℝ * → ¬ A = +∞ ∨ A = −∞ → A ∈ ℝ
18 11 17 sylbid ⊢ A ∈ ℝ * → −∞ < A ∧ A < +∞ → A ∈ ℝ
19 3 18 impbid2 ⊢ A ∈ ℝ * → A ∈ ℝ ↔ −∞ < A ∧ A < +∞