Theorem eliocre

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

	Ref	Expression
Assertion	eliocre	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐶 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		df-ioc	⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
2	1	elixx3g	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
3	2	biimpi	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
4	3	simpld	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
5	4	simp3d	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → 𝐶 ∈ ℝ* )
6	5	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐶 ∈ ℝ* )
7		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐵 ∈ ℝ )
8		mnfxr	⊢ -∞ ∈ ℝ*
9	8	a1i	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → -∞ ∈ ℝ* )
10	4	simp1d	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → 𝐴 ∈ ℝ* )
11		mnfle	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
12	10 11	syl	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → -∞ ≤ 𝐴 )
13	3	simprd	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → ( 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵 ) )
14	13	simpld	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → 𝐴 < 𝐶 )
15	9 10 5 12 14	xrlelttrd	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → -∞ < 𝐶 )
16	15	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → -∞ < 𝐶 )
17	13	simprd	⊢ ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → 𝐶 ≤ 𝐵 )
18	17	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐶 ≤ 𝐵 )
19		xrre	⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( -∞ < 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) → 𝐶 ∈ ℝ )
20	6 7 16 18 19	syl22anc	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐶 ∈ ℝ )