Theorem 0le1 11832

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 11303	. 2 ⊢ 0 ∈ ℝ
2		1re 11301	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11831	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11426	1 ⊢ 0 ≤ 1

This proof depends on syntax axioms:   class class class wbr 5103  0cc0 11193  1c1 11194   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537

This theorem is used by:  lemulge11  12172  0le2OLD  12439  1eluzge0  13000  x2times  13422  0elunit  13593  1elunit  13594  nnge2recico01  13631  fldiv4p1lem1div2  13968  1mod  14036  expge0  14234  expge1  14235  faclbnd3  14429  faclbnd4lem1  14430  hashsnle1  14555  hashgt12el  14560  hashgt12el2  14561  01sqrexlem1  15402  sqrt1  15431  sqrt2gt1lt2  15434  sqrtm1  15435  abs1  15457  rlimno1  15814  harmonic  16021  georeclim  16034  geoisumr  16040  fprodge0  16153  fprodge1  16155  ege2le3  16249  sinbnd  16341  cosbnd  16342  cos2bnd  16349  nn0oddm1d2  16548  flodddiv4  16578  sqnprm  16871  zsqrtelqelz  16927  modprm0  16976  pythagtriplem3  16989  prmolefac  17217  abvneg  21076  gzrngunitlem  21731  rge0srg  21737  psdmvr  22483  dscmet  24884  nmoid  25054  iccpnfcnv  25258  iccpnfhmeo  25259  xrhmeo  25260  ncvs1  25471  vitalilem4  25925  vitalilem5  25926  aalioulem3  26654  dvradcnv  26741  abelth2  26762  tanregt0  26860  efif1olem3  26865  dvlog2lem  26973  cxpge0  27004  cxpaddlelem  27072  bndatandm  27250  atans2  27252  cxp2lim  27297  scvxcvx  27306  logdiflbnd  27315  fsumharmonic  27332  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem5  27353  mule1  27468  sqff1o  27502  ppiub  27524  dchrabs2  27582  zabsle1  27616  lgslem2  27618  lgsfcl2  27623  lgsdir2lem1  27645  lgsne0  27655  lgsdinn0  27665  m1lgs  27708  chtppilim  27795  rpvmasumlem  27807  dchrisum0flblem1  27828  dchrisum0flblem2  27829  mulog2sumlem2  27855  pntlemb  27917  ostth3  27958  axcontlem2  29536  elntg2  29556  dfpth2  30307  clwwlknon1le1  30685  0ewlk  30698  0pth  30709  nv1  31270  nmosetn0  31360  nmoo0  31386  norm1  31844  nmopsetn0  32460  nmfnsetn0  32473  nmopge0  32506  nmfnge0  32522  nmop0  32581  nmfn0  32582  nmcexi  32621  hstle1  32821  strlem1  32845  strlem5  32850  jplem1  32863  receqid  33329  nexple  33417  cshw1s2  33514  xrsmulgzz  33563  xrge0slmod  33902  cos9thpiminplylem1  34407  cos9thpinconstrlem1  34414  unitssxrge0  34525  xrge0iifcnv  34558  xrge0iifiso  34560  xrge0iifhom  34562  ddemeas  34862  ballotlem2  35114  ballotlem4  35124  ballotlemic  35132  ballotlem1c  35133  signswch  35183  signsvf0  35202  itgexpif  35228  cvmliftlem13  36040  knoppndvlem11  37368  knoppndvlem18  37375  poimirlem23  38541  dvasin  38602  areacirclem1  38606  cntotbnd  38710  lcmineqlem3  43061  lcmineqlem10  43068  lcmineqlem12  43070  lcmineqlem18  43076  aks4d1p1p4  43101  aks4d1p1p7  43104  aks4d1p3  43108  posbezout  43130  aks6d1c1  43146  aks6d1c2lem4  43157  2np3bcnp1  43174  sticksstones12a  43187  sticksstones12  43188  bcled  43208  aks6d1c7lem1  43210  aks6d1c7lem2  43211  3cubeslem1  43674  pell1qrge1  43856  pell1qrgaplem  43859  pell14qrgapw  43862  pellqrex  43865  pellfundgt1  43869  rmspecnonsq  43893  rmspecfund  43895  rmspecpos  43902  monotoddzzfi  43928  jm2.23  43982  limsup10ex  46752  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem1  46980  stoweidlem11  46990  stoweidlem18  46997  stoweidlem34  47013  stoweidlem38  47017  stoweidlem55  47034  wallispi2lem1  47050  stirlinglem1  47053  stirlinglem11  47063  stirlinglem13  47065  fourierdlem11  47097  fourierdlem15  47101  fourierdlem39  47125  fourierdlem41  47127  fourierdlem48  47133  fourierdlem79  47164  ovn0lem  47544  hoidmvlelem2  47575  hoidmvlelem4  47577  smfmullem4  47773  ormkglobd  47856  goldratval  47905  iccpartgt  48478  flsqrt  48647  2exp340mod341  48800  8exp8mod9  48803  nfermltl8rev  48809  tgblthelfgott  48882  tgoldbach  48884  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  nn0eo  49609  seppcld  50007