Theorem elicore

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

	Ref	Expression
Assertion	elicore	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
2	1	elixx3g	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
3	2	biimpi	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
4	3	simpld	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
5	4	simp3d	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → 𝐶 ∈ ℝ* )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ* )
7		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ∈ ℝ )
8	3	simprd	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) )
9	8	simpld	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → 𝐴 ≤ 𝐶 )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ≤ 𝐶 )
11	4	simp2d	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ℝ* )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
13		pnfxr	⊢ +∞ ∈ ℝ*
14	13	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → +∞ ∈ ℝ* )
15	8	simprd	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → 𝐶 < 𝐵 )
16	15	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 < 𝐵 )
17		pnfge	⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
18	11 17	syl	⊢ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ≤ +∞ )
19	18	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ≤ +∞ )
20	6 12 14 16 19	xrltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 < +∞ )
21		xrre3	⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < +∞ ) ) → 𝐶 ∈ ℝ )
22	6 7 10 20 21	syl22anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ )