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 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
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 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |