Theorem 0le0 12338

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

Syntax hints:   class class class wbr 5110  0cc0 11096   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-addrcl 11157  ax-rnegex 11167  ax-cnre 11169  ax-pre-lttri 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  nn0ledivnn  13127  xsubge0  13283  xmulge0  13306  0e0icopnf  13481  0e0iccpnf  13482  0elunit  13492  0mod  13931  sqlecan  14241  discr  14272  cnpart  15287  sqrt0  15288  resqrex  15297  sqrt00  15310  fsumabs  15849  rpnnen2lem4  16269  divalglem7  16453  pcmptdvds  16950  prmreclem4  16975  prmreclem5  16976  prmreclem6  16977  ramz2  17080  ramz  17081  isabvd  20889  prdsxmetlem  24490  metustto  24675  cfilucfil  24681  nmolb2d  24840  nmoi  24850  nmoix  24851  nmoleub  24853  nmo0  24857  pcoval1  25137  pco0  25138  minveclem7  25559  ovolfiniun  25625  ovolicc1  25640  ioorf  25697  itg1ge0a  25835  mbfi1fseqlem5  25843  itg2const  25864  itg2const2  25865  itg2splitlem  25872  itg2cnlem1  25885  itg2cnlem2  25886  iblss  25929  itgle  25934  ibladdlem  25944  iblabs  25953  iblabsr  25954  iblmulc2  25955  bddmulibl  25963  bddiblnc  25966  c1lip1  26121  dveq0  26124  dv11cn  26125  fta1g  26292  abelthlem2  26557  sinq12ge0  26635  cxpge0  26810  abscxp2  26820  log2ublem3  27075  chtwordi  27282  ppiwordi  27288  chpub  27346  bposlem1  27410  bposlem6  27415  dchrisum0flblem2  27635  qabvle  27751  ostth2lem2  27760  colinearalg  29197  eucrct2eupth  30533  ex-po  30723  nvz0  30957  nmlnoubi  31085  nmblolbii  31088  blocnilem  31093  siilem2  31141  minvecolem7  31172  pjneli  32012  nmbdoplbi  32313  nmcoplbi  32317  nmbdfnlbi  32338  nmcfnlbi  32341  nmopcoi  32384  unierri  32393  leoprf2  32416  leoprf  32417  stle0i  32528  fzo0opth  33085  m1pmeq  33816  xrge0iifcnv  34264  xrge0iifiso  34266  xrge0iifhom  34268  esumrnmpt2  34399  dstfrvclim1  34809  ballotlemrc  34862  signsply0  34879  chtvalz  34957  poimirlem23  38177  mblfinlem2  38192  itg2addnclem  38205  itg2gt0cn  38209  ibladdnclem  38210  itgaddnclem2  38213  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem5  38231  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  areacirclem1  38242  areacirclem4  38245  mettrifi  38291  aks6d1c1  42768  bcled  42830  bcle2d  42831  readvrec2  43005  monotoddzzfi  43554  rmxypos  43559  rmygeid  43576  stoweidlem55  46654  fourierdlem14  46720  fourierdlem20  46726  fourierdlem92  46797  fourierdlem93  46798  fouriersw  46830  isomennd  47130  ovnssle  47160  hoidmvlelem3  47196  ovnhoilem1  47200  chnsubseqwl  47480  nnlog2ge0lt1  49224  dig1  49266  sepfsepc  49584  seppcld  49586  ex-gte  50385