Metamath Proof Explorer

Theorem ltnelicc

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

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

Proof

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