Theorem 0le0 12320

Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
0le0	⊢ 0 ≤ 0

Proof of Theorem 0le0

Step	Hyp	Ref	Expression
1		0re 11223	. 2 ⊢ 0 ∈ ℝ
2	1	leidi 11755	1 ⊢ 0 ≤ 0

Syntax hints:   class class class wbr 5148  0cc0 11116   ≤ cle 11256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-resscn 11173  ax-1cn 11174  ax-addrcl 11177  ax-rnegex 11187  ax-cnre 11189  ax-pre-lttri 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261

This theorem is referenced by:  nn0ledivnn  13094  xsubge0  13247  xmulge0  13270  0e0icopnf  13442  0e0iccpnf  13443  0elunit  13453  0mod  13874  sqlecan  14180  discr  14210  cnpart  15194  sqrt0  15195  resqrex  15204  sqrt00  15217  fsumabs  15754  rpnnen2lem4  16167  divalglem7  16349  pcmptdvds  16834  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  ramz2  16964  ramz  16965  isabvd  20575  prdsxmetlem  24107  metustto  24295  cfilucfil  24301  nmolb2d  24468  nmoi  24478  nmoix  24479  nmoleub  24481  nmo0  24485  pcoval1  24773  pco0  24774  minveclem7  25196  ovolfiniun  25263  ovolicc1  25278  ioorf  25335  itg1ge0a  25474  mbfi1fseqlem5  25482  itg2const  25503  itg2const2  25504  itg2splitlem  25511  itg2cnlem1  25524  itg2cnlem2  25525  iblss  25567  itgle  25572  ibladdlem  25582  iblabs  25591  iblabsr  25592  iblmulc2  25593  bddmulibl  25601  bddiblnc  25604  c1lip1  25763  dveq0  25766  dv11cn  25767  fta1g  25934  abelthlem2  26195  sinq12ge0  26269  cxpge0  26442  abscxp2  26452  log2ublem3  26704  chtwordi  26911  ppiwordi  26917  chpub  26974  bposlem1  27038  bposlem6  27043  dchrisum0flblem2  27263  qabvle  27379  ostth2lem2  27388  colinearalg  28450  eucrct2eupth  29780  ex-po  29970  nvz0  30203  nmlnoubi  30331  nmblolbii  30334  blocnilem  30339  siilem2  30387  minvecolem7  30418  pjneli  31258  nmbdoplbi  31559  nmcoplbi  31563  nmbdfnlbi  31584  nmcfnlbi  31587  nmopcoi  31630  unierri  31639  leoprf2  31662  leoprf  31663  stle0i  31774  xrge0iifcnv  33226  xrge0iifiso  33228  xrge0iifhom  33230  esumrnmpt2  33379  dstfrvclim1  33789  ballotlemrc  33842  signsply0  33875  chtvalz  33954  poimirlem23  36827  mblfinlem2  36842  itg2addnclem  36855  itg2gt0cn  36859  ibladdnclem  36860  itgaddnclem2  36863  iblabsnc  36868  iblmulc2nc  36869  ftc1anclem5  36881  ftc1anclem7  36883  ftc1anclem8  36884  ftc1anc  36885  areacirclem1  36892  areacirclem4  36895  mettrifi  36941  monotoddzzfi  41996  rmxypos  42001  rmygeid  42018  stoweidlem55  45082  fourierdlem14  45148  fourierdlem20  45154  fourierdlem92  45225  fourierdlem93  45226  fouriersw  45258  isomennd  45558  ovnssle  45588  hoidmvlelem3  45624  ovnhoilem1  45628  nnlog2ge0lt1  47352  dig1  47394  sepfsepc  47660  seppcld  47662  ex-gte  47874