Theorem 0le0 11591

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 10494	. 2 ⊢ 0 ∈ ℝ
2	1	leidi 11027	1 ⊢ 0 ≤ 0

Syntax hints:   class class class wbr 4966  0cc0 10388   ≤ cle 10527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-resscn 10445  ax-1cn 10446  ax-addrcl 10449  ax-rnegex 10459  ax-cnre 10461  ax-pre-lttri 10462

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-er 8144  df-en 8363  df-dom 8364  df-sdom 8365  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532

This theorem is referenced by:  nn0ledivnn  12357  xsubge0  12509  xmulge0  12532  0e0icopnf  12701  0e0iccpnf  12702  0elunit  12710  0mod  13125  sqlecan  13426  discr  13456  cnpart  14438  sqr0lem  14439  resqrex  14449  sqrt00  14462  fsumabs  14994  rpnnen2lem4  15408  divalglem7  15588  pcmptdvds  16064  prmreclem4  16089  prmreclem5  16090  prmreclem6  16091  ramz2  16194  ramz  16195  isabvd  19286  prdsxmetlem  22666  metustto  22851  cfilucfil  22857  nmolb2d  23015  nmoi  23025  nmoix  23026  nmoleub  23028  nmo0  23032  pcoval1  23305  pco0  23306  minveclem7  23726  ovolfiniun  23790  ovolicc1  23805  ioorf  23862  itg1ge0a  24000  mbfi1fseqlem5  24008  itg2const  24029  itg2const2  24030  itg2splitlem  24037  itg2cnlem1  24050  itg2cnlem2  24051  iblss  24093  itgle  24098  ibladdlem  24108  iblabs  24117  iblabsr  24118  iblmulc2  24119  bddmulibl  24127  c1lip1  24282  dveq0  24285  dv11cn  24286  fta1g  24449  abelthlem2  24708  sinq12ge0  24782  cxpge0  24952  abscxp2  24962  log2ublem3  25213  chtwordi  25420  ppiwordi  25426  chpub  25483  bposlem1  25547  bposlem6  25552  dchrisum0flblem2  25772  qabvle  25888  ostth2lem2  25897  colinearalg  26384  eucrct2eupthOLD  27718  eucrct2eupth  27719  ex-po  27911  nvz0  28141  nmlnoubi  28269  nmblolbii  28272  blocnilem  28277  siilem2  28325  minvecolem7  28356  pjneli  29196  nmbdoplbi  29497  nmcoplbi  29501  nmbdfnlbi  29522  nmcfnlbi  29525  nmopcoi  29568  unierri  29577  leoprf2  29600  leoprf  29601  stle0i  29712  xrge0iifcnv  30798  xrge0iifiso  30800  xrge0iifhom  30802  esumrnmpt2  30949  dstfrvclim1  31357  ballotlemrc  31410  signsply0  31443  chtvalz  31522  poimirlem23  34471  mblfinlem2  34486  itg2addnclem  34499  itg2gt0cn  34503  ibladdnclem  34504  itgaddnclem2  34507  iblabsnc  34512  iblmulc2nc  34513  bddiblnc  34518  ftc1anclem5  34527  ftc1anclem7  34529  ftc1anclem8  34530  ftc1anc  34531  areacirclem1  34538  areacirclem4  34541  mettrifi  34589  monotoddzzfi  39049  rmxypos  39054  rmygeid  39071  stoweidlem55  41908  fourierdlem14  41974  fourierdlem20  41980  fourierdlem92  42051  fourierdlem93  42052  fouriersw  42084  isomennd  42381  ovnssle  42411  hoidmvlelem3  42447  ovnhoilem1  42451  nnlog2ge0lt1  44133  dig1  44175  ex-gte  44334