Theorem 0le0 12246

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

Syntax hints:   class class class wbr 5098  0cc0 11026   ≤ cle 11167

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099  ax-pre-lttri 11100

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  nn0ledivnn  13020  xsubge0  13176  xmulge0  13199  0e0icopnf  13374  0e0iccpnf  13375  0elunit  13385  0mod  13822  sqlecan  14132  discr  14163  cnpart  15163  sqrt0  15164  resqrex  15173  sqrt00  15186  fsumabs  15724  rpnnen2lem4  16142  divalglem7  16326  pcmptdvds  16822  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  ramz2  16952  ramz  16953  isabvd  20745  prdsxmetlem  24312  metustto  24497  cfilucfil  24503  nmolb2d  24662  nmoi  24672  nmoix  24673  nmoleub  24675  nmo0  24679  pcoval1  24969  pco0  24970  minveclem7  25391  ovolfiniun  25458  ovolicc1  25473  ioorf  25530  itg1ge0a  25668  mbfi1fseqlem5  25676  itg2const  25697  itg2const2  25698  itg2splitlem  25705  itg2cnlem1  25718  itg2cnlem2  25719  iblss  25762  itgle  25767  ibladdlem  25777  iblabs  25786  iblabsr  25787  iblmulc2  25788  bddmulibl  25796  bddiblnc  25799  c1lip1  25958  dveq0  25961  dv11cn  25962  fta1g  26131  abelthlem2  26398  sinq12ge0  26473  cxpge0  26648  abscxp2  26658  log2ublem3  26914  chtwordi  27122  ppiwordi  27128  chpub  27187  bposlem1  27251  bposlem6  27256  dchrisum0flblem2  27476  qabvle  27592  ostth2lem2  27601  colinearalg  28983  eucrct2eupth  30320  ex-po  30510  nvz0  30743  nmlnoubi  30871  nmblolbii  30874  blocnilem  30879  siilem2  30927  minvecolem7  30958  pjneli  31798  nmbdoplbi  32099  nmcoplbi  32103  nmbdfnlbi  32124  nmcfnlbi  32127  nmopcoi  32170  unierri  32179  leoprf2  32202  leoprf  32203  stle0i  32314  fzo0opth  32883  m1pmeq  33666  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  esumrnmpt2  34225  dstfrvclim1  34635  ballotlemrc  34688  signsply0  34708  chtvalz  34786  poimirlem23  37844  mblfinlem2  37859  itg2addnclem  37872  itg2gt0cn  37876  ibladdnclem  37877  itgaddnclem2  37880  iblabsnc  37885  iblmulc2nc  37886  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  areacirclem1  37909  areacirclem4  37912  mettrifi  37958  aks6d1c1  42370  bcled  42432  bcle2d  42433  readvrec2  42616  monotoddzzfi  43184  rmxypos  43189  rmygeid  43206  stoweidlem55  46299  fourierdlem14  46365  fourierdlem20  46371  fourierdlem92  46442  fourierdlem93  46443  fouriersw  46475  isomennd  46775  ovnssle  46805  hoidmvlelem3  46841  ovnhoilem1  46845  chnsubseqwl  47123  nnlog2ge0lt1  48812  dig1  48854  sepfsepc  49173  seppcld  49175  ex-gte  49974