lbico1

Description: The lower bound belongs to a closed-below, open-above interval. See lbicc2 . (Contributed by FL, 29-May-2014)

		Ref	Expression
	Assertion	lbico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \in [A, B)$

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

Metamath Proof Explorer