Theorem 0lepnf 13153

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

Syntax hints:   ∈ wcel 2143   class class class wbr 5109  0cc0 11095  +∞cpnf 11235  ℝ^*cxr 11237   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-addrcl 11156  ax-rnegex 11166  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244

This theorem is referenced by:  xnn0ge0  13154  xsubge0  13282  xadddi2  13318  xnn0xrge0  13528  pcge0  16917  leordtval2  23369  iccpnfcnv  25103  taylfval  26522  elxrge02  33251  xrge0adddir  33338  xrge0iifcnv  34323  lmxrge0  34342  esumpinfval  34463  hashf2  34474  esumcvg  34476  aks4d1p1p6  42860  pnfel0pnf  46264