Metamath Proof Explorer

Theorem gtnelicc

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

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

Proof

Step Hyp Ref Expression
1 gtnelicc.a ⊢ φ → A ∈ ℝ *
2 gtnelicc.b ⊢ φ → B ∈ ℝ
3 gtnelicc.c ⊢ φ → C ∈ ℝ *
4 gtnelicc.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 intnand ⊢ φ → ¬ A ≤ C ∧ C ≤ B
10 elicc4 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B
11 1 5 3 10 syl3anc ⊢ φ → C ∈ A B ↔ A ≤ C ∧ C ≤ B
12 9 11 mtbird ⊢ φ → ¬ C ∈ A B