Theorem xrnpnfmnf

Description: An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xrnpnfmnf.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xrnpnfmnf.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
	xrnpnfmnf.3	⊢ ( 𝜑 → 𝐴 ≠ +∞ )
Assertion	xrnpnfmnf	⊢ ( 𝜑 → 𝐴 = -∞ )

Proof

Step	Hyp	Ref	Expression
1		xrnpnfmnf.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xrnpnfmnf.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
3		xrnpnfmnf.3	⊢ ( 𝜑 → 𝐴 ≠ +∞ )
4	1 3	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) )
5		xrnepnf	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = -∞ ) )
6	4 5	sylib	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∨ 𝐴 = -∞ ) )
7		pm2.53	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = -∞ ) → ( ¬ 𝐴 ∈ ℝ → 𝐴 = -∞ ) )
8	6 2 7	sylc	⊢ ( 𝜑 → 𝐴 = -∞ )