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 ∈ A B → C ∈ ℝ

Proof

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