Theorem 0le0 12367

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

Syntax hints:   class class class wbr 5143  0cc0 11155   ≤ cle 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-addrcl 11216  ax-rnegex 11226  ax-cnre 11228  ax-pre-lttri 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  nn0ledivnn  13148  xsubge0  13303  xmulge0  13326  0e0icopnf  13498  0e0iccpnf  13499  0elunit  13509  0mod  13942  sqlecan  14248  discr  14279  cnpart  15279  sqrt0  15280  resqrex  15289  sqrt00  15302  fsumabs  15837  rpnnen2lem4  16253  divalglem7  16436  pcmptdvds  16932  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  ramz2  17062  ramz  17063  isabvd  20813  prdsxmetlem  24378  metustto  24566  cfilucfil  24572  nmolb2d  24739  nmoi  24749  nmoix  24750  nmoleub  24752  nmo0  24756  pcoval1  25046  pco0  25047  minveclem7  25469  ovolfiniun  25536  ovolicc1  25551  ioorf  25608  itg1ge0a  25746  mbfi1fseqlem5  25754  itg2const  25775  itg2const2  25776  itg2splitlem  25783  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  itgle  25845  ibladdlem  25855  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddmulibl  25874  bddiblnc  25877  c1lip1  26036  dveq0  26039  dv11cn  26040  fta1g  26209  abelthlem2  26476  sinq12ge0  26550  cxpge0  26725  abscxp2  26735  log2ublem3  26991  chtwordi  27199  ppiwordi  27205  chpub  27264  bposlem1  27328  bposlem6  27333  dchrisum0flblem2  27553  qabvle  27669  ostth2lem2  27678  colinearalg  28925  eucrct2eupth  30264  ex-po  30454  nvz0  30687  nmlnoubi  30815  nmblolbii  30818  blocnilem  30823  siilem2  30871  minvecolem7  30902  pjneli  31742  nmbdoplbi  32043  nmcoplbi  32047  nmbdfnlbi  32068  nmcfnlbi  32071  nmopcoi  32114  unierri  32123  leoprf2  32146  leoprf  32147  stle0i  32258  fzo0opth  32807  m1pmeq  33608  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  esumrnmpt2  34069  dstfrvclim1  34480  ballotlemrc  34533  signsply0  34566  chtvalz  34644  poimirlem23  37650  mblfinlem2  37665  itg2addnclem  37678  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem2  37686  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirclem1  37715  areacirclem4  37718  mettrifi  37764  aks6d1c1  42117  bcled  42179  bcle2d  42180  readvrec2  42391  monotoddzzfi  42954  rmxypos  42959  rmygeid  42976  stoweidlem55  46070  fourierdlem14  46136  fourierdlem20  46142  fourierdlem92  46213  fourierdlem93  46214  fouriersw  46246  isomennd  46546  ovnssle  46576  hoidmvlelem3  46612  ovnhoilem1  46616  nnlog2ge0lt1  48487  dig1  48529  sepfsepc  48825  seppcld  48827  ex-gte  49248