Theorem 0le1 11701

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 11176	. 2 ⊢ 0 ∈ ℝ
2		1re 11174	. 2 ⊢ 1 ∈ ℝ
3		0lt1 11700	. 2 ⊢ 0 < 1
4	1, 2, 3	ltleii 11297	1 ⊢ 0 ≤ 1

Syntax hints:   class class class wbr 5107  0cc0 11068  1c1 11069   ≤ cle 11209

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408

This theorem is referenced by:  lemulge11  12045  0le2  12288  1eluzge0  12839  x2times  13259  0elunit  13430  1elunit  13431  fldiv4p1lem1div2  13797  1mod  13865  expge0  14063  expge1  14064  faclbnd3  14257  faclbnd4lem1  14258  hashsnle1  14382  hashgt12el  14387  hashgt12el2  14388  01sqrexlem1  15208  sqrt1  15237  sqrt2gt1lt2  15240  sqrtm1  15241  abs1  15263  rlimno1  15620  harmonic  15825  georeclim  15838  geoisumr  15844  fprodge0  15959  fprodge1  15961  ege2le3  16056  sinbnd  16148  cosbnd  16149  cos2bnd  16156  nn0oddm1d2  16355  flodddiv4  16385  sqnprm  16672  zsqrtelqelz  16728  modprm0  16776  pythagtriplem3  16789  prmolefac  17017  abvneg  20735  gzrngunitlem  21349  rge0srg  21355  psdmvr  22056  dscmet  24460  nmoid  24630  iccpnfcnv  24842  iccpnfhmeo  24843  xrhmeo  24844  ncvs1  25057  vitalilem4  25512  vitalilem5  25513  aalioulem3  26242  dvradcnv  26330  abelth2  26352  tanregt0  26448  efif1olem3  26453  dvlog2lem  26561  cxpge0  26592  cxpaddlelem  26661  bndatandm  26839  atans2  26841  cxp2lim  26887  scvxcvx  26896  logdiflbnd  26905  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  mule1  27058  sqff1o  27092  ppiub  27115  dchrabs2  27173  zabsle1  27207  lgslem2  27209  lgsfcl2  27214  lgsdir2lem1  27236  lgsne0  27246  lgsdinn0  27256  m1lgs  27299  chtppilim  27386  rpvmasumlem  27398  dchrisum0flblem1  27419  dchrisum0flblem2  27420  mulog2sumlem2  27446  pntlemb  27508  ostth3  27549  axcontlem2  28892  elntg2  28912  dfpth2  29659  clwwlknon1le1  30030  0ewlk  30043  0pth  30054  nv1  30604  nmosetn0  30694  nmoo0  30720  norm1  31178  nmopsetn0  31794  nmfnsetn0  31807  nmopge0  31840  nmfnge0  31856  nmop0  31915  nmfn0  31916  nmcexi  31955  hstle1  32155  strlem1  32179  strlem5  32184  jplem1  32197  receqid  32668  nexple  32769  cshw1s2  32882  xrsmulgzz  32947  xrge0slmod  33319  cos9thpiminplylem1  33772  cos9thpinconstrlem1  33779  unitssxrge0  33890  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  ddemeas  34226  ballotlem2  34480  ballotlem4  34490  ballotlemic  34498  ballotlem1c  34499  signswch  34552  signsvf0  34571  itgexpif  34597  cvmliftlem13  35283  knoppndvlem11  36510  knoppndvlem18  36517  poimirlem23  37637  dvasin  37698  areacirclem1  37702  cntotbnd  37790  lcmineqlem3  42019  lcmineqlem10  42026  lcmineqlem12  42028  lcmineqlem18  42034  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p3  42066  posbezout  42088  aks6d1c1  42104  aks6d1c2lem4  42115  2np3bcnp1  42132  sticksstones12a  42145  sticksstones12  42146  bcled  42166  aks6d1c7lem1  42168  aks6d1c7lem2  42169  3cubeslem1  42672  pell1qrge1  42858  pell1qrgaplem  42861  pell14qrgapw  42864  pellqrex  42867  pellfundgt1  42871  rmspecnonsq  42895  rmspecfund  42897  rmspecpos  42905  monotoddzzfi  42931  jm2.23  42985  limsup10ex  45771  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem1  45999  stoweidlem11  46009  stoweidlem18  46016  stoweidlem34  46032  stoweidlem38  46036  stoweidlem55  46053  wallispi2lem1  46069  stirlinglem1  46072  stirlinglem11  46082  stirlinglem13  46084  fourierdlem11  46116  fourierdlem15  46120  fourierdlem39  46144  fourierdlem41  46146  fourierdlem48  46152  fourierdlem79  46183  ovn0lem  46563  hoidmvlelem2  46594  hoidmvlelem4  46596  smfmullem4  46792  ormkglobd  46873  iccpartgt  47425  flsqrt  47591  2exp340mod341  47731  8exp8mod9  47734  nfermltl8rev  47740  tgblthelfgott  47813  tgoldbach  47815  pgnbgreunbgrlem2lem1  48101  pgnbgreunbgrlem2lem2  48102  nn0eo  48514  seppcld  48915