Metamath Proof Explorer


Theorem xrred

Description: An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses xrred.1 ( 𝜑𝐴 ∈ ℝ* )
xrred.2 ( 𝜑𝐴 ≠ -∞ )
xrred.3 ( 𝜑𝐴 ≠ +∞ )
Assertion xrred ( 𝜑𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 xrred.1 ( 𝜑𝐴 ∈ ℝ* )
2 xrred.2 ( 𝜑𝐴 ≠ -∞ )
3 xrred.3 ( 𝜑𝐴 ≠ +∞ )
4 1 2 jca ( 𝜑 → ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) )
5 xrnemnf ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
6 4 5 sylib ( 𝜑 → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
7 3 neneqd ( 𝜑 → ¬ 𝐴 = +∞ )
8 pm2.53 ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) → ( ¬ 𝐴 ∈ ℝ → 𝐴 = +∞ ) )
9 8 con1d ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) → ( ¬ 𝐴 = +∞ → 𝐴 ∈ ℝ ) )
10 6 7 9 sylc ( 𝜑𝐴 ∈ ℝ )