Theorem 0le1 11736

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 11215	. 2 ⊢ 0 ∈ ℝ
2		1re 11213	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11735	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11336	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5148  0cc0 11109  1c1 11110   ≤ cle 11248

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446

This theorem is referenced by:  lemulge11  12075  0le2  12313  1eluzge0  12875  x2times  13277  0elunit  13445  1elunit  13446  fldiv4p1lem1div2  13799  1mod  13867  expge0  14063  expge1  14064  faclbnd3  14251  faclbnd4lem1  14252  hashsnle1  14376  hashgt12el  14381  hashgt12el2  14382  01sqrexlem1  15188  sqrt1  15217  sqrt2gt1lt2  15220  sqrtm1  15221  abs1  15243  rlimno1  15599  harmonic  15804  georeclim  15817  geoisumr  15823  fprodge0  15936  fprodge1  15938  ege2le3  16032  sinbnd  16122  cosbnd  16123  cos2bnd  16130  nn0oddm1d2  16327  flodddiv4  16355  sqnprm  16638  zsqrtelqelz  16693  modprm0  16737  pythagtriplem3  16750  prmolefac  16978  abvneg  20441  gzrngunitlem  21009  rge0srg  21015  dscmet  24080  nmoid  24258  iccpnfcnv  24459  iccpnfhmeo  24460  xrhmeo  24461  ncvs1  24673  vitalilem4  25127  vitalilem5  25128  aalioulem3  25846  dvradcnv  25932  abelth2  25953  tanregt0  26047  efif1olem3  26052  dvlog2lem  26159  cxpge0  26190  cxpaddlelem  26256  bndatandm  26431  atans2  26433  cxp2lim  26478  scvxcvx  26487  logdiflbnd  26496  fsumharmonic  26513  lgamgulmlem2  26531  lgamgulmlem3  26532  lgamgulmlem5  26534  mule1  26649  sqff1o  26683  ppiub  26704  dchrabs2  26762  zabsle1  26796  lgslem2  26798  lgsfcl2  26803  lgsdir2lem1  26825  lgsne0  26835  lgsdinn0  26845  m1lgs  26888  chtppilim  26975  rpvmasumlem  26987  dchrisum0flblem1  27008  dchrisum0flblem2  27009  mulog2sumlem2  27035  pntlemb  27097  ostth3  27138  axcontlem2  28220  elntg2  28240  clwwlknon1le1  29351  0ewlk  29364  0pth  29375  nv1  29923  nmosetn0  30013  nmoo0  30039  norm1  30497  nmopsetn0  31113  nmfnsetn0  31126  nmopge0  31159  nmfnge0  31175  nmop0  31234  nmfn0  31235  nmcexi  31274  hstle1  31474  strlem1  31498  strlem5  31503  jplem1  31516  cshw1s2  32119  xrsmulgzz  32174  xrge0slmod  32458  unitssxrge0  32875  xrge0iifcnv  32908  xrge0iifiso  32910  xrge0iifhom  32912  nexple  33002  ddemeas  33229  ballotlem2  33482  ballotlem4  33492  ballotlemic  33500  ballotlem1c  33501  signswch  33567  signsvf0  33586  itgexpif  33613  cvmliftlem13  34282  knoppndvlem11  35393  knoppndvlem18  35400  poimirlem23  36506  dvasin  36567  areacirclem1  36571  cntotbnd  36659  lcmineqlem3  40891  lcmineqlem10  40898  lcmineqlem12  40900  lcmineqlem18  40906  aks4d1p1p4  40931  aks4d1p1p7  40934  aks4d1p3  40938  2np3bcnp1  40955  sticksstones12a  40968  sticksstones12  40969  metakunt1  40980  metakunt28  41007  3cubeslem1  41412  pell1qrge1  41598  pell1qrgaplem  41601  pell14qrgapw  41604  pellqrex  41607  pellfundgt1  41611  rmspecnonsq  41635  rmspecfund  41637  rmspecpos  41645  monotoddzzfi  41671  jm2.23  41725  limsup10ex  44479  ioodvbdlimc1lem2  44638  ioodvbdlimc2lem  44640  stoweidlem1  44707  stoweidlem11  44717  stoweidlem18  44724  stoweidlem34  44740  stoweidlem38  44744  stoweidlem55  44761  wallispi2lem1  44777  stirlinglem1  44780  stirlinglem11  44790  stirlinglem13  44792  fourierdlem11  44824  fourierdlem15  44828  fourierdlem39  44852  fourierdlem41  44854  fourierdlem48  44860  fourierdlem79  44891  ovn0lem  45271  hoidmvlelem2  45302  hoidmvlelem4  45304  smfmullem4  45500  iccpartgt  46085  flsqrt  46251  2exp340mod341  46391  8exp8mod9  46394  nfermltl8rev  46400  tgblthelfgott  46473  tgoldbach  46475  nn0eo  47204  seppcld  47552