MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0le0 Structured version   Unicode version

Theorem 0le0 10631
Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0le0  |-  0  <_  0

Proof of Theorem 0le0
StepHypRef Expression
1 0re 9599 . 2  |-  0  e.  RR
21leidi 10093 1  |-  0  <_  0
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4437   0cc0 9495    <_ cle 9632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637
This theorem is referenced by:  xsubge0  11462  xmulge0  11485  0e0icopnf  11639  0e0iccpnf  11640  0elunit  11647  0mod  12006  sqlecan  12253  discr  12282  hashle00  12444  cnpart  13052  sqr0lem  13053  resqrex  13063  sqrt00  13076  fsumabs  13594  rpnnen2lem4  13828  divalglem7  13934  pcmptdvds  14290  prmreclem4  14314  prmreclem5  14315  prmreclem6  14316  ramz2  14419  ramz  14420  isabvd  17343  prdsxmetlem  20744  metusttoOLD  20933  metustto  20934  cfilucfilOLD  20945  cfilucfil  20946  nmolb2d  21098  nmoi  21108  nmoix  21109  nmoleub  21111  nmo0  21115  pcoval1  21386  pco0  21387  minveclem7  21723  ovolfiniun  21785  ovolicc1  21800  ioorf  21855  itg1ge0a  21991  mbfi1fseqlem5  21999  itg2const  22020  itg2const2  22021  itg2splitlem  22028  itg2cnlem1  22041  itg2cnlem2  22042  iblss  22084  itgle  22089  ibladdlem  22099  iblabs  22108  iblabsr  22109  iblmulc2  22110  bddmulibl  22118  c1lip1  22271  dveq0  22274  dv11cn  22275  fta1g  22441  abelthlem2  22699  sinq12ge0  22773  cxpge0  22936  abscxp2  22946  log2ublem3  23151  chtwordi  23302  ppiwordi  23308  chpub  23367  bposlem1  23431  bposlem6  23436  dchrisum0flblem2  23566  qabvle  23682  ostth2lem2  23691  colinearalg  24085  ex-po  25028  nvz0  25443  nmlnoubi  25583  nmblolbii  25586  blocnilem  25591  siilem2  25639  minvecolem7  25671  pjneli  26513  nmbdoplbi  26815  nmcoplbi  26819  nmbdfnlbi  26840  nmcfnlbi  26843  nmopcoi  26886  unierri  26895  leoprf2  26918  leoprf  26919  stle0i  27030  xrge0iifcnv  27788  xrge0iifiso  27790  xrge0iifhom  27792  dstfrvclim1  28289  ballotlemrc  28342  signsply0  28381  mblfinlem2  30027  itg2addnclem  30041  itg2gt0cn  30045  ibladdnclem  30046  itgaddnclem2  30049  iblabsnc  30054  iblmulc2nc  30055  bddiblnc  30060  ftc1anclem5  30069  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  areacirclem1  30082  areacirclem4  30085  mettrifi  30225  monotoddzzfi  30853  rmxypos  30860  rmygeid  30877  stoweidlem55  31726  fourierdlem14  31792  fourierdlem20  31798  fourierdlem92  31870  fourierdlem93  31871  fouriersw  31903  ex-gte  32858
  Copyright terms: Public domain W3C validator