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

Theorem 0le0 9823
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 8834 . 2  |-  0  e.  RR
21leidi 9303 1  |-  0  <_  0
Colors of variables: wff set class
Syntax hints:   class class class wbr 4025   0cc0 8733    <_ cle 8864
This theorem is referenced by:  xsubge0  10576  xmulge0  10599  0elunit  10749  0mod  10990  sqlecan  11204  discr  11233  cnpart  11720  sqr0lem  11721  resqrex  11731  sqr00  11744  fsumge0  12248  fsumabs  12254  rpnnen2lem4  12491  divalglem7  12593  pcmptdvds  12937  prmreclem4  12961  prmreclem5  12962  prmreclem6  12963  ramz2  13066  ramz  13067  isabvd  15580  xrge0subm  16407  rege0subm  16423  prdsxmetlem  17927  nmolb2d  18222  nmoi  18232  nmoix  18233  nmoleub  18235  nmo0  18239  pcoval1  18506  pco0  18507  minveclem7  18794  ovolfiniun  18855  ovolicc1  18870  ioorf  18923  itg1ge0a  19061  mbfi1fseqlem5  19069  itg2const  19090  itg2const2  19091  itg2splitlem  19098  itg2split  19099  itg2gt0  19110  itg2cnlem1  19111  itg2cnlem2  19112  itg2cn  19113  iblss  19154  itgle  19159  itgeqa  19163  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2lem1  19181  bddmulibl  19188  itggt0  19191  itgcn  19192  c1lip1  19339  dveq0  19342  dv11cn  19343  fta1g  19548  abelthlem2  19803  sinq12ge0  19871  cxpge0  20025  abscxp2  20035  cxpcn3  20083  log2ublem3  20239  efrlim  20259  chtwordi  20389  ppiwordi  20395  chpub  20454  bposlem1  20518  bposlem6  20523  dchrisum0flblem2  20653  qabvle  20769  ostth2lem2  20778  ex-po  20798  nvz0  21227  nmlnoubi  21367  nmblolbii  21370  blocnilem  21375  siilem2  21423  minvecolem7  21455  pjneli  22295  nmbdoplbi  22597  nmcoplbi  22601  nmbdfnlbi  22622  nmcfnlbi  22625  nmopcoi  22668  unierri  22677  leoprf2  22700  leoprf  22701  stle0i  22812  ballotlemrc  23083  colinearalg  23946  mettrifi  25873  monotoddzzfi  26427  rmxypos  26434  rmygeid  26451  ex-gte  27460
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-i2m1 8801  ax-1ne0 8802  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-ov 5823  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869
  Copyright terms: Public domain W3C validator