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 ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ℝ ↔ ( -∞ < 𝐴 ∧ 𝐴 < +∞ ) ) )

Proof

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