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

Theorem 0le1 9553
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 9093 . 2  |-  0  e.  RR
2 1re 9092 . 2  |-  1  e.  RR
3 0lt1 9552 . 2  |-  0  <  1
41, 2, 3ltleii 9198 1  |-  0  <_  1
Colors of variables: wff set class
Syntax hints:   class class class wbr 4214   0cc0 8992   1c1 8993    <_ cle 9123
This theorem is referenced by:  lemulge11  9874  x2times  10880  0elunit  11017  1elunit  11018  injresinj  11202  1mod  11275  expge0  11418  expge1  11419  faclbnd3  11585  faclbnd4lem1  11586  hashsnlei  11682  hashgt12el  11684  hashgt12el2  11685  sqrlem1  12050  sqr1  12079  sqr2gt1lt2  12082  sqrm1  12083  abs1  12104  rlimno1  12449  harmonic  12640  georeclim  12651  geoisumr  12657  geoihalfsum  12661  ege2le3  12694  sinbnd  12783  cosbnd  12784  cos2bnd  12791  sqnprm  13100  zsqrelqelz  13152  pythagtriplem3  13194  abvneg  15924  gzrngunitlem  16765  dscmet  18622  nmoid  18778  iccpnfcnv  18971  iccpnfhmeo  18972  xrhmeo  18973  vitalilem4  19505  vitalilem5  19506  aalioulem3  20253  dvradcnv  20339  abelth2  20360  tanregt0  20443  efif1olem3  20448  dvlog2lem  20545  cxpge0  20576  cxpaddlelem  20637  bndatandm  20771  atans2  20773  cxp2lim  20817  scvxcvx  20826  logdiflbnd  20835  fsumharmonic  20852  mule1  20933  sqff1o  20967  ppiub  20990  dchrabs2  21048  lgslem2  21083  lgsfcl2  21088  lgsdir2lem1  21109  lgsne0  21119  lgsdinn0  21126  m1lgs  21148  chtppilim  21171  rpvmasumlem  21183  dchrisum0flblem1  21204  dchrisum0flblem2  21205  mulog2sumlem2  21231  pntlemb  21293  ostth3  21334  0pth  21572  constr3trllem3  21641  nv1  22167  nmosetn0  22268  nmoo0  22294  norm1  22753  nmopsetn0  23370  nmfnsetn0  23383  nmopge0  23416  nmfnge0  23432  nmop0  23491  nmfn0  23492  nmcexi  23531  hstle1  23731  strlem1  23755  strlem5  23760  jplem1  23773  xrsmulgzz  24202  unitssxrge0  24300  xrge0iifcnv  24321  xrge0iifiso  24323  xrge0iifhom  24325  ballotlem2  24748  ballotlemfc0  24752  ballotlemfcc  24753  ballotlem4  24758  ballotlemic  24766  ballotlem1c  24767  lgamgulmlem2  24816  lgamgulmlem3  24817  lgamgulmlem5  24819  cvmliftlem13  24985  axcontlem2  25906  dvreasin  26292  areacirclem1  26294  cntotbnd  26507  pell1qrge1  26935  pell1qrgaplem  26938  pell14qrgapw  26941  pellqrex  26944  pellfundgt1  26948  rmspecnonsq  26972  rmspecfund  26974  rmspecpos  26981  monotoddzzfi  27007  jm2.23  27069  stoweidlem1  27728  stoweidlem11  27738  stoweidlem18  27745  stoweidlem34  27761  stoweidlem38  27765  stoweidlem55  27782  wallispi2lem1  27798  stirlinglem1  27801  stirlinglem11  27811  stirlinglem13  27813  1eluzge0  28102  modprm0  28230
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-po 4505  df-so 4506  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-riota 6551  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296
  Copyright terms: Public domain W3C validator