Theorem 0lepnf 13069

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5102  0cc0 11044  +∞cpnf 11181  ℝ^*cxr 11183   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  xnn0ge0  13070  xsubge0  13197  xadddi2  13233  xnn0xrge0  13443  pcge0  16809  leordtval2  23075  iccpnfcnv  24818  taylfval  26242  elxrge02  32825  xrge0adddir  32932  xrge0iifcnv  33896  lmxrge0  33915  esumpinfval  34036  hashf2  34047  esumcvg  34049  aks4d1p1p6  42034  pnfel0pnf  45499