MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0le1 Structured version   Visualization version   GIF version

Theorem 0le1 11686
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
StepHypRef Expression
1 0re 11165 . 2 0 ∈ ℝ
2 1re 11163 . 2 1 ∈ ℝ
3 0lt1 11685 . 2 0 < 1
41, 2, 3ltleii 11286 1 0 ≤ 1
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5109  0cc0 11059  1c1 11060  cle 11198
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 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396
This theorem is referenced by:  lemulge11  12025  0le2  12263  1eluzge0  12825  x2times  13227  0elunit  13395  1elunit  13396  fldiv4p1lem1div2  13749  1mod  13817  expge0  14013  expge1  14014  faclbnd3  14201  faclbnd4lem1  14202  hashsnle1  14326  hashgt12el  14331  hashgt12el2  14332  01sqrexlem1  15136  sqrt1  15165  sqrt2gt1lt2  15168  sqrtm1  15169  abs1  15191  rlimno1  15547  harmonic  15752  georeclim  15765  geoisumr  15771  fprodge0  15884  fprodge1  15886  ege2le3  15980  sinbnd  16070  cosbnd  16071  cos2bnd  16078  nn0oddm1d2  16275  flodddiv4  16303  sqnprm  16586  zsqrtelqelz  16641  modprm0  16685  pythagtriplem3  16698  prmolefac  16926  abvneg  20336  gzrngunitlem  20885  rge0srg  20891  dscmet  23951  nmoid  24129  iccpnfcnv  24330  iccpnfhmeo  24331  xrhmeo  24332  ncvs1  24544  vitalilem4  24998  vitalilem5  24999  aalioulem3  25717  dvradcnv  25803  abelth2  25824  tanregt0  25918  efif1olem3  25923  dvlog2lem  26030  cxpge0  26061  cxpaddlelem  26127  bndatandm  26302  atans2  26304  cxp2lim  26349  scvxcvx  26358  logdiflbnd  26367  fsumharmonic  26384  lgamgulmlem2  26402  lgamgulmlem3  26403  lgamgulmlem5  26405  mule1  26520  sqff1o  26554  ppiub  26575  dchrabs2  26633  zabsle1  26667  lgslem2  26669  lgsfcl2  26674  lgsdir2lem1  26696  lgsne0  26706  lgsdinn0  26716  m1lgs  26759  chtppilim  26846  rpvmasumlem  26858  dchrisum0flblem1  26879  dchrisum0flblem2  26880  mulog2sumlem2  26906  pntlemb  26968  ostth3  27009  axcontlem2  27963  elntg2  27983  clwwlknon1le1  29094  0ewlk  29107  0pth  29118  nv1  29666  nmosetn0  29756  nmoo0  29782  norm1  30240  nmopsetn0  30856  nmfnsetn0  30869  nmopge0  30902  nmfnge0  30918  nmop0  30977  nmfn0  30978  nmcexi  31017  hstle1  31217  strlem1  31241  strlem5  31246  jplem1  31259  cshw1s2  31870  xrsmulgzz  31925  xrge0slmod  32194  unitssxrge0  32545  xrge0iifcnv  32578  xrge0iifiso  32580  xrge0iifhom  32582  nexple  32672  ddemeas  32899  ballotlem2  33152  ballotlem4  33162  ballotlemic  33170  ballotlem1c  33171  signswch  33237  signsvf0  33256  itgexpif  33283  cvmliftlem13  33954  knoppndvlem11  35038  knoppndvlem18  35045  poimirlem23  36151  dvasin  36212  areacirclem1  36216  cntotbnd  36305  lcmineqlem3  40538  lcmineqlem10  40545  lcmineqlem12  40547  lcmineqlem18  40553  aks4d1p1p4  40578  aks4d1p1p7  40581  aks4d1p3  40585  2np3bcnp1  40602  sticksstones12a  40615  sticksstones12  40616  metakunt1  40627  metakunt28  40654  3cubeslem1  41054  pell1qrge1  41240  pell1qrgaplem  41243  pell14qrgapw  41246  pellqrex  41249  pellfundgt1  41253  rmspecnonsq  41277  rmspecfund  41279  rmspecpos  41287  monotoddzzfi  41313  jm2.23  41367  limsup10ex  44104  ioodvbdlimc1lem2  44263  ioodvbdlimc2lem  44265  stoweidlem1  44332  stoweidlem11  44342  stoweidlem18  44349  stoweidlem34  44365  stoweidlem38  44369  stoweidlem55  44386  wallispi2lem1  44402  stirlinglem1  44405  stirlinglem11  44415  stirlinglem13  44417  fourierdlem11  44449  fourierdlem15  44453  fourierdlem39  44477  fourierdlem41  44479  fourierdlem48  44485  fourierdlem79  44516  ovn0lem  44896  hoidmvlelem2  44927  hoidmvlelem4  44929  smfmullem4  45125  iccpartgt  45709  flsqrt  45875  2exp340mod341  46015  8exp8mod9  46018  nfermltl8rev  46024  tgblthelfgott  46097  tgoldbach  46099  nn0eo  46704  seppcld  47052
  Copyright terms: Public domain W3C validator