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	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐶 ∈ ℝ )

Metamath Proof Explorer

Theorem eliocre

Proof