Metamath Proof Explorer


Theorem iocgtlb

Description: An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion iocgtlb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < 𝐶 )

Proof

Step Hyp Ref Expression
1 elioc1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵 ) ) )
2 simp2 ( ( 𝐶 ∈ ℝ*𝐴 < 𝐶𝐶𝐵 ) → 𝐴 < 𝐶 )
3 1 2 syl6bi ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → 𝐴 < 𝐶 ) )
4 3 3impia ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < 𝐶 )