Theorem 0le0 12247

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

Syntax hints:   class class class wbr 5095  0cc0 11028   ≤ cle 11169

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101  ax-pre-lttri 11102

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  nn0ledivnn  13026  xsubge0  13181  xmulge0  13204  0e0icopnf  13379  0e0iccpnf  13380  0elunit  13390  0mod  13824  sqlecan  14134  discr  14165  cnpart  15165  sqrt0  15166  resqrex  15175  sqrt00  15188  fsumabs  15726  rpnnen2lem4  16144  divalglem7  16328  pcmptdvds  16824  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  ramz2  16954  ramz  16955  isabvd  20715  prdsxmetlem  24272  metustto  24457  cfilucfil  24463  nmolb2d  24622  nmoi  24632  nmoix  24633  nmoleub  24635  nmo0  24639  pcoval1  24929  pco0  24930  minveclem7  25351  ovolfiniun  25418  ovolicc1  25433  ioorf  25490  itg1ge0a  25628  mbfi1fseqlem5  25636  itg2const  25657  itg2const2  25658  itg2splitlem  25665  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  itgle  25727  ibladdlem  25737  iblabs  25746  iblabsr  25747  iblmulc2  25748  bddmulibl  25756  bddiblnc  25759  c1lip1  25918  dveq0  25921  dv11cn  25922  fta1g  26091  abelthlem2  26358  sinq12ge0  26433  cxpge0  26608  abscxp2  26618  log2ublem3  26874  chtwordi  27082  ppiwordi  27088  chpub  27147  bposlem1  27211  bposlem6  27216  dchrisum0flblem2  27436  qabvle  27552  ostth2lem2  27561  colinearalg  28873  eucrct2eupth  30207  ex-po  30397  nvz0  30630  nmlnoubi  30758  nmblolbii  30761  blocnilem  30766  siilem2  30814  minvecolem7  30845  pjneli  31685  nmbdoplbi  31986  nmcoplbi  31990  nmbdfnlbi  32011  nmcfnlbi  32014  nmopcoi  32057  unierri  32066  leoprf2  32089  leoprf  32090  stle0i  32201  fzo0opth  32761  m1pmeq  33531  xrge0iifcnv  33902  xrge0iifiso  33904  xrge0iifhom  33906  esumrnmpt2  34037  dstfrvclim1  34448  ballotlemrc  34501  signsply0  34521  chtvalz  34599  poimirlem23  37625  mblfinlem2  37640  itg2addnclem  37653  itg2gt0cn  37657  ibladdnclem  37658  itgaddnclem2  37661  iblabsnc  37666  iblmulc2nc  37667  ftc1anclem5  37679  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  areacirclem1  37690  areacirclem4  37693  mettrifi  37739  aks6d1c1  42092  bcled  42154  bcle2d  42155  readvrec2  42337  monotoddzzfi  42918  rmxypos  42923  rmygeid  42940  stoweidlem55  46040  fourierdlem14  46106  fourierdlem20  46112  fourierdlem92  46183  fourierdlem93  46184  fouriersw  46216  isomennd  46516  ovnssle  46546  hoidmvlelem3  46582  ovnhoilem1  46586  nnlog2ge0lt1  48555  dig1  48597  sepfsepc  48916  seppcld  48918  ex-gte  49718