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

Theorem 0le1 10809
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 10299 . 2 0 ∈ ℝ
2 1re 10297 . 2 1 ∈ ℝ
3 0lt1 10808 . 2 0 < 1
41, 2, 3ltleii 10418 1 0 ≤ 1
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4811  0cc0 10193  1c1 10194  cle 10333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-po 5200  df-so 5201  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-er 7951  df-en 8165  df-dom 8166  df-sdom 8167  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527
This theorem is referenced by:  lemulge11  11143  0le2  11385  1eluzge0  11937  x2times  12336  0elunit  12500  1elunit  12501  fldiv4p1lem1div2  12849  1mod  12915  expge0  13108  expge1  13109  faclbnd3  13288  faclbnd4lem1  13289  hashsnle1  13411  hashgt12el  13416  hashgt12el2  13417  sqrlem1  14282  sqrt1  14311  sqrt2gt1lt2  14314  sqrtm1  14315  abs1  14336  rlimno1  14683  harmonic  14889  georeclim  14901  geoisumr  14907  fprodge0  15020  fprodge1  15022  ege2le3  15116  sinbnd  15206  cosbnd  15207  cos2bnd  15214  nn0oddm1d2  15397  flodddiv4  15432  sqnprm  15707  zsqrtelqelz  15759  modprm0  15803  pythagtriplem3  15816  prmolefac  16043  abvneg  19117  gzrngunitlem  20098  rge0srg  20104  dscmet  22670  nmoid  22839  iccpnfcnv  23036  iccpnfhmeo  23037  xrhmeo  23038  ncvs1  23249  vitalilem4  23683  vitalilem5  23684  aalioulem3  24394  dvradcnv  24480  abelth2  24501  tanregt0  24591  efif1olem3  24596  dvlog2lem  24703  cxpge0  24734  cxpaddlelem  24797  bndatandm  24961  atans2  24963  cxp2lim  25008  scvxcvx  25017  logdiflbnd  25026  fsumharmonic  25043  lgamgulmlem2  25061  lgamgulmlem3  25062  lgamgulmlem5  25064  mule1  25179  sqff1o  25213  ppiub  25234  dchrabs2  25292  zabsle1  25326  lgslem2  25328  lgsfcl2  25333  lgsdir2lem1  25355  lgsne0  25365  lgsdinn0  25375  m1lgs  25418  chtppilim  25469  rpvmasumlem  25481  dchrisum0flblem1  25502  dchrisum0flblem2  25503  mulog2sumlem2  25529  pntlemb  25591  ostth3  25632  axcontlem2  26150  clwwlknon1le1  27392  0ewlk  27410  0pth  27421  nv1  28007  nmosetn0  28097  nmoo0  28123  norm1  28583  nmopsetn0  29201  nmfnsetn0  29214  nmopge0  29247  nmfnge0  29263  nmop0  29322  nmfn0  29323  nmcexi  29362  hstle1  29562  strlem1  29586  strlem5  29591  jplem1  29604  nn0sqeq1  29983  xrsmulgzz  30146  xrge0slmod  30312  unitssxrge0  30414  xrge0iifcnv  30447  xrge0iifiso  30449  xrge0iifhom  30451  nexple  30539  ddemeas  30767  ballotlem2  31019  ballotlem4  31029  ballotlemic  31037  ballotlem1c  31038  signswch  31108  signsvf0  31129  itgexpif  31156  cvmliftlem13  31747  knoppndvlem11  32973  knoppndvlem18  32980  poimirlem23  33877  dvasin  33940  areacirclem1  33944  cntotbnd  34038  pell1qrge1  38136  pell1qrgaplem  38139  pell14qrgapw  38142  pellqrex  38145  pellfundgt1  38149  rmspecnonsq  38173  rmspecfund  38175  rmspecpos  38182  monotoddzzfi  38208  jm2.23  38264  limsup10ex  40667  ioodvbdlimc1lem2  40809  ioodvbdlimc2lem  40811  stoweidlem1  40879  stoweidlem11  40889  stoweidlem18  40896  stoweidlem34  40912  stoweidlem38  40916  stoweidlem55  40933  wallispi2lem1  40949  stirlinglem1  40952  stirlinglem11  40962  stirlinglem13  40964  fourierdlem11  40996  fourierdlem15  41000  fourierdlem39  41024  fourierdlem41  41026  fourierdlem48  41032  fourierdlem79  41063  ovn0lem  41443  hoidmvlelem2  41474  hoidmvlelem4  41476  smfmullem4  41665  iccpartgt  42121  flsqrt  42208  tgblthelfgott  42403  tgoldbach  42405  nn0eo  43015
  Copyright terms: Public domain W3C validator