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

Theorem leidd 10707
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 10246 . 2 (𝐴 ∈ ℝ → 𝐴𝐴)
31, 2syl 17 1 (𝜑𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103   class class class wbr 4760  cr 10048  cle 10188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-pre-lttri 10123
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193
This theorem is referenced by:  zextle  11563  uzind  11582  uzid  11815  ifle  12142  supxrre  12271  infxrre  12280  nn0fz0  12552  fvinim0ffz  12702  flid  12724  modabs2  12819  monoord  12946  leexp2r  13033  facwordi  13191  faclbnd6  13201  2swrdeqwrdeq  13574  swrdccatid  13618  repswcshw  13679  iseraltlem2  14533  climcndslem1  14701  cvgrat  14735  eirrlem  15052  ruclem2  15081  ruclem9  15087  sadcaddlem  15302  nn0seqcvgd  15406  eulerthlem2  15610  pcidlem  15699  pc2dvds  15706  pcprmpw2  15709  pcmpt  15719  ramub1lem2  15854  prmolefac  15873  prmgaplem4  15881  pgpfi  18141  psrridm  19527  zntoslem  20028  methaus  22447  nmoid  22668  xrsxmet  22734  reconnlem1  22751  metdstri  22776  nmoleub3  23040  ovolctb  23379  ovolicc1  23405  volcn  23495  mbflimsup  23553  mbfi1fseqlem4  23605  itg2const2  23628  itg2uba  23630  itg2splitlem  23635  itg2cnlem1  23648  itg2cnlem2  23649  iblss  23691  itgless  23703  itgsplitioo  23724  dvge0  23889  dvcvx  23903  dvfsumlem2  23910  dvfsumlem3  23911  dvfsumrlim  23914  coe1mul4  23980  deg1mul2  23994  ply1divex  24016  deg1submon1p  24032  coe1termlem  24134  dgradd2  24144  dgrco  24151  aaliou3lem2  24218  abelth2  24316  jensen  24835  logexprlim  25070  bcmono  25122  bcmax  25123  dchrisum0flblem1  25317  pntleml  25420  eupth2  27312  blocnilem  27889  fiunelros  30467  dstfrvunirn  30766  ballotlemsi  30806  dnibndlem2  32696  knoppndvlem15  32744  relowlssretop  33443  poimirlem28  33669  mblfinlem2  33679  itg2addnclem  33693  itg2gt0cn  33697  ftc1anclem7  33723  ftc1anclem8  33724  ftc1anc  33725  ssbnd  33819  bfplem1  33853  acongeq  37969  expdiophlem1  38007  hbt  38119  dvgrat  38930  ssinc  39680  ssdec  39681  uzublem  40072  fmul01  40232  fmul01lt1lem1  40236  limciccioolb  40273  climxrre  40402  ioccncflimc  40518  icocncflimc  40522  cncfiooicclem1  40526  dvnmul  40578  iblspltprt  40609  itgspltprt  40615  stoweidlem20  40657  stoweidlem51  40688  wallispilem3  40704  fourierdlem10  40754  fourierdlem11  40755  fourierdlem14  40758  fourierdlem17  40761  fourierdlem32  40776  fourierdlem33  40777  fourierdlem41  40785  fourierdlem46  40789  fourierdlem48  40791  fourierdlem49  40792  fourierdlem50  40793  fourierdlem73  40816  fourierdlem76  40819  fourierdlem79  40822  fourierdlem93  40836  fourierdlem102  40845  fourierdlem103  40846  fourierdlem104  40847  fourierdlem107  40850  fourierdlem111  40854  fourierdlem114  40857  etransclem23  40894  rrxsnicc  40940  hsphoidmvle2  41222  hsphoidmvle  41223  hoidmv1lelem1  41228  hoidmv1lelem2  41229  hoidmv1lelem3  41230  hoidmvlelem1  41232  hoidifhspdmvle  41257  ovolval4lem2  41287  iinhoiicc  41311  vonicclem2  41321  2leaddle2  41739  pfxsuffeqwrdeq  41833  bgoldbachlt  42128  bgoldbachltOLD  42134  logbpw2m1  42788  fllog2  42789  dignn0ldlem  42823
  Copyright terms: Public domain W3C validator