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 ⊢ φ → A ∈ ℝ
ge0lere.b ⊢ φ → B ∈ 0 +∞
ge0lere.l ⊢ φ → B ≤ A
Assertion ge0lere ⊢ φ → B ∈ ℝ

Proof

Step Hyp Ref Expression
1 ge0lere.a ⊢ φ → A ∈ ℝ
2 ge0lere.b ⊢ φ → B ∈ 0 +∞
3 ge0lere.l ⊢ φ → B ≤ A
4 iccssxr ⊢ 0 +∞ ⊆ ℝ *
5 4 2 sselid ⊢ φ → B ∈ ℝ *
6 pnfxr ⊢ +∞ ∈ ℝ *
7 6 a1i ⊢ φ → +∞ ∈ ℝ *
8 1 rexrd ⊢ φ → A ∈ ℝ *
9 1 ltpnfd ⊢ φ → A < +∞
10 5 8 7 3 9 xrlelttrd ⊢ φ → B < +∞
11 5 7 10 xrltned ⊢ φ → B ≠ +∞
12 ge0xrre ⊢ B ∈ 0 +∞ ∧ B ≠ +∞ → B ∈ ℝ
13 2 11 12 syl2anc ⊢ φ → B ∈ ℝ