Theorem 0le1 11498

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 10977	. 2 ⊢ 0 ∈ ℝ
2		1re 10975	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11497	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11098	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5074  0cc0 10871  1c1 10872   ≤ cle 11010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208

This theorem is referenced by:  lemulge11  11837  0le2  12075  1eluzge0  12632  x2times  13033  0elunit  13201  1elunit  13202  fldiv4p1lem1div2  13555  1mod  13623  expge0  13819  expge1  13820  faclbnd3  14006  faclbnd4lem1  14007  hashsnle1  14132  hashgt12el  14137  hashgt12el2  14138  sqrlem1  14954  sqrt1  14983  sqrt2gt1lt2  14986  sqrtm1  14987  abs1  15009  rlimno1  15365  harmonic  15571  georeclim  15584  geoisumr  15590  fprodge0  15703  fprodge1  15705  ege2le3  15799  sinbnd  15889  cosbnd  15890  cos2bnd  15897  nn0oddm1d2  16094  flodddiv4  16122  sqnprm  16407  zsqrtelqelz  16462  modprm0  16506  pythagtriplem3  16519  prmolefac  16747  abvneg  20094  gzrngunitlem  20663  rge0srg  20669  dscmet  23728  nmoid  23906  iccpnfcnv  24107  iccpnfhmeo  24108  xrhmeo  24109  ncvs1  24321  vitalilem4  24775  vitalilem5  24776  aalioulem3  25494  dvradcnv  25580  abelth2  25601  tanregt0  25695  efif1olem3  25700  dvlog2lem  25807  cxpge0  25838  cxpaddlelem  25904  bndatandm  26079  atans2  26081  cxp2lim  26126  scvxcvx  26135  logdiflbnd  26144  fsumharmonic  26161  lgamgulmlem2  26179  lgamgulmlem3  26180  lgamgulmlem5  26182  mule1  26297  sqff1o  26331  ppiub  26352  dchrabs2  26410  zabsle1  26444  lgslem2  26446  lgsfcl2  26451  lgsdir2lem1  26473  lgsne0  26483  lgsdinn0  26493  m1lgs  26536  chtppilim  26623  rpvmasumlem  26635  dchrisum0flblem1  26656  dchrisum0flblem2  26657  mulog2sumlem2  26683  pntlemb  26745  ostth3  26786  axcontlem2  27333  elntg2  27353  clwwlknon1le1  28465  0ewlk  28478  0pth  28489  nv1  29037  nmosetn0  29127  nmoo0  29153  norm1  29611  nmopsetn0  30227  nmfnsetn0  30240  nmopge0  30273  nmfnge0  30289  nmop0  30348  nmfn0  30349  nmcexi  30388  hstle1  30588  strlem1  30612  strlem5  30617  jplem1  30630  cshw1s2  31232  xrsmulgzz  31287  xrge0slmod  31548  unitssxrge0  31850  xrge0iifcnv  31883  xrge0iifiso  31885  xrge0iifhom  31887  nexple  31977  ddemeas  32204  ballotlem2  32455  ballotlem4  32465  ballotlemic  32473  ballotlem1c  32474  signswch  32540  signsvf0  32559  itgexpif  32586  cvmliftlem13  33258  knoppndvlem11  34702  knoppndvlem18  34709  poimirlem23  35800  dvasin  35861  areacirclem1  35865  cntotbnd  35954  lcmineqlem3  40039  lcmineqlem10  40046  lcmineqlem12  40048  lcmineqlem18  40054  aks4d1p1p4  40079  aks4d1p1p7  40082  aks4d1p3  40086  2np3bcnp1  40100  sticksstones12a  40113  sticksstones12  40114  metakunt1  40125  metakunt28  40152  3cubeslem1  40506  pell1qrge1  40692  pell1qrgaplem  40695  pell14qrgapw  40698  pellqrex  40701  pellfundgt1  40705  rmspecnonsq  40729  rmspecfund  40731  rmspecpos  40738  monotoddzzfi  40764  jm2.23  40818  limsup10ex  43314  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem1  43542  stoweidlem11  43552  stoweidlem18  43559  stoweidlem34  43575  stoweidlem38  43579  stoweidlem55  43596  wallispi2lem1  43612  stirlinglem1  43615  stirlinglem11  43625  stirlinglem13  43627  fourierdlem11  43659  fourierdlem15  43663  fourierdlem39  43687  fourierdlem41  43689  fourierdlem48  43695  fourierdlem79  43726  ovn0lem  44103  hoidmvlelem2  44134  hoidmvlelem4  44136  smfmullem4  44328  iccpartgt  44879  flsqrt  45045  2exp340mod341  45185  8exp8mod9  45188  nfermltl8rev  45194  tgblthelfgott  45267  tgoldbach  45269  nn0eo  45874  seppcld  46223