This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eliccnelico

Description: An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses eliccnelico.1 ⊢ φ → A ∈ ℝ *
eliccnelico.b ⊢ φ → B ∈ ℝ *
eliccnelico.c ⊢ φ → C ∈ A B
eliccnelico.nel ⊢ φ → ¬ C ∈ A B
Assertion eliccnelico ⊢ φ → C = B

Proof

Step Hyp Ref Expression
1 eliccnelico.1 ⊢ φ → A ∈ ℝ *
2 eliccnelico.b ⊢ φ → B ∈ ℝ *
3 eliccnelico.c ⊢ φ → C ∈ A B
4 eliccnelico.nel ⊢ φ → ¬ C ∈ A B
5 eliccxr ⊢ C ∈ A B → C ∈ ℝ *
6 3 5 syl ⊢ φ → C ∈ ℝ *
7 iccleub ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → C ≤ B
8 1 2 3 7 syl3anc ⊢ φ → C ≤ B
9 1 adantr ⊢ φ ∧ ¬ B ≤ C → A ∈ ℝ *
10 2 adantr ⊢ φ ∧ ¬ B ≤ C → B ∈ ℝ *
11 6 adantr ⊢ φ ∧ ¬ B ≤ C → C ∈ ℝ *
12 iccgelb ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ A B → A ≤ C
13 1 2 3 12 syl3anc ⊢ φ → A ≤ C
14 13 adantr ⊢ φ ∧ ¬ B ≤ C → A ≤ C
15 simpr ⊢ φ ∧ ¬ B ≤ C → ¬ B ≤ C
16 xrltnle ⊢ C ∈ ℝ * ∧ B ∈ ℝ * → C < B ↔ ¬ B ≤ C
17 6 2 16 syl2anc ⊢ φ → C < B ↔ ¬ B ≤ C
18 17 adantr ⊢ φ ∧ ¬ B ≤ C → C < B ↔ ¬ B ≤ C
19 15 18 mpbird ⊢ φ ∧ ¬ B ≤ C → C < B
20 9 10 11 14 19 elicod ⊢ φ ∧ ¬ B ≤ C → C ∈ A B
21 4 adantr ⊢ φ ∧ ¬ B ≤ C → ¬ C ∈ A B
22 20 21 condan ⊢ φ → B ≤ C
23 6 2 8 22 xrletrid ⊢ φ → C = B