Theorem eliccd

Description: Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	eliccd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	eliccd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	eliccd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	eliccd.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
	eliccd.5	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
Assertion	eliccd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eliccd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		eliccd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		eliccd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		eliccd.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
5		eliccd.5	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
6		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
7	1 2 6	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
8	3 4 5 7	mpbir3and	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )