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

Syntax hints:   class class class wbr 5086  0cc0 11027   ≤ cle 11168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-addrcl 11088  ax-rnegex 11098  ax-cnre 11100  ax-pre-lttri 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173

This theorem is referenced by:  nn0ledivnn  13021  xsubge0  13177  xmulge0  13200  0e0icopnf  13375  0e0iccpnf  13376  0elunit  13386  0mod  13823  sqlecan  14133  discr  14164  cnpart  15164  sqrt0  15165  resqrex  15174  sqrt00  15187  fsumabs  15725  rpnnen2lem4  16143  divalglem7  16327  pcmptdvds  16823  prmreclem4  16848  prmreclem5  16849  prmreclem6  16850  ramz2  16953  ramz  16954  isabvd  20747  prdsxmetlem  24311  metustto  24496  cfilucfil  24502  nmolb2d  24661  nmoi  24671  nmoix  24672  nmoleub  24674  nmo0  24678  pcoval1  24958  pco0  24959  minveclem7  25380  ovolfiniun  25446  ovolicc1  25461  ioorf  25518  itg1ge0a  25656  mbfi1fseqlem5  25664  itg2const  25685  itg2const2  25686  itg2splitlem  25693  itg2cnlem1  25706  itg2cnlem2  25707  iblss  25750  itgle  25755  ibladdlem  25765  iblabs  25774  iblabsr  25775  iblmulc2  25776  bddmulibl  25784  bddiblnc  25787  c1lip1  25943  dveq0  25946  dv11cn  25947  fta1g  26116  abelthlem2  26382  sinq12ge0  26457  cxpge0  26632  abscxp2  26642  log2ublem3  26898  chtwordi  27106  ppiwordi  27112  chpub  27171  bposlem1  27235  bposlem6  27240  dchrisum0flblem2  27460  qabvle  27576  ostth2lem2  27585  colinearalg  28967  eucrct2eupth  30304  ex-po  30494  nvz0  30728  nmlnoubi  30856  nmblolbii  30859  blocnilem  30864  siilem2  30912  minvecolem7  30943  pjneli  31783  nmbdoplbi  32084  nmcoplbi  32088  nmbdfnlbi  32109  nmcfnlbi  32112  nmopcoi  32155  unierri  32164  leoprf2  32187  leoprf  32188  stle0i  32299  fzo0opth  32866  m1pmeq  33650  xrge0iifcnv  34083  xrge0iifiso  34085  xrge0iifhom  34087  esumrnmpt2  34218  dstfrvclim1  34628  ballotlemrc  34681  signsply0  34701  chtvalz  34779  poimirlem23  37955  mblfinlem2  37970  itg2addnclem  37983  itg2gt0cn  37987  ibladdnclem  37988  itgaddnclem2  37991  iblabsnc  37996  iblmulc2nc  37997  ftc1anclem5  38009  ftc1anclem7  38011  ftc1anclem8  38012  ftc1anc  38013  areacirclem1  38020  areacirclem4  38023  mettrifi  38069  aks6d1c1  42547  bcled  42609  bcle2d  42610  readvrec2  42792  monotoddzzfi  43373  rmxypos  43378  rmygeid  43395  stoweidlem55  46487  fourierdlem14  46553  fourierdlem20  46559  fourierdlem92  46630  fourierdlem93  46631  fouriersw  46663  isomennd  46963  ovnssle  46993  hoidmvlelem3  47029  ovnhoilem1  47033  chnsubseqwl  47311  nnlog2ge0lt1  49000  dig1  49042  sepfsepc  49361  seppcld  49363  ex-gte  50162