Theorem 0le0 12226

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

Syntax hints:   class class class wbr 5091  0cc0 11006   ≤ cle 11147

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079  ax-pre-lttri 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  nn0ledivnn  13005  xsubge0  13160  xmulge0  13183  0e0icopnf  13358  0e0iccpnf  13359  0elunit  13369  0mod  13806  sqlecan  14116  discr  14147  cnpart  15147  sqrt0  15148  resqrex  15157  sqrt00  15170  fsumabs  15708  rpnnen2lem4  16126  divalglem7  16310  pcmptdvds  16806  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  ramz2  16936  ramz  16937  isabvd  20728  prdsxmetlem  24284  metustto  24469  cfilucfil  24475  nmolb2d  24634  nmoi  24644  nmoix  24645  nmoleub  24647  nmo0  24651  pcoval1  24941  pco0  24942  minveclem7  25363  ovolfiniun  25430  ovolicc1  25445  ioorf  25502  itg1ge0a  25640  mbfi1fseqlem5  25648  itg2const  25669  itg2const2  25670  itg2splitlem  25677  itg2cnlem1  25690  itg2cnlem2  25691  iblss  25734  itgle  25739  ibladdlem  25749  iblabs  25758  iblabsr  25759  iblmulc2  25760  bddmulibl  25768  bddiblnc  25771  c1lip1  25930  dveq0  25933  dv11cn  25934  fta1g  26103  abelthlem2  26370  sinq12ge0  26445  cxpge0  26620  abscxp2  26630  log2ublem3  26886  chtwordi  27094  ppiwordi  27100  chpub  27159  bposlem1  27223  bposlem6  27228  dchrisum0flblem2  27448  qabvle  27564  ostth2lem2  27573  colinearalg  28889  eucrct2eupth  30223  ex-po  30413  nvz0  30646  nmlnoubi  30774  nmblolbii  30777  blocnilem  30782  siilem2  30830  minvecolem7  30861  pjneli  31701  nmbdoplbi  32002  nmcoplbi  32006  nmbdfnlbi  32027  nmcfnlbi  32030  nmopcoi  32073  unierri  32082  leoprf2  32105  leoprf  32106  stle0i  32217  fzo0opth  32783  m1pmeq  33545  xrge0iifcnv  33944  xrge0iifiso  33946  xrge0iifhom  33948  esumrnmpt2  34079  dstfrvclim1  34489  ballotlemrc  34542  signsply0  34562  chtvalz  34640  poimirlem23  37689  mblfinlem2  37704  itg2addnclem  37717  itg2gt0cn  37721  ibladdnclem  37722  itgaddnclem2  37725  iblabsnc  37730  iblmulc2nc  37731  ftc1anclem5  37743  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  areacirclem1  37754  areacirclem4  37757  mettrifi  37803  aks6d1c1  42155  bcled  42217  bcle2d  42218  readvrec2  42400  monotoddzzfi  42981  rmxypos  42986  rmygeid  43003  stoweidlem55  46099  fourierdlem14  46165  fourierdlem20  46171  fourierdlem92  46242  fourierdlem93  46243  fouriersw  46275  isomennd  46575  ovnssle  46605  hoidmvlelem3  46641  ovnhoilem1  46645  nnlog2ge0lt1  48604  dig1  48646  sepfsepc  48965  seppcld  48967  ex-gte  49767