Theorem 0lepnf 13262

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 11356	. 2 ⊢ 0 ∈ ℝ*
2		pnfge 13259	. 2 ⊢ (0 ∈ ℝ* → 0 ≤ +∞)
3	1, 2	ax-mp 5	1 ⊢ 0 ≤ +∞

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  0cc0 11200  +∞cpnf 11340  ℝ^*cxr 11342   ≤ cle 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349

This theorem is used by:  xnn0ge0  13263  xsubge0  13391  xadddi2  13427  xnn0xrge0  13637  pcge0  17040  leordtval2  23530  iccpnfcnv  25265  taylfval  26686  elxrge02  33498  xrge0adddir  33579  xrge0iifcnv  34565  lmxrge0  34584  esumpinfval  34705  hashf2  34716  esumcvg  34718  aks4d1p1p6  43123  pnfel0pnf  46539