xrge0nemnfd

Description: A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	xrge0nemnfd.1	$⊢ φ \to A \in [0, +∞]$
	Assertion	xrge0nemnfd	$⊢ φ \to A \neq −∞$

Step	Hyp	Ref	Expression
1		xrge0nemnfd.1	$⊢ φ \to A \in [0, +∞]$
2		mnfxr	$⊢ −∞ \in ℝ^{*}$
3	2	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
4		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
5	4 1	sselid	$⊢ φ \to A \in ℝ^{*}$
6		0xr	$⊢ 0 \in ℝ^{*}$
7	6	a1i	$⊢ φ \to 0 \in ℝ^{*}$
8		mnflt0	$⊢ −∞ < 0$
9	8	a1i	$⊢ φ \to −∞ < 0$
10		pnfxr	$⊢ +∞ \in ℝ^{*}$
11	10	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
12		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land A \in [0, +∞]) \to 0 \leq A$
13	7 11 1 12	syl3anc	$⊢ φ \to 0 \leq A$
14	3 7 5 9 13	xrltletrd	$⊢ φ \to −∞ < A$
15	3 5 14	xrgtned	$⊢ φ \to A \neq −∞$

Metamath Proof Explorer