Theorem 0le1 11000

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

Step	Hyp	Ref	Expression
1		0re 10478	. 2 ⊢ 0 ∈ ℝ
2		1re 10476	. 2 ⊢ 1 ∈ ℝ
3		0lt1 10999	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 10599	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 4956  0cc0 10372  1c1 10373   ≤ cle 10511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448  ax-pre-mulgt0 10449

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-po 5354  df-so 5355  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-sub 10708  df-neg 10709

This theorem is referenced by:  lemulge11  11339  0le2  11576  1eluzge0  12130  x2times  12531  0elunit  12694  1elunit  12695  fldiv4p1lem1div2  13043  1mod  13109  expge0  13303  expge1  13304  faclbnd3  13490  faclbnd4lem1  13491  hashsnle1  13614  hashgt12el  13619  hashgt12el2  13620  sqrlem1  14424  sqrt1  14453  sqrt2gt1lt2  14456  sqrtm1  14457  abs1  14479  rlimno1  14832  harmonic  15035  georeclim  15049  geoisumr  15055  fprodge0  15168  fprodge1  15170  ege2le3  15264  sinbnd  15354  cosbnd  15355  cos2bnd  15362  nn0oddm1d2  15557  flodddiv4  15585  sqnprm  15863  zsqrtelqelz  15915  modprm0  15959  pythagtriplem3  15972  prmolefac  16199  abvneg  19283  gzrngunitlem  20280  rge0srg  20286  dscmet  22853  nmoid  23022  iccpnfcnv  23219  iccpnfhmeo  23220  xrhmeo  23221  ncvs1  23432  vitalilem4  23883  vitalilem5  23884  aalioulem3  24594  dvradcnv  24680  abelth2  24701  tanregt0  24792  efif1olem3  24797  dvlog2lem  24904  cxpge0  24935  cxpaddlelem  25001  bndatandm  25176  atans2  25178  cxp2lim  25224  scvxcvx  25233  logdiflbnd  25242  fsumharmonic  25259  lgamgulmlem2  25277  lgamgulmlem3  25278  lgamgulmlem5  25280  mule1  25395  sqff1o  25429  ppiub  25450  dchrabs2  25508  zabsle1  25542  lgslem2  25544  lgsfcl2  25549  lgsdir2lem1  25571  lgsne0  25581  lgsdinn0  25591  m1lgs  25634  chtppilim  25721  rpvmasumlem  25733  dchrisum0flblem1  25754  dchrisum0flblem2  25755  mulog2sumlem2  25781  pntlemb  25843  ostth3  25884  axcontlem2  26422  elntg2  26442  clwwlknon1le1  27555  0ewlk  27568  0pth  27579  nv1  28131  nmosetn0  28221  nmoo0  28247  norm1  28705  nmopsetn0  29321  nmfnsetn0  29334  nmopge0  29367  nmfnge0  29383  nmop0  29442  nmfn0  29443  nmcexi  29482  hstle1  29682  strlem1  29706  strlem5  29711  jplem1  29724  cshw1s2  30278  xrsmulgzz  30309  xrge0slmod  30526  unitssxrge0  30716  xrge0iifcnv  30749  xrge0iifiso  30751  xrge0iifhom  30753  nexple  30841  ddemeas  31068  ballotlem2  31319  ballotlem4  31329  ballotlemic  31337  ballotlem1c  31338  signswch  31404  signsvf0  31423  itgexpif  31450  cvmliftlem13  32107  knoppndvlem11  33414  knoppndvlem18  33421  poimirlem23  34392  dvasin  34455  areacirclem1  34459  cntotbnd  34552  pell1qrge1  38903  pell1qrgaplem  38906  pell14qrgapw  38909  pellqrex  38912  pellfundgt1  38916  rmspecnonsq  38940  rmspecfund  38942  rmspecpos  38949  monotoddzzfi  38975  jm2.23  39029  limsup10ex  41550  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  stoweidlem1  41782  stoweidlem11  41792  stoweidlem18  41799  stoweidlem34  41815  stoweidlem38  41819  stoweidlem55  41836  wallispi2lem1  41852  stirlinglem1  41855  stirlinglem11  41865  stirlinglem13  41867  fourierdlem11  41899  fourierdlem15  41903  fourierdlem39  41927  fourierdlem41  41929  fourierdlem48  41935  fourierdlem79  41966  ovn0lem  42343  hoidmvlelem2  42374  hoidmvlelem4  42376  smfmullem4  42565  iccpartgt  43023  flsqrt  43192  2exp340mod341  43334  8exp8mod9  43337  nfermltl8rev  43343  tgblthelfgott  43416  tgoldbach  43418  nn0eo  44023