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

Theorem 0le0 10621
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 9585 . 2  |-  0  e.  RR
21leidi 10083 1  |-  0  <_  0
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4439   0cc0 9481    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623
This theorem is referenced by:  xsubge0  11456  xmulge0  11479  0e0icopnf  11633  0e0iccpnf  11634  0elunit  11641  0mod  12009  sqlecan  12256  discr  12285  hashle00  12449  cnpart  13155  sqr0lem  13156  resqrex  13166  sqrt00  13179  fsumabs  13697  rpnnen2lem4  14035  divalglem7  14141  pcmptdvds  14497  prmreclem4  14521  prmreclem5  14522  prmreclem6  14523  ramz2  14626  ramz  14627  isabvd  17664  prdsxmetlem  21037  metusttoOLD  21226  metustto  21227  cfilucfilOLD  21238  cfilucfil  21239  nmolb2d  21391  nmoi  21401  nmoix  21402  nmoleub  21404  nmo0  21408  pcoval1  21679  pco0  21680  minveclem7  22016  ovolfiniun  22078  ovolicc1  22093  ioorf  22148  itg1ge0a  22284  mbfi1fseqlem5  22292  itg2const  22313  itg2const2  22314  itg2splitlem  22321  itg2cnlem1  22334  itg2cnlem2  22335  iblss  22377  itgle  22382  ibladdlem  22392  iblabs  22401  iblabsr  22402  iblmulc2  22403  bddmulibl  22411  c1lip1  22564  dveq0  22567  dv11cn  22568  fta1g  22734  abelthlem2  22993  sinq12ge0  23067  cxpge0  23232  abscxp2  23242  log2ublem3  23476  chtwordi  23628  ppiwordi  23634  chpub  23693  bposlem1  23757  bposlem6  23762  dchrisum0flblem2  23892  qabvle  24008  ostth2lem2  24017  colinearalg  24415  ex-po  25358  nvz0  25769  nmlnoubi  25909  nmblolbii  25912  blocnilem  25917  siilem2  25965  minvecolem7  25997  pjneli  26839  nmbdoplbi  27141  nmcoplbi  27145  nmbdfnlbi  27166  nmcfnlbi  27169  nmopcoi  27212  unierri  27221  leoprf2  27244  leoprf  27245  stle0i  27356  xrge0iifcnv  28150  xrge0iifiso  28152  xrge0iifhom  28154  esumrnmpt2  28297  dstfrvclim1  28680  ballotlemrc  28733  signsply0  28772  mblfinlem2  30292  itg2addnclem  30306  itg2gt0cn  30310  ibladdnclem  30311  itgaddnclem2  30314  iblabsnc  30319  iblmulc2nc  30320  bddiblnc  30325  ftc1anclem5  30334  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  areacirclem1  30347  areacirclem4  30350  mettrifi  30490  monotoddzzfi  31117  rmxypos  31124  rmygeid  31141  stoweidlem55  32076  fourierdlem14  32142  fourierdlem20  32148  fourierdlem92  32220  fourierdlem93  32221  fouriersw  32253  nnlog2ge0lt1  33441  dig1  33483  ex-gte  33513
  Copyright terms: Public domain W3C validator