Theorem 0le1 11765

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 11242	. 2 ⊢ 0 ∈ ℝ
2		1re 11240	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11764	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11363	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5124  0cc0 11134  1c1 11135   ≤ cle 11275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474

This theorem is referenced by:  lemulge11  12109  0le2  12347  1eluzge0  12913  x2times  13320  0elunit  13491  1elunit  13492  fldiv4p1lem1div2  13857  1mod  13925  expge0  14121  expge1  14122  faclbnd3  14315  faclbnd4lem1  14316  hashsnle1  14440  hashgt12el  14445  hashgt12el2  14446  01sqrexlem1  15266  sqrt1  15295  sqrt2gt1lt2  15298  sqrtm1  15299  abs1  15321  rlimno1  15675  harmonic  15880  georeclim  15893  geoisumr  15899  fprodge0  16014  fprodge1  16016  ege2le3  16111  sinbnd  16203  cosbnd  16204  cos2bnd  16211  nn0oddm1d2  16409  flodddiv4  16439  sqnprm  16726  zsqrtelqelz  16782  modprm0  16830  pythagtriplem3  16843  prmolefac  17071  abvneg  20791  gzrngunitlem  21405  rge0srg  21411  psdmvr  22112  dscmet  24516  nmoid  24686  iccpnfcnv  24898  iccpnfhmeo  24899  xrhmeo  24900  ncvs1  25114  vitalilem4  25569  vitalilem5  25570  aalioulem3  26299  dvradcnv  26387  abelth2  26409  tanregt0  26505  efif1olem3  26510  dvlog2lem  26618  cxpge0  26649  cxpaddlelem  26718  bndatandm  26896  atans2  26898  cxp2lim  26944  scvxcvx  26953  logdiflbnd  26962  fsumharmonic  26979  lgamgulmlem2  26997  lgamgulmlem3  26998  lgamgulmlem5  27000  mule1  27115  sqff1o  27149  ppiub  27172  dchrabs2  27230  zabsle1  27264  lgslem2  27266  lgsfcl2  27271  lgsdir2lem1  27293  lgsne0  27303  lgsdinn0  27313  m1lgs  27356  chtppilim  27443  rpvmasumlem  27455  dchrisum0flblem1  27476  dchrisum0flblem2  27477  mulog2sumlem2  27503  pntlemb  27565  ostth3  27606  axcontlem2  28949  elntg2  28969  dfpth2  29716  clwwlknon1le1  30087  0ewlk  30100  0pth  30111  nv1  30661  nmosetn0  30751  nmoo0  30777  norm1  31235  nmopsetn0  31851  nmfnsetn0  31864  nmopge0  31897  nmfnge0  31913  nmop0  31972  nmfn0  31973  nmcexi  32012  hstle1  32212  strlem1  32236  strlem5  32241  jplem1  32254  receqid  32727  nexple  32828  cshw1s2  32941  xrsmulgzz  33006  xrge0slmod  33368  cos9thpiminplylem1  33821  cos9thpinconstrlem1  33828  unitssxrge0  33936  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhom  33973  ddemeas  34272  ballotlem2  34526  ballotlem4  34536  ballotlemic  34544  ballotlem1c  34545  signswch  34598  signsvf0  34617  itgexpif  34643  cvmliftlem13  35323  knoppndvlem11  36545  knoppndvlem18  36552  poimirlem23  37672  dvasin  37733  areacirclem1  37737  cntotbnd  37825  lcmineqlem3  42049  lcmineqlem10  42056  lcmineqlem12  42058  lcmineqlem18  42064  aks4d1p1p4  42089  aks4d1p1p7  42092  aks4d1p3  42096  posbezout  42118  aks6d1c1  42134  aks6d1c2lem4  42145  2np3bcnp1  42162  sticksstones12a  42175  sticksstones12  42176  bcled  42196  aks6d1c7lem1  42198  aks6d1c7lem2  42199  3cubeslem1  42674  pell1qrge1  42860  pell1qrgaplem  42863  pell14qrgapw  42866  pellqrex  42869  pellfundgt1  42873  rmspecnonsq  42897  rmspecfund  42899  rmspecpos  42907  monotoddzzfi  42933  jm2.23  42987  limsup10ex  45769  ioodvbdlimc1lem2  45928  ioodvbdlimc2lem  45930  stoweidlem1  45997  stoweidlem11  46007  stoweidlem18  46014  stoweidlem34  46030  stoweidlem38  46034  stoweidlem55  46051  wallispi2lem1  46067  stirlinglem1  46070  stirlinglem11  46080  stirlinglem13  46082  fourierdlem11  46114  fourierdlem15  46118  fourierdlem39  46142  fourierdlem41  46144  fourierdlem48  46150  fourierdlem79  46181  ovn0lem  46561  hoidmvlelem2  46592  hoidmvlelem4  46594  smfmullem4  46790  ormkglobd  46871  iccpartgt  47408  flsqrt  47574  2exp340mod341  47714  8exp8mod9  47717  nfermltl8rev  47723  tgblthelfgott  47796  tgoldbach  47798  nn0eo  48475  seppcld  48871