Theorem 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 \left(A\in ℝ\leftrightarrow \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		renemnf	$$⊢A\in ℝ\to A\ne \mathrm{-\infty }$$
2	1	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge A\in ℝ\right)\to A\ne \mathrm{-\infty }$$
3		renepnf	$$⊢A\in ℝ\to A\ne \mathrm{+\infty }$$
4	3	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge A\in ℝ\right)\to A\ne \mathrm{+\infty }$$
5	2 4	jca	$$⊢\left(A\in {ℝ}^{*}\wedge A\in ℝ\right)\to \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)$$
6	5	ex	$$⊢A\in {ℝ}^{*}\to \left(A\in ℝ\to \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)$$
7		simpl	$$⊢\left(A\in {ℝ}^{*}\wedge \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)\to A\in {ℝ}^{*}$$
8		simprl	$$⊢\left(A\in {ℝ}^{*}\wedge \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)\to A\ne \mathrm{-\infty }$$
9		simprr	$$⊢\left(A\in {ℝ}^{*}\wedge \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)\to A\ne \mathrm{+\infty }$$
10	7 8 9	xrred	$$⊢\left(A\in {ℝ}^{*}\wedge \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)\to A\in ℝ$$
11	10	ex	$$⊢A\in {ℝ}^{*}\to \left(\left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\to A\in ℝ\right)$$
12	6 11	impbid	$$⊢A\in {ℝ}^{*}\to \left(A\in ℝ\leftrightarrow \left(A\ne \mathrm{-\infty }\wedge A\ne \mathrm{+\infty }\right)\right)$$