Theorem 0le1 11737

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 11216	. 2 ⊢ 0 ∈ ℝ
2		1re 11214	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11736	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11337	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5149  0cc0 11110  1c1 11111   ≤ cle 11249

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447

This theorem is referenced by:  lemulge11  12076  0le2  12314  1eluzge0  12876  x2times  13278  0elunit  13446  1elunit  13447  fldiv4p1lem1div2  13800  1mod  13868  expge0  14064  expge1  14065  faclbnd3  14252  faclbnd4lem1  14253  hashsnle1  14377  hashgt12el  14382  hashgt12el2  14383  01sqrexlem1  15189  sqrt1  15218  sqrt2gt1lt2  15221  sqrtm1  15222  abs1  15244  rlimno1  15600  harmonic  15805  georeclim  15818  geoisumr  15824  fprodge0  15937  fprodge1  15939  ege2le3  16033  sinbnd  16123  cosbnd  16124  cos2bnd  16131  nn0oddm1d2  16328  flodddiv4  16356  sqnprm  16639  zsqrtelqelz  16694  modprm0  16738  pythagtriplem3  16751  prmolefac  16979  abvneg  20442  gzrngunitlem  21010  rge0srg  21016  dscmet  24081  nmoid  24259  iccpnfcnv  24460  iccpnfhmeo  24461  xrhmeo  24462  ncvs1  24674  vitalilem4  25128  vitalilem5  25129  aalioulem3  25847  dvradcnv  25933  abelth2  25954  tanregt0  26048  efif1olem3  26053  dvlog2lem  26160  cxpge0  26191  cxpaddlelem  26259  bndatandm  26434  atans2  26436  cxp2lim  26481  scvxcvx  26490  logdiflbnd  26499  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  mule1  26652  sqff1o  26686  ppiub  26707  dchrabs2  26765  zabsle1  26799  lgslem2  26801  lgsfcl2  26806  lgsdir2lem1  26828  lgsne0  26838  lgsdinn0  26848  m1lgs  26891  chtppilim  26978  rpvmasumlem  26990  dchrisum0flblem1  27011  dchrisum0flblem2  27012  mulog2sumlem2  27038  pntlemb  27100  ostth3  27141  axcontlem2  28223  elntg2  28243  clwwlknon1le1  29354  0ewlk  29367  0pth  29378  nv1  29928  nmosetn0  30018  nmoo0  30044  norm1  30502  nmopsetn0  31118  nmfnsetn0  31131  nmopge0  31164  nmfnge0  31180  nmop0  31239  nmfn0  31240  nmcexi  31279  hstle1  31479  strlem1  31503  strlem5  31508  jplem1  31521  cshw1s2  32124  xrsmulgzz  32179  xrge0slmod  32463  unitssxrge0  32880  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  nexple  33007  ddemeas  33234  ballotlem2  33487  ballotlem4  33497  ballotlemic  33505  ballotlem1c  33506  signswch  33572  signsvf0  33591  itgexpif  33618  cvmliftlem13  34287  knoppndvlem11  35398  knoppndvlem18  35405  poimirlem23  36511  dvasin  36572  areacirclem1  36576  cntotbnd  36664  lcmineqlem3  40896  lcmineqlem10  40903  lcmineqlem12  40905  lcmineqlem18  40911  aks4d1p1p4  40936  aks4d1p1p7  40939  aks4d1p3  40943  2np3bcnp1  40960  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt28  41012  3cubeslem1  41422  pell1qrge1  41608  pell1qrgaplem  41611  pell14qrgapw  41614  pellqrex  41617  pellfundgt1  41621  rmspecnonsq  41645  rmspecfund  41647  rmspecpos  41655  monotoddzzfi  41681  jm2.23  41735  limsup10ex  44489  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem1  44717  stoweidlem11  44727  stoweidlem18  44734  stoweidlem34  44750  stoweidlem38  44754  stoweidlem55  44771  wallispi2lem1  44787  stirlinglem1  44790  stirlinglem11  44800  stirlinglem13  44802  fourierdlem11  44834  fourierdlem15  44838  fourierdlem39  44862  fourierdlem41  44864  fourierdlem48  44870  fourierdlem79  44901  ovn0lem  45281  hoidmvlelem2  45312  hoidmvlelem4  45314  smfmullem4  45510  iccpartgt  46095  flsqrt  46261  2exp340mod341  46401  8exp8mod9  46404  nfermltl8rev  46410  tgblthelfgott  46483  tgoldbach  46485  nn0eo  47214  seppcld  47562