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

Theorem leidd 11195
Description: 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
leidd.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
leidd (𝜑𝐴𝐴)

Proof of Theorem leidd
StepHypRef Expression
1 leidd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 leid 10725 . 2 (𝐴 ∈ ℝ → 𝐴𝐴)
31, 2syl 17 1 (𝜑𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114   class class class wbr 5042  cr 10525  cle 10665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-pre-lttri 10600
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670
This theorem is referenced by:  zextle  12043  uzind  12062  uzid  12246  ifle  12578  supxrre  12708  infxrre  12717  nn0fz0  13000  fvinim0ffz  13151  flid  13173  modabs2  13268  monoord  13396  leexp2r  13534  facwordi  13645  faclbnd6  13655  pfxsuffeqwrdeq  14051  repswcshw  14165  iseraltlem2  15030  climcndslem1  15195  cvgrat  15230  eirrlem  15548  ruclem2  15576  ruclem9  15582  sadcaddlem  15795  nn0seqcvgd  15903  eulerthlem2  16108  pcidlem  16197  pc2dvds  16204  pcprmpw2  16207  pcmpt  16217  ramub1lem2  16352  prmolefac  16371  prmgaplem4  16379  pgpfi  18721  zntoslem  20246  psrridm  20640  methaus  23125  nmoid  23346  xrsxmet  23412  reconnlem1  23429  metdstri  23454  nmoleub3  23722  ovolctb  24092  ovolicc1  24118  volcn  24208  mbflimsup  24268  mbfi1fseqlem4  24320  itg2const2  24343  itg2uba  24345  itg2splitlem  24350  itg2cnlem1  24363  itg2cnlem2  24364  iblss  24406  itgless  24418  itgsplitioo  24439  dvge0  24607  dvcvx  24621  dvfsumlem2  24628  dvfsumlem3  24629  dvfsumrlim  24632  coe1mul4  24699  deg1mul2  24713  ply1divex  24735  deg1submon1p  24751  coe1termlem  24853  dgradd2  24863  dgrco  24870  aaliou3lem2  24937  abelth2  25035  jensen  25572  logexprlim  25807  bcmono  25859  bcmax  25860  dchrisum0flblem1  26090  pntleml  26193  eupth2  28022  blocnilem  28585  wrdt2ind  30637  fiunelros  31507  dstfrvunirn  31806  ballotlemsi  31846  dnibndlem2  33892  knoppndvlem15  33939  relowlssretop  34741  poimirlem28  35047  mblfinlem2  35057  itg2addnclem  35070  itg2gt0cn  35074  ftc1anclem7  35098  ftc1anclem8  35099  ftc1anc  35100  ssbnd  35188  bfplem1  35222  lcmineqlem4  39285  3lexlogpow5ineq2  39307  metakunt1  39313  metakunt10  39322  metakunt24  39336  2xp3dxp2ge1d  39341  fltnlta  39553  acongeq  39858  expdiophlem1  39896  hbt  40008  dvgrat  40954  ssinc  41663  ssdec  41664  uzublem  42010  fmul01  42165  fmul01lt1lem1  42169  limciccioolb  42206  climxrre  42335  ioccncflimc  42470  icocncflimc  42474  cncfiooicclem1  42478  dvnmul  42528  iblspltprt  42558  itgspltprt  42564  stoweidlem20  42605  stoweidlem51  42636  wallispilem3  42652  fourierdlem10  42702  fourierdlem11  42703  fourierdlem14  42706  fourierdlem17  42709  fourierdlem32  42724  fourierdlem33  42725  fourierdlem41  42733  fourierdlem46  42737  fourierdlem48  42739  fourierdlem49  42740  fourierdlem50  42741  fourierdlem73  42764  fourierdlem76  42767  fourierdlem79  42770  fourierdlem93  42784  fourierdlem102  42793  fourierdlem103  42794  fourierdlem104  42795  fourierdlem107  42798  fourierdlem111  42802  fourierdlem114  42805  etransclem23  42842  rrxsnicc  42885  hsphoidmvle2  43167  hsphoidmvle  43168  hoidmv1lelem1  43173  hoidmv1lelem2  43174  hoidmv1lelem3  43175  hoidmvlelem1  43177  hoidifhspdmvle  43202  ovolval4lem2  43232  iinhoiicc  43256  vonicclem2  43266  2leaddle2  43798  bgoldbachlt  44274  logbpw2m1  44924  dignn0ldlem  44959
  Copyright terms: Public domain W3C validator