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

Proof

Step	Hyp	Ref	Expression
1		renemnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) → 𝐴 ≠ -∞ )
3		renepnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) → 𝐴 ≠ +∞ )
5	2 4	jca	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) )
6	5	ex	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ℝ → ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) )
7		simpl	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) → 𝐴 ∈ ℝ* )
8		simprl	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) → 𝐴 ≠ -∞ )
9		simprr	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) → 𝐴 ≠ +∞ )
10	7 8 9	xrred	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) → 𝐴 ∈ ℝ )
11	10	ex	⊢ ( 𝐴 ∈ ℝ* → ( ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) → 𝐴 ∈ ℝ ) )
12	6 11	impbid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ℝ ↔ ( 𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞ ) ) )