Theorem 0le1 11786

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 11263	. 2 ⊢ 0 ∈ ℝ
2		1re 11261	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11785	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11384	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5143  0cc0 11155  1c1 11156   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495

This theorem is referenced by:  lemulge11  12130  0le2  12368  1eluzge0  12934  x2times  13341  0elunit  13509  1elunit  13510  fldiv4p1lem1div2  13875  1mod  13943  expge0  14139  expge1  14140  faclbnd3  14331  faclbnd4lem1  14332  hashsnle1  14456  hashgt12el  14461  hashgt12el2  14462  01sqrexlem1  15281  sqrt1  15310  sqrt2gt1lt2  15313  sqrtm1  15314  abs1  15336  rlimno1  15690  harmonic  15895  georeclim  15908  geoisumr  15914  fprodge0  16029  fprodge1  16031  ege2le3  16126  sinbnd  16216  cosbnd  16217  cos2bnd  16224  nn0oddm1d2  16422  flodddiv4  16452  sqnprm  16739  zsqrtelqelz  16795  modprm0  16843  pythagtriplem3  16856  prmolefac  17084  abvneg  20827  gzrngunitlem  21450  rge0srg  21456  psdmvr  22173  dscmet  24585  nmoid  24763  iccpnfcnv  24975  iccpnfhmeo  24976  xrhmeo  24977  ncvs1  25191  vitalilem4  25646  vitalilem5  25647  aalioulem3  26376  dvradcnv  26464  abelth2  26486  tanregt0  26581  efif1olem3  26586  dvlog2lem  26694  cxpge0  26725  cxpaddlelem  26794  bndatandm  26972  atans2  26974  cxp2lim  27020  scvxcvx  27029  logdiflbnd  27038  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  mule1  27191  sqff1o  27225  ppiub  27248  dchrabs2  27306  zabsle1  27340  lgslem2  27342  lgsfcl2  27347  lgsdir2lem1  27369  lgsne0  27379  lgsdinn0  27389  m1lgs  27432  chtppilim  27519  rpvmasumlem  27531  dchrisum0flblem1  27552  dchrisum0flblem2  27553  mulog2sumlem2  27579  pntlemb  27641  ostth3  27682  axcontlem2  28980  elntg2  29000  dfpth2  29749  clwwlknon1le1  30120  0ewlk  30133  0pth  30144  nv1  30694  nmosetn0  30784  nmoo0  30810  norm1  31268  nmopsetn0  31884  nmfnsetn0  31897  nmopge0  31930  nmfnge0  31946  nmop0  32005  nmfn0  32006  nmcexi  32045  hstle1  32245  strlem1  32269  strlem5  32274  jplem1  32287  nexple  32833  cshw1s2  32945  xrsmulgzz  33011  xrge0slmod  33376  unitssxrge0  33899  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  ddemeas  34237  ballotlem2  34491  ballotlem4  34501  ballotlemic  34509  ballotlem1c  34510  signswch  34576  signsvf0  34595  itgexpif  34621  cvmliftlem13  35301  knoppndvlem11  36523  knoppndvlem18  36530  poimirlem23  37650  dvasin  37711  areacirclem1  37715  cntotbnd  37803  lcmineqlem3  42032  lcmineqlem10  42039  lcmineqlem12  42041  lcmineqlem18  42047  aks4d1p1p4  42072  aks4d1p1p7  42075  aks4d1p3  42079  posbezout  42101  aks6d1c1  42117  aks6d1c2lem4  42128  2np3bcnp1  42145  sticksstones12a  42158  sticksstones12  42159  bcled  42179  aks6d1c7lem1  42181  aks6d1c7lem2  42182  metakunt1  42206  metakunt28  42233  3cubeslem1  42695  pell1qrge1  42881  pell1qrgaplem  42884  pell14qrgapw  42887  pellqrex  42890  pellfundgt1  42894  rmspecnonsq  42918  rmspecfund  42920  rmspecpos  42928  monotoddzzfi  42954  jm2.23  43008  limsup10ex  45788  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem1  46016  stoweidlem11  46026  stoweidlem18  46033  stoweidlem34  46049  stoweidlem38  46053  stoweidlem55  46070  wallispi2lem1  46086  stirlinglem1  46089  stirlinglem11  46099  stirlinglem13  46101  fourierdlem11  46133  fourierdlem15  46137  fourierdlem39  46161  fourierdlem41  46163  fourierdlem48  46169  fourierdlem79  46200  ovn0lem  46580  hoidmvlelem2  46611  hoidmvlelem4  46613  smfmullem4  46809  ormkglobd  46890  iccpartgt  47414  flsqrt  47580  2exp340mod341  47720  8exp8mod9  47723  nfermltl8rev  47729  tgblthelfgott  47802  tgoldbach  47804  nn0eo  48449  seppcld  48827