Theorem 0le0 12287

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

Syntax hints:   class class class wbr 5107  0cc0 11068   ≤ cle 11209

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141  ax-pre-lttri 11142

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  nn0ledivnn  13066  xsubge0  13221  xmulge0  13244  0e0icopnf  13419  0e0iccpnf  13420  0elunit  13430  0mod  13864  sqlecan  14174  discr  14205  cnpart  15206  sqrt0  15207  resqrex  15216  sqrt00  15229  fsumabs  15767  rpnnen2lem4  16185  divalglem7  16369  pcmptdvds  16865  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  ramz2  16995  ramz  16996  isabvd  20721  prdsxmetlem  24256  metustto  24441  cfilucfil  24447  nmolb2d  24606  nmoi  24616  nmoix  24617  nmoleub  24619  nmo0  24623  pcoval1  24913  pco0  24914  minveclem7  25335  ovolfiniun  25402  ovolicc1  25417  ioorf  25474  itg1ge0a  25612  mbfi1fseqlem5  25620  itg2const  25641  itg2const2  25642  itg2splitlem  25649  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  itgle  25711  ibladdlem  25721  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddmulibl  25740  bddiblnc  25743  c1lip1  25902  dveq0  25905  dv11cn  25906  fta1g  26075  abelthlem2  26342  sinq12ge0  26417  cxpge0  26592  abscxp2  26602  log2ublem3  26858  chtwordi  27066  ppiwordi  27072  chpub  27131  bposlem1  27195  bposlem6  27200  dchrisum0flblem2  27420  qabvle  27536  ostth2lem2  27545  colinearalg  28837  eucrct2eupth  30174  ex-po  30364  nvz0  30597  nmlnoubi  30725  nmblolbii  30728  blocnilem  30733  siilem2  30781  minvecolem7  30812  pjneli  31652  nmbdoplbi  31953  nmcoplbi  31957  nmbdfnlbi  31978  nmcfnlbi  31981  nmopcoi  32024  unierri  32033  leoprf2  32056  leoprf  32057  stle0i  32168  fzo0opth  32728  m1pmeq  33552  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  esumrnmpt2  34058  dstfrvclim1  34469  ballotlemrc  34522  signsply0  34542  chtvalz  34620  poimirlem23  37637  mblfinlem2  37652  itg2addnclem  37665  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem2  37673  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem1  37702  areacirclem4  37705  mettrifi  37751  aks6d1c1  42104  bcled  42166  bcle2d  42167  readvrec2  42349  monotoddzzfi  42931  rmxypos  42936  rmygeid  42953  stoweidlem55  46053  fourierdlem14  46119  fourierdlem20  46125  fourierdlem92  46196  fourierdlem93  46197  fouriersw  46229  isomennd  46529  ovnssle  46559  hoidmvlelem3  46595  ovnhoilem1  46599  nnlog2ge0lt1  48555  dig1  48597  sepfsepc  48916  seppcld  48918  ex-gte  49718