Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
eliccelicod
Metamath Proof Explorer
Description: A member of a closed interval that is not the upper bound, is a member
of the left-closed, right-open interval. (Contributed by Glauco
Siliprandi , 17-Aug-2020)
Ref
Expression
Hypotheses
eliccelicod.a
⊢ φ → A ∈ ℝ *
eliccelicod.b
⊢ φ → B ∈ ℝ *
eliccelicod.c
⊢ φ → C ∈ A B
eliccelicod.d
⊢ φ → C ≠ B
Assertion
eliccelicod
⊢ φ → C ∈ A B
Proof
Step
Hyp
Ref
Expression
1
eliccelicod.a
⊢ φ → A ∈ ℝ *
2
eliccelicod.b
⊢ φ → B ∈ ℝ *
3
eliccelicod.c
⊢ φ → C ∈ A B
4
eliccelicod.d
⊢ φ → C ≠ B
5
eliccxr
⊢ C ∈ A B → C ∈ ℝ *
6
3 5
syl
⊢ φ → C ∈ ℝ *
7
iccgelb
⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → A ≤ C
8
1 2 3 7
syl3anc
⊢ φ → A ≤ C
9
iccleub
⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → C ≤ B
10
1 2 3 9
syl3anc
⊢ φ → C ≤ B
11
6 2 10 4
xrleneltd
⊢ φ → C < B
12
1 2 6 8 11
elicod
⊢ φ → C ∈ A B