Theorem mnfled

Description: Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	mnfled.1	$$⊢\phi \to A\in {ℝ}^{*}$$
Assertion	mnfled	$$⊢\phi \to \mathrm{-\infty }\le A$$

Proof

Step	Hyp	Ref	Expression
1		mnfled.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		mnfle	$$⊢A\in {ℝ}^{*}\to \mathrm{-\infty }\le A$$
3	1 2	syl	$$⊢\phi \to \mathrm{-\infty }\le A$$