Metamath Proof Explorer

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 ⊢B∈ℝ∧C∈AB→C∈ℝ

Proof

Step Hyp Ref Expression
1 df-ioc ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x<z∧z≤y
2 1 elixx3g ⊢C∈AB↔A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<C∧C≤B
3 2 biimpi ⊢C∈AB→A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<C∧C≤B
4 3 simpld ⊢C∈AB→A∈ℝ*∧B∈ℝ*∧C∈ℝ*
5 4 simp3d ⊢C∈AB→C∈ℝ*
6 5 adantl ⊢B∈ℝ∧C∈AB→C∈ℝ*
7 simpl ⊢B∈ℝ∧C∈AB→B∈ℝ
8 mnfxr ⊢−∞∈ℝ*
9 8 a1i ⊢C∈AB→−∞∈ℝ*
10 4 simp1d ⊢C∈AB→A∈ℝ*
11 mnfle ⊢A∈ℝ*→−∞≤A
12 10 11 syl ⊢C∈AB→−∞≤A
13 3 simprd ⊢C∈AB→A<C∧C≤B
14 13 simpld ⊢C∈AB→A<C
15 9 10 5 12 14 xrlelttrd ⊢C∈AB→−∞<C
16 15 adantl ⊢B∈ℝ∧C∈AB→−∞<C
17 13 simprd ⊢C∈AB→C≤B
18 17 adantl ⊢B∈ℝ∧C∈AB→C≤B
19 xrre ⊢C∈ℝ*∧B∈ℝ∧−∞<C∧C≤B→C∈ℝ
20 6 7 16 18 19 syl22anc ⊢B∈ℝ∧C∈AB→C∈ℝ