elxrge0

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	elxrge0	$⊢ A \in [0, +∞] \leftrightarrow (A \in ℝ^{*} \land 0 \leq A)$

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (A \in ℝ^{} \land 0 \leq A \land A \leq +∞) \leftrightarrow ((A \in ℝ^{} \land 0 \leq A) \land A \leq +∞)$
2		0xr	$⊢ 0 \in ℝ^{*}$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (A \in [0, +∞] \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A \leq +∞))$
5	2 3 4	mp2an	$⊢ A \in [0, +∞] \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A \leq +∞)$
6		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
7	6	adantr	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \leq +∞$
8	7	pm4.71i	$⊢ (A \in ℝ^{} \land 0 \leq A) \leftrightarrow ((A \in ℝ^{} \land 0 \leq A) \land A \leq +∞)$
9	1 5 8	3bitr4i	$⊢ A \in [0, +∞] \leftrightarrow (A \in ℝ^{*} \land 0 \leq A)$

Metamath Proof Explorer