Theorem 0le1 11677

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 11152	. 2 ⊢ 0 ∈ ℝ
2		1re 11150	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11676	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11273	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5102  0cc0 11044  1c1 11045   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384

This theorem is referenced by:  lemulge11  12021  0le2  12264  1eluzge0  12815  x2times  13235  0elunit  13406  1elunit  13407  fldiv4p1lem1div2  13773  1mod  13841  expge0  14039  expge1  14040  faclbnd3  14233  faclbnd4lem1  14234  hashsnle1  14358  hashgt12el  14363  hashgt12el2  14364  01sqrexlem1  15184  sqrt1  15213  sqrt2gt1lt2  15216  sqrtm1  15217  abs1  15239  rlimno1  15596  harmonic  15801  georeclim  15814  geoisumr  15820  fprodge0  15935  fprodge1  15937  ege2le3  16032  sinbnd  16124  cosbnd  16125  cos2bnd  16132  nn0oddm1d2  16331  flodddiv4  16361  sqnprm  16648  zsqrtelqelz  16704  modprm0  16752  pythagtriplem3  16765  prmolefac  16993  abvneg  20711  gzrngunitlem  21325  rge0srg  21331  psdmvr  22032  dscmet  24436  nmoid  24606  iccpnfcnv  24818  iccpnfhmeo  24819  xrhmeo  24820  ncvs1  25033  vitalilem4  25488  vitalilem5  25489  aalioulem3  26218  dvradcnv  26306  abelth2  26328  tanregt0  26424  efif1olem3  26429  dvlog2lem  26537  cxpge0  26568  cxpaddlelem  26637  bndatandm  26815  atans2  26817  cxp2lim  26863  scvxcvx  26872  logdiflbnd  26881  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem5  26919  mule1  27034  sqff1o  27068  ppiub  27091  dchrabs2  27149  zabsle1  27183  lgslem2  27185  lgsfcl2  27190  lgsdir2lem1  27212  lgsne0  27222  lgsdinn0  27232  m1lgs  27275  chtppilim  27362  rpvmasumlem  27374  dchrisum0flblem1  27395  dchrisum0flblem2  27396  mulog2sumlem2  27422  pntlemb  27484  ostth3  27525  axcontlem2  28868  elntg2  28888  dfpth2  29632  clwwlknon1le1  30003  0ewlk  30016  0pth  30027  nv1  30577  nmosetn0  30667  nmoo0  30693  norm1  31151  nmopsetn0  31767  nmfnsetn0  31780  nmopge0  31813  nmfnge0  31829  nmop0  31888  nmfn0  31889  nmcexi  31928  hstle1  32128  strlem1  32152  strlem5  32157  jplem1  32170  receqid  32641  nexple  32742  cshw1s2  32855  xrsmulgzz  32920  xrge0slmod  33292  cos9thpiminplylem1  33745  cos9thpinconstrlem1  33752  unitssxrge0  33863  xrge0iifcnv  33896  xrge0iifiso  33898  xrge0iifhom  33900  ddemeas  34199  ballotlem2  34453  ballotlem4  34463  ballotlemic  34471  ballotlem1c  34472  signswch  34525  signsvf0  34544  itgexpif  34570  cvmliftlem13  35256  knoppndvlem11  36483  knoppndvlem18  36490  poimirlem23  37610  dvasin  37671  areacirclem1  37675  cntotbnd  37763  lcmineqlem3  41992  lcmineqlem10  41999  lcmineqlem12  42001  lcmineqlem18  42007  aks4d1p1p4  42032  aks4d1p1p7  42035  aks4d1p3  42039  posbezout  42061  aks6d1c1  42077  aks6d1c2lem4  42088  2np3bcnp1  42105  sticksstones12a  42118  sticksstones12  42119  bcled  42139  aks6d1c7lem1  42141  aks6d1c7lem2  42142  3cubeslem1  42645  pell1qrge1  42831  pell1qrgaplem  42834  pell14qrgapw  42837  pellqrex  42840  pellfundgt1  42844  rmspecnonsq  42868  rmspecfund  42870  rmspecpos  42878  monotoddzzfi  42904  jm2.23  42958  limsup10ex  45744  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem1  45972  stoweidlem11  45982  stoweidlem18  45989  stoweidlem34  46005  stoweidlem38  46009  stoweidlem55  46026  wallispi2lem1  46042  stirlinglem1  46045  stirlinglem11  46055  stirlinglem13  46057  fourierdlem11  46089  fourierdlem15  46093  fourierdlem39  46117  fourierdlem41  46119  fourierdlem48  46125  fourierdlem79  46156  ovn0lem  46536  hoidmvlelem2  46567  hoidmvlelem4  46569  smfmullem4  46765  ormkglobd  46846  iccpartgt  47401  flsqrt  47567  2exp340mod341  47707  8exp8mod9  47710  nfermltl8rev  47716  tgblthelfgott  47789  tgoldbach  47791  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  nn0eo  48490  seppcld  48891