Metamath Proof Explorer


Theorem eliccre

Description: A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliccre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵 ) ) )
2 1 biimp3a ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐶 ∈ ℝ ∧ 𝐴𝐶𝐶𝐵 ) )
3 2 simp1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℝ )