elicopnf

Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014)

		Ref	Expression
	Assertion	elicopnf	$⊢ A \in ℝ \to (B \in [A, +∞) \leftrightarrow (B \in ℝ \land A \leq B))$

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		elico2	$⊢ (A \in ℝ \land +∞ \in ℝ^{*}) \to (B \in [A, +∞) \leftrightarrow (B \in ℝ \land A \leq B \land B < +∞))$
3	1 2	mpan2	$⊢ A \in ℝ \to (B \in [A, +∞) \leftrightarrow (B \in ℝ \land A \leq B \land B < +∞))$
4		ltpnf	$⊢ B \in ℝ \to B < +∞$
5	4	adantr	$⊢ (B \in ℝ \land A \leq B) \to B < +∞$
6	5	pm4.71i	$⊢ (B \in ℝ \land A \leq B) \leftrightarrow ((B \in ℝ \land A \leq B) \land B < +∞)$
7		df-3an	$⊢ (B \in ℝ \land A \leq B \land B < +∞) \leftrightarrow ((B \in ℝ \land A \leq B) \land B < +∞)$
8	6 7	bitr4i	$⊢ (B \in ℝ \land A \leq B) \leftrightarrow (B \in ℝ \land A \leq B \land B < +∞)$
9	3 8	bitr4di	$⊢ A \in ℝ \to (B \in [A, +∞) \leftrightarrow (B \in ℝ \land A \leq B))$

Metamath Proof Explorer