Metamath Proof Explorer

Theorem xrgtnelicc

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

Ref Expression
Hypotheses xrgtnelicc.1 ⊢ φ → A ∈ ℝ *
xrgtnelicc.2 ⊢ φ → B ∈ ℝ *
xrgtnelicc.3 ⊢ φ → C ∈ ℝ *
xrgtnelicc.4 ⊢ φ → B < C
Assertion xrgtnelicc ⊢ φ → ¬ C ∈ A B

Proof

Step Hyp Ref Expression
1 xrgtnelicc.1 ⊢ φ → A ∈ ℝ *
2 xrgtnelicc.2 ⊢ φ → B ∈ ℝ *
3 xrgtnelicc.3 ⊢ φ → C ∈ ℝ *
4 xrgtnelicc.4 ⊢ φ → B < C
5 xrltnle ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B < C ↔ ¬ C ≤ B
6 2 3 5 syl2anc ⊢ φ → B < C ↔ ¬ C ≤ B
7 4 6 mpbid ⊢ φ → ¬ C ≤ B
8 7 intnand ⊢ φ → ¬ A ≤ C ∧ C ≤ B
9 elicc4 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A B ↔ A ≤ C ∧ C ≤ B
10 1 2 3 9 syl3anc ⊢ φ → C ∈ A B ↔ A ≤ C ∧ C ≤ B
11 8 10 mtbird ⊢ φ → ¬ C ∈ A B