Theorem eliccxrd

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

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

Proof

Step	Hyp	Ref	Expression
1		eliccxrd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		eliccxrd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		eliccxrd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		eliccxrd.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
5		eliccxrd.5	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
6	4 5	jca	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) )
7		elicc4	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
8	1 2 3 7	syl3anc	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
9	6 8	mpbird	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )