Metamath Proof Explorer

Theorem eliccelicod

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