Theorem elxrge0

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

	Ref	Expression
Assertion	elxrge0	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-3an	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ 𝐴 ≤ +∞ ) )
2		0xr	⊢ 0 ∈ ℝ*
3		pnfxr	⊢ +∞ ∈ ℝ*
4		elicc1	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) ) )
5	2 3 4	mp2an	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) )
6		pnfge	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≤ +∞ )
8	7	pm4.71i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ 𝐴 ≤ +∞ ) )
9	1 5 8	3bitr4i	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) )