Theorem 0le0 12294

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

Syntax hints:   class class class wbr 5110  0cc0 11075   ≤ cle 11216

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148  ax-pre-lttri 11149

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  nn0ledivnn  13073  xsubge0  13228  xmulge0  13251  0e0icopnf  13426  0e0iccpnf  13427  0elunit  13437  0mod  13871  sqlecan  14181  discr  14212  cnpart  15213  sqrt0  15214  resqrex  15223  sqrt00  15236  fsumabs  15774  rpnnen2lem4  16192  divalglem7  16376  pcmptdvds  16872  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  ramz2  17002  ramz  17003  isabvd  20728  prdsxmetlem  24263  metustto  24448  cfilucfil  24454  nmolb2d  24613  nmoi  24623  nmoix  24624  nmoleub  24626  nmo0  24630  pcoval1  24920  pco0  24921  minveclem7  25342  ovolfiniun  25409  ovolicc1  25424  ioorf  25481  itg1ge0a  25619  mbfi1fseqlem5  25627  itg2const  25648  itg2const2  25649  itg2splitlem  25656  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  itgle  25718  ibladdlem  25728  iblabs  25737  iblabsr  25738  iblmulc2  25739  bddmulibl  25747  bddiblnc  25750  c1lip1  25909  dveq0  25912  dv11cn  25913  fta1g  26082  abelthlem2  26349  sinq12ge0  26424  cxpge0  26599  abscxp2  26609  log2ublem3  26865  chtwordi  27073  ppiwordi  27079  chpub  27138  bposlem1  27202  bposlem6  27207  dchrisum0flblem2  27427  qabvle  27543  ostth2lem2  27552  colinearalg  28844  eucrct2eupth  30181  ex-po  30371  nvz0  30604  nmlnoubi  30732  nmblolbii  30735  blocnilem  30740  siilem2  30788  minvecolem7  30819  pjneli  31659  nmbdoplbi  31960  nmcoplbi  31964  nmbdfnlbi  31985  nmcfnlbi  31988  nmopcoi  32031  unierri  32040  leoprf2  32063  leoprf  32064  stle0i  32175  fzo0opth  32735  m1pmeq  33559  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  esumrnmpt2  34065  dstfrvclim1  34476  ballotlemrc  34529  signsply0  34549  chtvalz  34627  poimirlem23  37644  mblfinlem2  37659  itg2addnclem  37672  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem2  37680  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirclem1  37709  areacirclem4  37712  mettrifi  37758  aks6d1c1  42111  bcled  42173  bcle2d  42174  readvrec2  42356  monotoddzzfi  42938  rmxypos  42943  rmygeid  42960  stoweidlem55  46060  fourierdlem14  46126  fourierdlem20  46132  fourierdlem92  46203  fourierdlem93  46204  fouriersw  46236  isomennd  46536  ovnssle  46566  hoidmvlelem3  46602  ovnhoilem1  46606  nnlog2ge0lt1  48559  dig1  48601  sepfsepc  48920  seppcld  48922  ex-gte  49722