Theorem xrge0nemnfd

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

	Ref	Expression
Hypothesis	xrge0nemnfd.1	⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,] +∞ ) )
Assertion	xrge0nemnfd	⊢ ( 𝜑 → 𝐴 ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		xrge0nemnfd.1	⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,] +∞ ) )
2		mnfxr	⊢ -∞ ∈ ℝ*
3	2	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
4		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5	4 1	sselid	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
6		0xr	⊢ 0 ∈ ℝ*
7	6	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
8		mnflt0	⊢ -∞ < 0
9	8	a1i	⊢ ( 𝜑 → -∞ < 0 )
10		pnfxr	⊢ +∞ ∈ ℝ*
11	10	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
12		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐴 )
13	7 11 1 12	syl3anc	⊢ ( 𝜑 → 0 ≤ 𝐴 )
14	3 7 5 9 13	xrltletrd	⊢ ( 𝜑 → -∞ < 𝐴 )
15	3 5 14	xrgtned	⊢ ( 𝜑 → 𝐴 ≠ -∞ )