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	$⊢ (A \in ℝ \land C \in [A, B)) \to C \in ℝ$

Step	Hyp	Ref	Expression
1		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
2	1	elixx3g	$⊢ C \in [A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq C \land C < B))$
3	2	biimpi	$⊢ C \in [A, B) \to ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A \leq C \land C < B))$
4	3	simpld	$⊢ C \in [A, B) \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*})$
5	4	simp3d	$⊢ C \in [A, B) \to C \in ℝ^{*}$
6	5	adantl	$⊢ (A \in ℝ \land C \in [A, B)) \to C \in ℝ^{*}$
7		simpl	$⊢ (A \in ℝ \land C \in [A, B)) \to A \in ℝ$
8	3	simprd	$⊢ C \in [A, B) \to (A \leq C \land C < B)$
9	8	simpld	$⊢ C \in [A, B) \to A \leq C$
10	9	adantl	$⊢ (A \in ℝ \land C \in [A, B)) \to A \leq C$
11	4	simp2d	$⊢ C \in [A, B) \to B \in ℝ^{*}$
12	11	adantl	$⊢ (A \in ℝ \land C \in [A, B)) \to B \in ℝ^{*}$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14	13	a1i	$⊢ (A \in ℝ \land C \in [A, B)) \to +∞ \in ℝ^{*}$
15	8	simprd	$⊢ C \in [A, B) \to C < B$
16	15	adantl	$⊢ (A \in ℝ \land C \in [A, B)) \to C < B$
17		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
18	11 17	syl	$⊢ C \in [A, B) \to B \leq +∞$
19	18	adantl	$⊢ (A \in ℝ \land C \in [A, B)) \to B \leq +∞$
20	6 12 14 16 19	xrltletrd	$⊢ (A \in ℝ \land C \in [A, B)) \to C < +∞$
21		xrre3	$⊢ ((C \in ℝ^{*} \land A \in ℝ) \land (A \leq C \land C < +∞)) \to C \in ℝ$
22	6 7 10 20 21	syl22anc	$⊢ (A \in ℝ \land C \in [A, B)) \to C \in ℝ$

Metamath Proof Explorer