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 (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$

Proof

Step	Hyp	Ref	Expression
1		mnflt	$⊢ A \in ℝ \to −∞ < A$
2		ltpnf	$⊢ A \in ℝ \to A < +∞$
3	1 2	jca	$⊢ A \in ℝ \to (−∞ < A \land A < +∞)$
4		nltpnft	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$
5		ngtmnft	$⊢ A \in ℝ^{*} \to (A = −∞ \leftrightarrow \neg −∞ < A)$
6	4 5	orbi12d	$⊢ A \in ℝ^{*} \to ((A = +∞ \lor A = −∞) \leftrightarrow (\neg A < +∞ \lor \neg −∞ < A))$
7		ianor	$⊢ \neg (−∞ < A \land A < +∞) \leftrightarrow (\neg −∞ < A \lor \neg A < +∞)$
8		orcom	$⊢ (\neg −∞ < A \lor \neg A < +∞) \leftrightarrow (\neg A < +∞ \lor \neg −∞ < A)$
9	7 8	bitr2i	$⊢ (\neg A < +∞ \lor \neg −∞ < A) \leftrightarrow \neg (−∞ < A \land A < +∞)$
10	6 9	bitrdi	$⊢ A \in ℝ^{*} \to ((A = +∞ \lor A = −∞) \leftrightarrow \neg (−∞ < A \land A < +∞))$
11	10	con2bid	$⊢ A \in ℝ^{*} \to ((−∞ < A \land A < +∞) \leftrightarrow \neg (A = +∞ \lor A = −∞))$
12		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
13		3orass	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \leftrightarrow (A \in ℝ \lor (A = +∞ \lor A = −∞))$
14		orcom	$⊢ (A \in ℝ \lor (A = +∞ \lor A = −∞)) \leftrightarrow ((A = +∞ \lor A = −∞) \lor A \in ℝ)$
15	13 14	bitri	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \leftrightarrow ((A = +∞ \lor A = −∞) \lor A \in ℝ)$
16	12 15	sylbb	$⊢ A \in ℝ^{*} \to ((A = +∞ \lor A = −∞) \lor A \in ℝ)$
17	16	ord	$⊢ A \in ℝ^{*} \to (\neg (A = +∞ \lor A = −∞) \to A \in ℝ)$
18	11 17	sylbid	$⊢ A \in ℝ^{*} \to ((−∞ < A \land A < +∞) \to A \in ℝ)$
19	3 18	impbid2	$⊢ A \in ℝ^{*} \to (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$