elioore

Description: A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	elioore	$⊢ A \in (B, C) \to A \in ℝ$

Step	Hyp	Ref	Expression
1		elioo3g	$⊢ A \in (B, C) \leftrightarrow ((B \in ℝ^{} \land C \in ℝ^{} \land A \in ℝ^{*}) \land (B < A \land A < C))$
2		3ancomb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land A \in ℝ^{}) \leftrightarrow (B \in ℝ^{} \land A \in ℝ^{} \land C \in ℝ^{})$
3		xrre2	$⊢ ((B \in ℝ^{} \land A \in ℝ^{} \land C \in ℝ^{*}) \land (B < A \land A < C)) \to A \in ℝ$
4	2 3	sylanb	$⊢ ((B \in ℝ^{} \land C \in ℝ^{} \land A \in ℝ^{*}) \land (B < A \land A < C)) \to A \in ℝ$
5	1 4	sylbi	$⊢ A \in (B, C) \to A \in ℝ$

Metamath Proof Explorer