Theorem 0lepnf 12337

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

Syntax hints:   ∈ wcel 2048   class class class wbr 4923  0cc0 10327  +∞cpnf 10463  ℝ^*cxr 10465   ≤ cle 10467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-addrcl 10388  ax-rnegex 10398  ax-cnre 10400

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-xp 5406  df-cnv 5408  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472

This theorem is referenced by:  xnn0ge0  12338  xsubge0  12463  xadddi2  12499  xnn0xrge0  12700  pcge0  16044  leordtval2  21514  iccpnfcnv  23241  taylfval  24640  elxrge02  30343  xrge0adddir  30389  xrge0iifcnv  30777  lmxrge0  30796  esumpinfval  30933  hashf2  30944  esumcvg  30946  pnfel0pnf  41181