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

Theorem 0le0 10687
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 9629 . 2  |-  0  e.  RR
21leidi 10136 1  |-  0  <_  0
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4373   0cc0 9525    <_ cle 9662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-i2m1 9593  ax-1ne0 9594  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667
This theorem is referenced by:  xsubge0  11536  xmulge0  11559  0e0icopnf  11732  0e0iccpnf  11733  0elunit  11740  0mod  12121  sqlecan  12374  discr  12402  hashle00  12570  cnpart  13313  sqr0lem  13314  resqrex  13324  sqrt00  13337  fsumabs  13871  rpnnen2lem4  14280  divalglem7  14389  pcmptdvds  14849  prmreclem4  14873  prmreclem5  14874  prmreclem6  14875  ramz2  14992  ramz  14993  isabvd  18058  prdsxmetlem  21393  metustto  21578  cfilucfil  21584  nmolb2d  21733  nmoi  21743  nmoix  21744  nmoleub  21746  nmoiOLD  21759  nmoixOLD  21760  nmoleubOLD  21762  nmo0  21766  pcoval1  22054  pco0  22055  minveclem7  22387  minveclem7OLD  22399  ovolfiniun  22464  ovolicc1  22479  ioorf  22536  ioorfOLD  22541  itg1ge0a  22680  mbfi1fseqlem5  22688  itg2const  22709  itg2const2  22710  itg2splitlem  22717  itg2cnlem1  22730  itg2cnlem2  22731  iblss  22773  itgle  22778  ibladdlem  22788  iblabs  22797  iblabsr  22798  iblmulc2  22799  bddmulibl  22807  c1lip1  22960  dveq0  22963  dv11cn  22964  fta1g  23129  abelthlem2  23398  sinq12ge0  23474  cxpge0  23639  abscxp2  23649  log2ublem3  23885  chtwordi  24094  ppiwordi  24100  chpub  24159  bposlem1  24223  bposlem6  24228  dchrisum0flblem2  24358  qabvle  24474  ostth2lem2  24483  colinearalg  24951  ex-po  25896  nvz0  26308  nmlnoubi  26448  nmblolbii  26451  blocnilem  26456  siilem2  26504  minvecolem7  26536  minvecolem7OLD  26546  pjneli  27387  nmbdoplbi  27688  nmcoplbi  27692  nmbdfnlbi  27713  nmcfnlbi  27716  nmopcoi  27759  unierri  27768  leoprf2  27791  leoprf  27792  stle0i  27903  xrge0iifcnv  28745  xrge0iifiso  28747  xrge0iifhom  28749  esumrnmpt2  28895  dstfrvclim1  29315  ballotlemrc  29368  ballotlemrcOLD  29406  signsply0  29445  poimirlem23  31964  mblfinlem2  31979  itg2addnclem  31994  itg2gt0cn  31998  ibladdnclem  31999  itgaddnclem2  32002  iblabsnc  32007  iblmulc2nc  32008  bddiblnc  32013  ftc1anclem5  32022  ftc1anclem7  32024  ftc1anclem8  32025  ftc1anc  32026  areacirclem1  32033  areacirclem4  32036  mettrifi  32087  monotoddzzfi  35791  rmxypos  35798  rmygeid  35815  stoweidlem55  37972  fourierdlem14  38039  fourierdlem20  38045  fourierdlem92  38118  fourierdlem93  38119  fouriersw  38151  isomennd  38415  ovnssle  38445  hoidmvlelem3  38481  ovnhoilem1  38485  nnlog2ge0lt1  40701  dig1  40743  ex-gte  40773
  Copyright terms: Public domain W3C validator