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