Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
ge0lere
Metamath Proof Explorer
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
sseldi
⊢ φ → 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 ∈ ℝ