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

Metamath Proof Explorer

Theorem lbicc2

Description: The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007) (Revised by FL, 29-May-2014) (Revised by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Assertion	lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in ℝ^{*}$
2		xrleid	$⊢ A \in ℝ^{*} \to A \leq A$
3	2	3ad2ant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \leq A$
4		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \leq B$
5		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \in [A, B] \leftrightarrow (A \in ℝ^{*} \land A \leq A \land A \leq B))$
6	5	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A \in [A, B] \leftrightarrow (A \in ℝ^{*} \land A \leq A \land A \leq B))$
7	1 3 4 6	mpbir3and	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$