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	sseldi	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
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	⊢ ( 𝜑 → 𝐵 ∈ ℝ )