Theorem pnfel0pnf

Description: +oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pnfel0pnf	⊢ +∞ ∈ ( 0 [,] +∞ )

Proof

Step	Hyp	Ref	Expression
1		0xr	⊢ 0 ∈ ℝ*
2		pnfxr	⊢ +∞ ∈ ℝ*
3		0lepnf	⊢ 0 ≤ +∞
4		ubicc2	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
5	1 2 3 4	mp3an	⊢ +∞ ∈ ( 0 [,] +∞ )