Metamath Proof Explorer

Theorem gtnelioc

Description: A real number larger than the upper bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses gtnelioc.a ⊢ φ → A ∈ ℝ *
gtnelioc.b ⊢ φ → B ∈ ℝ
gtnelioc.c ⊢ φ → C ∈ ℝ *
gtnelioc.bltc ⊢ φ → B < C
Assertion gtnelioc ⊢ φ → ¬ C ∈ A B

Proof

Step Hyp Ref Expression
1 gtnelioc.a ⊢ φ → A ∈ ℝ *
2 gtnelioc.b ⊢ φ → B ∈ ℝ
3 gtnelioc.c ⊢ φ → C ∈ ℝ *
4 gtnelioc.bltc ⊢ φ → B < C
5 2 rexrd ⊢ φ → B ∈ ℝ *
6 xrltnle ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B < C ↔ ¬ C ≤ B
7 5 3 6 syl2anc ⊢ φ → B < C ↔ ¬ C ≤ B
8 4 7 mpbid ⊢ φ → ¬ C ≤ B
9 8 intn3an3d ⊢ φ → ¬ C ∈ ℝ ∧ A < C ∧ C ≤ B
10 elioc2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C ≤ B
11 1 2 10 syl2anc ⊢ φ → C ∈ A B ↔ C ∈ ℝ ∧ A < C ∧ C ≤ B
12 9 11 mtbird ⊢ φ → ¬ C ∈ A B