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

Theorem 0le1 10164
Description: 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
0le1  |-  0  <_  1

Proof of Theorem 0le1
StepHypRef Expression
1 0re 9668 . 2  |-  0  e.  RR
2 1re 9667 . 2  |-  1  e.  RR
3 0lt1 10163 . 2  |-  0  <  1
41, 2, 3ltleii 9782 1  |-  0  <_  1
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4415   0cc0 9564   1c1 9565    <_ cle 9701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-po 4773  df-so 4774  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888
This theorem is referenced by:  lemulge11  10494  0le2  10727  1eluzge0  11230  x2times  11613  0elunit  11778  1elunit  11779  1mod  12160  expge0  12339  expge1  12340  faclbnd3  12508  faclbnd4lem1  12509  hashsnlei  12624  hashgt12el  12627  hashgt12el2  12628  sqrlem1  13354  sqrt1  13383  sqrt2gt1lt2  13386  sqrtm1  13387  abs1  13408  rlimno1  13765  harmonic  13965  georeclim  13976  geoisumr  13982  geoihalfsum  13986  fprodge0  14095  fprodge1  14097  ege2le3  14192  sinbnd  14282  cosbnd  14283  cos2bnd  14290  sqnprm  14694  zsqrtelqelz  14755  modprm0  14804  pythagtriplem3  14816  prmolefac  15052  prmorlefacOLD  15066  abvneg  18110  gzrngunitlem  19080  rge0srg  19086  dscmet  21635  nmoid  21811  iccpnfcnv  22020  iccpnfhmeo  22021  xrhmeo  22022  vitalilem4  22617  vitalilem5  22618  aalioulem3  23338  dvradcnv  23424  abelth2  23445  tanregt0  23536  efif1olem3  23541  dvlog2lem  23645  cxpge0  23676  cxpaddlelem  23739  bndatandm  23903  atans2  23905  cxp2lim  23950  scvxcvx  23959  logdiflbnd  23968  fsumharmonic  23985  lgamgulmlem2  24003  lgamgulmlem3  24004  lgamgulmlem5  24006  mule1  24123  sqff1o  24157  ppiub  24180  dchrabs2  24238  lgslem2  24273  lgsfcl2  24278  lgsdir2lem1  24299  lgsne0  24309  lgsdinn0  24316  m1lgs  24338  chtppilim  24361  rpvmasumlem  24373  dchrisum0flblem1  24394  dchrisum0flblem2  24395  mulog2sumlem2  24421  pntlemb  24483  ostth3  24524  axcontlem2  25043  0pth  25348  constr3trllem3  25428  nv1  26353  nmosetn0  26454  nmoo0  26480  norm1  26950  nmopsetn0  27566  nmfnsetn0  27579  nmopge0  27612  nmfnge0  27628  nmop0  27687  nmfn0  27688  nmcexi  27727  hstle1  27927  strlem1  27951  strlem5  27956  jplem1  27969  nn0sqeq1  28372  xrsmulgzz  28488  xrge0slmod  28655  unitssxrge0  28754  xrge0iifcnv  28787  xrge0iifiso  28789  xrge0iifhom  28791  nexple  28879  ddemeas  29107  ballotlem2  29369  ballotlem4  29379  ballotlemic  29387  ballotlem1c  29388  ballotlemicOLD  29425  ballotlem1cOLD  29426  signswch  29498  signsvf0  29517  cvmliftlem13  30067  poimirlem23  32007  dvasin  32072  areacirclem1  32076  cntotbnd  32172  pell1qrge1  35760  pell1qrgaplem  35763  pell14qrgapw  35766  pellqrex  35770  pellfundgt1  35775  rmspecnonsq  35799  rmspecfund  35801  rmspecpos  35808  monotoddzzfi  35834  jm2.23  35895  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  stoweidlem1  37898  stoweidlem11  37908  stoweidlem18  37915  stoweidlem34  37932  stoweidlem38  37936  stoweidlem55  37953  wallispi2lem1  37970  stirlinglem1  37973  stirlinglem11  37983  stirlinglem13  37985  fourierdlem11  38017  fourierdlem15  38021  fourierdlem39  38046  fourierdlem41  38048  fourierdlem48  38055  fourierdlem79  38086  ovn0lem  38424  hoidmvlelem2  38455  hoidmvlelem4  38457  iccpartgt  38778  tgblthelfgott  38945  tgoldbach  38948  0ewlk  39827  0pth-av  39840  nn0eo  40607
  Copyright terms: Public domain W3C validator