This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ge0lere

Description: A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Hypotheses	ge0lere.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
		ge0lere.b	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
		ge0lere.l	⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
	Assertion	ge0lere	⊢ ( 𝜑 → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ge0lere.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ge0lere.b	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
3		ge0lere.l	⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
4		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ^*
5	4 2	sselid	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
6		pnfxr	⊢ +∞ ∈ ℝ^*
7	6	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
8	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
9	1	ltpnfd	⊢ ( 𝜑 → 𝐴 < +∞ )
10	5 8 7 3 9	xrlelttrd	⊢ ( 𝜑 → 𝐵 < +∞ )
11	5 7 10	xrltned	⊢ ( 𝜑 → 𝐵 ≠ +∞ )
12		ge0xrre	⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≠ +∞ ) → 𝐵 ∈ ℝ )
13	2 11 12	syl2anc	⊢ ( 𝜑 → 𝐵 ∈ ℝ )