Theorem 0le1 11733

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 11206	. 2 ⊢ 0 ∈ ℝ
2		1re 11204	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11732	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11329	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5110  0cc0 11096  1c1 11097   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440

This theorem is referenced by:  lemulge11  12073  0le2OLD  12340  1eluzge0  12900  x2times  13321  0elunit  13492  1elunit  13493  nnge2recico01  13530  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  16140  sinbnd  16232  cosbnd  16233  cos2bnd  16240  nn0oddm1d2  16439  flodddiv4  16469  sqnprm  16757  zsqrtelqelz  16813  modprm0  16861  pythagtriplem3  16874  prmolefac  17102  abvneg  20903  gzrngunitlem  21547  rge0srg  21553  psdmvr  22297  dscmet  24694  nmoid  24864  iccpnfcnv  25068  iccpnfhmeo  25069  xrhmeo  25070  ncvs1  25281  vitalilem4  25735  vitalilem5  25736  aalioulem3  26460  dvradcnv  26546  abelth2  26567  tanregt0  26666  efif1olem3  26671  dvlog2lem  26779  cxpge0  26810  cxpaddlelem  26878  bndatandm  27056  atans2  27058  cxp2lim  27103  scvxcvx  27112  logdiflbnd  27121  fsumharmonic  27138  lgamgulmlem2  27156  lgamgulmlem3  27157  lgamgulmlem5  27159  mule1  27274  sqff1o  27308  ppiub  27330  dchrabs2  27388  zabsle1  27422  lgslem2  27424  lgsfcl2  27429  lgsdir2lem1  27451  lgsne0  27461  lgsdinn0  27471  m1lgs  27514  chtppilim  27601  rpvmasumlem  27613  dchrisum0flblem1  27634  dchrisum0flblem2  27635  mulog2sumlem2  27661  pntlemb  27723  ostth3  27764  axcontlem2  29252  elntg2  29272  dfpth2  30015  clwwlknon1le1  30389  0ewlk  30402  0pth  30413  nv1  30964  nmosetn0  31054  nmoo0  31080  norm1  31538  nmopsetn0  32154  nmfnsetn0  32167  nmopge0  32200  nmfnge0  32216  nmop0  32275  nmfn0  32276  nmcexi  32315  hstle1  32515  strlem1  32539  strlem5  32544  jplem1  32557  receqid  33026  nexple  33114  cshw1s2  33217  xrsmulgzz  33266  xrge0slmod  33607  cos9thpiminplylem1  34113  cos9thpinconstrlem1  34120  unitssxrge0  34231  xrge0iifcnv  34264  xrge0iifiso  34266  xrge0iifhom  34268  ddemeas  34567  ballotlem2  34820  ballotlem4  34830  ballotlemic  34838  ballotlem1c  34839  signswch  34889  signsvf0  34908  itgexpif  34934  cvmliftlem13  35683  knoppndvlem11  36996  knoppndvlem18  37003  poimirlem23  38177  dvasin  38238  areacirclem1  38242  cntotbnd  38330  lcmineqlem3  42683  lcmineqlem10  42690  lcmineqlem12  42692  lcmineqlem18  42698  aks4d1p1p4  42723  aks4d1p1p7  42726  aks4d1p3  42730  posbezout  42752  aks6d1c1  42768  aks6d1c2lem4  42779  2np3bcnp1  42796  sticksstones12a  42809  sticksstones12  42810  bcled  42830  aks6d1c7lem1  42832  aks6d1c7lem2  42833  3cubeslem1  43302  pell1qrge1  43484  pell1qrgaplem  43487  pell14qrgapw  43490  pellqrex  43493  pellfundgt1  43497  rmspecnonsq  43521  rmspecfund  43523  rmspecpos  43530  monotoddzzfi  43556  jm2.23  43610  limsup10ex  46374  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  stoweidlem1  46602  stoweidlem11  46612  stoweidlem18  46619  stoweidlem34  46635  stoweidlem38  46639  stoweidlem55  46656  wallispi2lem1  46672  stirlinglem1  46675  stirlinglem11  46685  stirlinglem13  46687  fourierdlem11  46719  fourierdlem15  46723  fourierdlem39  46747  fourierdlem41  46749  fourierdlem48  46755  fourierdlem79  46786  ovn0lem  47166  hoidmvlelem2  47197  hoidmvlelem4  47199  smfmullem4  47395  ormkglobd  47478  iccpartgt  48060  flsqrt  48229  2exp340mod341  48382  8exp8mod9  48385  nfermltl8rev  48391  tgblthelfgott  48464  tgoldbach  48466  pgnbgreunbgrlem2lem1  48763  pgnbgreunbgrlem2lem2  48764  nn0eo  49188  seppcld  49588