Theorem 0lepnf 12961

Description: 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0lepnf	⊢ 0 ≤ +∞

Proof of Theorem 0lepnf

Step	Hyp	Ref	Expression
1		0xr 11115	. 2 ⊢ 0 ∈ ℝ*
2		pnfge 12959	. 2 ⊢ (0 ∈ ℝ* → 0 ≤ +∞)
3	1, 2	ax-mp 5	1 ⊢ 0 ≤ +∞

Syntax hints:   ∈ wcel 2105   class class class wbr 5089  0cc0 10964  +∞cpnf 11099  ℝ^*cxr 11101   ≤ cle 11103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-addrcl 11025  ax-rnegex 11035  ax-cnre 11037

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108

This theorem is referenced by:  xnn0ge0  12962  xsubge0  13088  xadddi2  13124  xnn0xrge0  13331  pcge0  16652  leordtval2  22461  iccpnfcnv  24205  taylfval  25616  elxrge02  31434  xrge0adddir  31529  xrge0iifcnv  32122  lmxrge0  32141  esumpinfval  32280  hashf2  32291  esumcvg  32293  aks4d1p1p6  40328  pnfel0pnf  43391