This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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