Metamath Proof Explorer

Theorem lenelioc

Description: A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 lenelioc.1 ⊢ φ → A ∈ ℝ *
2 lenelioc.2 ⊢ φ → B ∈ ℝ *
3 lenelioc.3 ⊢ φ → C ∈ ℝ *
4 lenelioc.4 ⊢ φ → C ≤ A
5 3 1 xrlenltd ⊢ φ → C ≤ A ↔ ¬ A < C
6 4 5 mpbid ⊢ φ → ¬ A < C
7 6 intn3an2d ⊢ φ → ¬ C ∈ ℝ * ∧ A < C ∧ C ≤ B
8 elioc1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C ≤ B
9 1 2 8 syl2anc ⊢ φ → C ∈ A B ↔ C ∈ ℝ * ∧ A < C ∧ C ≤ B
10 7 9 mtbird ⊢ φ → ¬ C ∈ A B