Theorem 0le1 11732

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 11205	. 2 ⊢ 0 ∈ ℝ
2		1re 11203	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11731	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11328	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5109  0cc0 11095  1c1 11096   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439

This theorem is referenced by:  lemulge11  12072  0le2OLD  12339  1eluzge0  12899  x2times  13320  0elunit  13491  1elunit  13492  nnge2recico01  13529  fldiv4p1lem1div2  13864  1mod  13932  expge0  14130  expge1  14131  faclbnd3  14324  faclbnd4lem1  14325  hashsnle1  14450  hashgt12el  14455  hashgt12el2  14456  01sqrexlem1  15289  sqrt1  15318  sqrt2gt1lt2  15321  sqrtm1  15322  abs1  15344  rlimno1  15701  harmonic  15909  georeclim  15922  geoisumr  15928  fprodge0  16043  fprodge1  16045  ege2le3  16139  sinbnd  16231  cosbnd  16232  cos2bnd  16239  nn0oddm1d2  16438  flodddiv4  16468  sqnprm  16756  zsqrtelqelz  16812  modprm0  16860  pythagtriplem3  16873  prmolefac  17101  abvneg  20929  gzrngunitlem  21582  rge0srg  21588  psdmvr  22332  dscmet  24729  nmoid  24899  iccpnfcnv  25103  iccpnfhmeo  25104  xrhmeo  25105  ncvs1  25316  vitalilem4  25770  vitalilem5  25771  aalioulem3  26497  dvradcnv  26584  abelth2  26605  tanregt0  26704  efif1olem3  26709  dvlog2lem  26817  cxpge0  26848  cxpaddlelem  26916  bndatandm  27094  atans2  27096  cxp2lim  27141  scvxcvx  27150  logdiflbnd  27159  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  mule1  27312  sqff1o  27346  ppiub  27368  dchrabs2  27426  zabsle1  27460  lgslem2  27462  lgsfcl2  27467  lgsdir2lem1  27489  lgsne0  27499  lgsdinn0  27509  m1lgs  27552  chtppilim  27639  rpvmasumlem  27651  dchrisum0flblem1  27672  dchrisum0flblem2  27673  mulog2sumlem2  27699  pntlemb  27761  ostth3  27802  axcontlem2  29315  elntg2  29335  dfpth2  30078  clwwlknon1le1  30452  0ewlk  30465  0pth  30476  nv1  31027  nmosetn0  31117  nmoo0  31143  norm1  31601  nmopsetn0  32217  nmfnsetn0  32230  nmopge0  32263  nmfnge0  32279  nmop0  32338  nmfn0  32339  nmcexi  32378  hstle1  32578  strlem1  32602  strlem5  32607  jplem1  32620  receqid  33089  nexple  33177  cshw1s2  33280  xrsmulgzz  33329  xrge0slmod  33668  cos9thpiminplylem1  34172  cos9thpinconstrlem1  34179  unitssxrge0  34290  xrge0iifcnv  34323  xrge0iifiso  34325  xrge0iifhom  34327  ddemeas  34626  ballotlem2  34879  ballotlem4  34889  ballotlemic  34897  ballotlem1c  34898  signswch  34948  signsvf0  34967  itgexpif  34993  cvmliftlem13  35788  knoppndvlem11  37111  knoppndvlem18  37118  poimirlem23  38294  dvasin  38355  areacirclem1  38359  cntotbnd  38447  lcmineqlem3  42798  lcmineqlem10  42805  lcmineqlem12  42807  lcmineqlem18  42813  aks4d1p1p4  42838  aks4d1p1p7  42841  aks4d1p3  42845  posbezout  42867  aks6d1c1  42883  aks6d1c2lem4  42894  2np3bcnp1  42911  sticksstones12a  42924  sticksstones12  42925  bcled  42945  aks6d1c7lem1  42947  aks6d1c7lem2  42948  3cubeslem1  43415  pell1qrge1  43597  pell1qrgaplem  43600  pell14qrgapw  43603  pellqrex  43606  pellfundgt1  43610  rmspecnonsq  43634  rmspecfund  43636  rmspecpos  43643  monotoddzzfi  43669  jm2.23  43723  limsup10ex  46487  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  stoweidlem1  46715  stoweidlem11  46725  stoweidlem18  46732  stoweidlem34  46748  stoweidlem38  46752  stoweidlem55  46769  wallispi2lem1  46785  stirlinglem1  46788  stirlinglem11  46798  stirlinglem13  46800  fourierdlem11  46832  fourierdlem15  46836  fourierdlem39  46860  fourierdlem41  46862  fourierdlem48  46868  fourierdlem79  46899  ovn0lem  47279  hoidmvlelem2  47310  hoidmvlelem4  47312  smfmullem4  47508  ormkglobd  47591  iccpartgt  48176  flsqrt  48345  2exp340mod341  48498  8exp8mod9  48501  nfermltl8rev  48507  tgblthelfgott  48580  tgoldbach  48582  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  nn0eo  49308  seppcld  49708