Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
iocleubd
Metamath Proof Explorer
Description: An element of a left-open right-closed interval is smaller than or equal
to its upper bound. (Contributed by Glauco Siliprandi , 23-Oct-2021)
Ref
Expression
Hypotheses
iocleubd.1
⊢ φ → A ∈ ℝ *
iocleubd.2
⊢ φ → B ∈ ℝ *
iocleubd.3
⊢ φ → C ∈ A B
Assertion
iocleubd
⊢ φ → C ≤ B
Proof
Step
Hyp
Ref
Expression
1
iocleubd.1
⊢ φ → A ∈ ℝ *
2
iocleubd.2
⊢ φ → B ∈ ℝ *
3
iocleubd.3
⊢ φ → C ∈ A B
4
iocleub
⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → C ≤ B
5
1 2 3 4
syl3anc
⊢ φ → C ≤ B