This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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