Theorem 0lepnf 13100

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5110  0cc0 11075  +∞cpnf 11212  ℝ^*cxr 11214   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  xnn0ge0  13101  xsubge0  13228  xadddi2  13264  xnn0xrge0  13474  pcge0  16840  leordtval2  23106  iccpnfcnv  24849  taylfval  26273  elxrge02  32859  xrge0adddir  32966  xrge0iifcnv  33930  lmxrge0  33949  esumpinfval  34070  hashf2  34081  esumcvg  34083  aks4d1p1p6  42068  pnfel0pnf  45533