Theorem xrinfm

Description: The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018) (Revised by AV, 28-Sep-2020)

	Ref	Expression
Assertion	xrinfm	⊢ inf ( ℝ* , ℝ* , < ) = -∞

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℝ* ⊆ ℝ*
2		mnfxr	⊢ -∞ ∈ ℝ*
3		infxrmnf	⊢ ( ( ℝ* ⊆ ℝ* ∧ -∞ ∈ ℝ* ) → inf ( ℝ* , ℝ* , < ) = -∞ )
4	1 2 3	mp2an	⊢ inf ( ℝ* , ℝ* , < ) = -∞