Theorem 0le1 11201

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 10681	. 2 ⊢ 0 ∈ ℝ
2		1re 10679	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11200	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 10801	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5032  0cc0 10575  1c1 10576   ≤ cle 10714

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-po 5443  df-so 5444  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911

This theorem is referenced by:  lemulge11  11540  0le2  11776  1eluzge0  12332  x2times  12733  0elunit  12901  1elunit  12902  fldiv4p1lem1div2  13254  1mod  13320  expge0  13515  expge1  13516  faclbnd3  13702  faclbnd4lem1  13703  hashsnle1  13828  hashgt12el  13833  hashgt12el2  13834  sqrlem1  14650  sqrt1  14679  sqrt2gt1lt2  14682  sqrtm1  14683  abs1  14705  rlimno1  15058  harmonic  15262  georeclim  15276  geoisumr  15282  fprodge0  15395  fprodge1  15397  ege2le3  15491  sinbnd  15581  cosbnd  15582  cos2bnd  15589  nn0oddm1d2  15786  flodddiv4  15814  sqnprm  16098  zsqrtelqelz  16153  modprm0  16197  pythagtriplem3  16210  prmolefac  16437  abvneg  19673  gzrngunitlem  20231  rge0srg  20237  dscmet  23274  nmoid  23444  iccpnfcnv  23645  iccpnfhmeo  23646  xrhmeo  23647  ncvs1  23858  vitalilem4  24311  vitalilem5  24312  aalioulem3  25029  dvradcnv  25115  abelth2  25136  tanregt0  25230  efif1olem3  25235  dvlog2lem  25342  cxpge0  25373  cxpaddlelem  25439  bndatandm  25614  atans2  25616  cxp2lim  25661  scvxcvx  25670  logdiflbnd  25679  fsumharmonic  25696  lgamgulmlem2  25714  lgamgulmlem3  25715  lgamgulmlem5  25717  mule1  25832  sqff1o  25866  ppiub  25887  dchrabs2  25945  zabsle1  25979  lgslem2  25981  lgsfcl2  25986  lgsdir2lem1  26008  lgsne0  26018  lgsdinn0  26028  m1lgs  26071  chtppilim  26158  rpvmasumlem  26170  dchrisum0flblem1  26191  dchrisum0flblem2  26192  mulog2sumlem2  26218  pntlemb  26280  ostth3  26321  axcontlem2  26858  elntg2  26878  clwwlknon1le1  27985  0ewlk  27998  0pth  28009  nv1  28557  nmosetn0  28647  nmoo0  28673  norm1  29131  nmopsetn0  29747  nmfnsetn0  29760  nmopge0  29793  nmfnge0  29809  nmop0  29868  nmfn0  29869  nmcexi  29908  hstle1  30108  strlem1  30132  strlem5  30137  jplem1  30150  cshw1s2  30756  xrsmulgzz  30813  xrge0slmod  31069  unitssxrge0  31371  xrge0iifcnv  31404  xrge0iifiso  31406  xrge0iifhom  31408  nexple  31496  ddemeas  31723  ballotlem2  31974  ballotlem4  31984  ballotlemic  31992  ballotlem1c  31993  signswch  32059  signsvf0  32078  itgexpif  32105  cvmliftlem13  32774  knoppndvlem11  34251  knoppndvlem18  34258  poimirlem23  35360  dvasin  35421  areacirclem1  35425  cntotbnd  35514  lcmineqlem3  39598  lcmineqlem10  39605  lcmineqlem12  39607  lcmineqlem18  39613  aks4d1p1p4  39637  aks4d1p1p7  39640  2np3bcnp1  39645  metakunt1  39647  metakunt28  39674  3cubeslem1  39998  pell1qrge1  40184  pell1qrgaplem  40187  pell14qrgapw  40190  pellqrex  40193  pellfundgt1  40197  rmspecnonsq  40221  rmspecfund  40223  rmspecpos  40230  monotoddzzfi  40256  jm2.23  40310  limsup10ex  42781  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  stoweidlem1  43009  stoweidlem11  43019  stoweidlem18  43026  stoweidlem34  43042  stoweidlem38  43046  stoweidlem55  43063  wallispi2lem1  43079  stirlinglem1  43082  stirlinglem11  43092  stirlinglem13  43094  fourierdlem11  43126  fourierdlem15  43130  fourierdlem39  43154  fourierdlem41  43156  fourierdlem48  43162  fourierdlem79  43193  ovn0lem  43570  hoidmvlelem2  43601  hoidmvlelem4  43603  smfmullem4  43792  iccpartgt  44312  flsqrt  44478  2exp340mod341  44618  8exp8mod9  44621  nfermltl8rev  44627  tgblthelfgott  44700  tgoldbach  44702  nn0eo  45307