ubioc1

Description: The upper bound belongs to an open-below, closed-above interval. See ubicc2 . (Contributed by FL, 29-May-2014)

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

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

Metamath Proof Explorer