This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 +∞