Theorem 0le1 11664

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 11137	. 2 ⊢ 0 ∈ ℝ
2		1re 11135	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11663	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11260	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5086  0cc0 11029  1c1 11030   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371

This theorem is referenced by:  lemulge11  12009  0le2  12274  1eluzge0  12821  x2times  13242  0elunit  13413  1elunit  13414  nnge2recico01  13451  fldiv4p1lem1div2  13785  1mod  13853  expge0  14051  expge1  14052  faclbnd3  14245  faclbnd4lem1  14246  hashsnle1  14370  hashgt12el  14375  hashgt12el2  14376  01sqrexlem1  15195  sqrt1  15224  sqrt2gt1lt2  15227  sqrtm1  15228  abs1  15250  rlimno1  15607  harmonic  15815  georeclim  15828  geoisumr  15834  fprodge0  15949  fprodge1  15951  ege2le3  16046  sinbnd  16138  cosbnd  16139  cos2bnd  16146  nn0oddm1d2  16345  flodddiv4  16375  sqnprm  16663  zsqrtelqelz  16719  modprm0  16767  pythagtriplem3  16780  prmolefac  17008  abvneg  20794  gzrngunitlem  21422  rge0srg  21428  psdmvr  22145  dscmet  24547  nmoid  24717  iccpnfcnv  24921  iccpnfhmeo  24922  xrhmeo  24923  ncvs1  25134  vitalilem4  25588  vitalilem5  25589  aalioulem3  26311  dvradcnv  26399  abelth2  26420  tanregt0  26516  efif1olem3  26521  dvlog2lem  26629  cxpge0  26660  cxpaddlelem  26728  bndatandm  26906  atans2  26908  cxp2lim  26954  scvxcvx  26963  logdiflbnd  26972  fsumharmonic  26989  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem5  27010  mule1  27125  sqff1o  27159  ppiub  27181  dchrabs2  27239  zabsle1  27273  lgslem2  27275  lgsfcl2  27280  lgsdir2lem1  27302  lgsne0  27312  lgsdinn0  27322  m1lgs  27365  chtppilim  27452  rpvmasumlem  27464  dchrisum0flblem1  27485  dchrisum0flblem2  27486  mulog2sumlem2  27512  pntlemb  27574  ostth3  27615  axcontlem2  29048  elntg2  29068  dfpth2  29812  clwwlknon1le1  30186  0ewlk  30199  0pth  30210  nv1  30761  nmosetn0  30851  nmoo0  30877  norm1  31335  nmopsetn0  31951  nmfnsetn0  31964  nmopge0  31997  nmfnge0  32013  nmop0  32072  nmfn0  32073  nmcexi  32112  hstle1  32312  strlem1  32336  strlem5  32341  jplem1  32354  receqid  32832  nexple  32932  cshw1s2  33035  xrsmulgzz  33084  xrge0slmod  33423  cos9thpiminplylem1  33942  cos9thpinconstrlem1  33949  unitssxrge0  34060  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  ddemeas  34396  ballotlem2  34649  ballotlem4  34659  ballotlemic  34667  ballotlem1c  34668  signswch  34721  signsvf0  34740  itgexpif  34766  cvmliftlem13  35494  knoppndvlem11  36798  knoppndvlem18  36805  poimirlem23  37978  dvasin  38039  areacirclem1  38043  cntotbnd  38131  lcmineqlem3  42484  lcmineqlem10  42491  lcmineqlem12  42493  lcmineqlem18  42499  aks4d1p1p4  42524  aks4d1p1p7  42527  aks4d1p3  42531  posbezout  42553  aks6d1c1  42569  aks6d1c2lem4  42580  2np3bcnp1  42597  sticksstones12a  42610  sticksstones12  42611  bcled  42631  aks6d1c7lem1  42633  aks6d1c7lem2  42634  3cubeslem1  43130  pell1qrge1  43316  pell1qrgaplem  43319  pell14qrgapw  43322  pellqrex  43325  pellfundgt1  43329  rmspecnonsq  43353  rmspecfund  43355  rmspecpos  43362  monotoddzzfi  43388  jm2.23  43442  limsup10ex  46219  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem1  46447  stoweidlem11  46457  stoweidlem18  46464  stoweidlem34  46480  stoweidlem38  46484  stoweidlem55  46501  wallispi2lem1  46517  stirlinglem1  46520  stirlinglem11  46530  stirlinglem13  46532  fourierdlem11  46564  fourierdlem15  46568  fourierdlem39  46592  fourierdlem41  46594  fourierdlem48  46600  fourierdlem79  46631  ovn0lem  47011  hoidmvlelem2  47042  hoidmvlelem4  47044  smfmullem4  47240  ormkglobd  47321  iccpartgt  47899  flsqrt  48068  2exp340mod341  48221  8exp8mod9  48224  nfermltl8rev  48230  tgblthelfgott  48303  tgoldbach  48305  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  nn0eo  49016  seppcld  49417