xrre4

Description: An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Assertion	xrre4	$⊢ A \in ℝ^{*} \to (A \in ℝ \leftrightarrow (A \neq −∞ \land A \neq +∞))$

Step	Hyp	Ref	Expression
1		renemnf	$⊢ A \in ℝ \to A \neq −∞$
2	1	adantl	$⊢ (A \in ℝ^{*} \land A \in ℝ) \to A \neq −∞$
3		renepnf	$⊢ A \in ℝ \to A \neq +∞$
4	3	adantl	$⊢ (A \in ℝ^{*} \land A \in ℝ) \to A \neq +∞$
5	2 4	jca	$⊢ (A \in ℝ^{*} \land A \in ℝ) \to (A \neq −∞ \land A \neq +∞)$
6	5	ex	$⊢ A \in ℝ^{*} \to (A \in ℝ \to (A \neq −∞ \land A \neq +∞))$
7		simpl	$⊢ (A \in ℝ^{} \land (A \neq −∞ \land A \neq +∞)) \to A \in ℝ^{}$
8		simprl	$⊢ (A \in ℝ^{*} \land (A \neq −∞ \land A \neq +∞)) \to A \neq −∞$
9		simprr	$⊢ (A \in ℝ^{*} \land (A \neq −∞ \land A \neq +∞)) \to A \neq +∞$
10	7 8 9	xrred	$⊢ (A \in ℝ^{*} \land (A \neq −∞ \land A \neq +∞)) \to A \in ℝ$
11	10	ex	$⊢ A \in ℝ^{*} \to ((A \neq −∞ \land A \neq +∞) \to A \in ℝ)$
12	6 11	impbid	$⊢ A \in ℝ^{*} \to (A \in ℝ \leftrightarrow (A \neq −∞ \land A \neq +∞))$

Metamath Proof Explorer