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 ( 𝜑𝐴 ∈ ℝ )
ltnelicc.b ( 𝜑𝐵 ∈ ℝ* )
ltnelicc.c ( 𝜑𝐶 ∈ ℝ* )
ltnelicc.clta ( 𝜑𝐶 < 𝐴 )
Assertion ltnelicc ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ltnelicc.a ( 𝜑𝐴 ∈ ℝ )
2 ltnelicc.b ( 𝜑𝐵 ∈ ℝ* )
3 ltnelicc.c ( 𝜑𝐶 ∈ ℝ* )
4 ltnelicc.clta ( 𝜑𝐶 < 𝐴 )
5 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
6 xrltnle ( ( 𝐶 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 𝐶 < 𝐴 ↔ ¬ 𝐴𝐶 ) )
7 3 5 6 syl2anc ( 𝜑 → ( 𝐶 < 𝐴 ↔ ¬ 𝐴𝐶 ) )
8 4 7 mpbid ( 𝜑 → ¬ 𝐴𝐶 )
9 8 intnanrd ( 𝜑 → ¬ ( 𝐴𝐶𝐶𝐵 ) )
10 elicc4 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴𝐶𝐶𝐵 ) ) )
11 5 2 3 10 syl3anc ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴𝐶𝐶𝐵 ) ) )
12 9 11 mtbird ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )