Theorem eqidd 2770

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2769	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  nfabd2  2954  neleq1  3076  neleq2  3077  elabd3  3639  nelrdva  3677  sbcbidv  3808  csbie2df  4414  reusngf  4645  rexreusng  4650  reuprg0  4673  iunxdif3  5065  mpteq1  5204  mpteq1i  5206  mpteq2da  5207  mpteq2dva  5208  nfcvb  5348  dfid2  5559  feq23d  6701  f10d  6856  fvmptdv2  7009  elrnrexdm  7085  f1ossf1o  7125  fmptco  7126  cofmpt  7129  fprg  7153  ftpg  7154  fmptsng  7167  fmptsnd  7168  f1dom3fv3dif  7267  f1dom3el3dif  7268  fliftfun  7311  fliftval  7315  nfriotad  7379  cbvmpo  7505  fconstmpo  7528  eqfnov2  7541  ovmpod  7563  ovmpodv2  7569  fvmpopr2d  7573  elovmporab  7657  elovmporab1w  7658  elovmporab1  7659  ovmpt3rab1  7669  elovmpt3rab  7672  ofval  7686  ofrval  7687  offn  7688  fnfvof  7692  off  7693  ofres  7694  coof  7699  ofco  7700  caofref  7706  caofid0l  7708  caofid0r  7709  caofid1  7710  caofid2  7711  caofrss  7714  caoftrn  7716  tfisi  7855  fsplitfpar  8113  fczsupp0  8189  suppssof1  8195  suppofss1d  8200  suppofss2d  8201  fvmpocurryd  8267  fpr3g  8282  iserd  8721  fsetfocdm  8858  ixpsnf1o  8936  mapxpen  9131  dffi3  9391  cantnf0  9644  cantnfp1  9650  cantnflem1  9658  ttrcltr  9685  axcclem  10441  ttukeylem3  10495  fpwwe2lem8  10623  ofsubeq0  12215  ofnegsub  12216  ofsubge0  12217  fzo0to3tp  13781  fzo1to4tp  13783  modsubmod  13965  seqid  14083  seqid2  14084  seqz  14086  seqof  14095  elovmptnn0wrd  14596  ccatdmss  14619  ccatws1ls  14671  pfxsuffeqwrdeq  14735  wrdind  14759  wrd2ind  14760  ccats1pfxeqbi  14779  repswsymb  14811  repswsymball  14816  repswsymballbi  14817  s3eq2  14907  swrds2m  14978  wrdl2exs2  14983  swrd2lsw  14989  wwlktovfo  14995  s3sndisj  15004  s3iunsndisj  15005  relexp0g  15059  relexpsucnnr  15062  relexp1g  15063  rtrclreclem1  15094  rtrclreclem4  15098  dfrtrcl2  15099  sgnneg  15137  rlim2  15547  climcl  15550  rlimcl  15554  clim2  15555  rlimclim1  15596  rlimclim  15597  climrlim2  15598  climuni  15603  rlimres  15609  climeq  15618  2clim  15623  climshftlem  15625  climabs0  15636  climcn1  15643  climcn2  15644  o1of2  15664  o1rlimmul  15670  o1add2  15675  o1mul2  15676  o1sub2  15677  o1dif  15681  climsqz  15692  climsqz2  15693  rlimdiv  15697  isercoll  15719  climsup  15721  climcau  15722  caurcvgr  15725  caucvgb  15731  serf0  15732  iseralt  15736  sumz  15773  fsumss  15776  fsumsplitsn  15795  fsumsplit1  15796  fsumsplitsnun  15806  isumclim3  15810  isummulc2  15813  fsum2dlem  15821  fsumconst  15841  fsumabs  15853  fsumparts  15858  fsumrlim  15863  fsumo1  15864  seqabs  15866  cvgcmpce  15870  fsumiun  15873  ackbijnn  15882  isumshft  15893  isumltss  15902  climcndslem1  15903  climcndslem2  15904  climcnds  15905  mertenslem1  15938  mertenslem2  15939  prod1  15998  fprodss  16002  fprodconst  16032  fprod2dlem  16034  fprodsplitsn  16043  iprodclim3  16054  eftlcl  16163  reeftlcl  16164  eftlub  16165  efsep  16166  effsumlt  16167  eirrlem  16260  rpnnen2lem6  16275  rpnnen2lem7  16276  rpnnen2lem8  16277  rpnnen2lem9  16278  rpnnen2lem12  16281  2tp1odd  16410  sadasslem  16528  smupvallem  16541  smumul  16551  alginv  16633  algfx  16638  cncongr1  16725  qnumdencoprm  16804  qeqnumdivden  16805  vdwlem1  17041  vdwlem12  17052  vdwlem13  17053  prmodvdslcmf  17107  prmgap  17119  prmgaplcm  17120  prmgapprmo  17122  setsexstruct2  17235  setsstruct  17236  prdssca  17509  prdsbas  17510  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  prdsip  17514  prdsle  17515  prdsds  17517  prdstset  17519  prdshom  17520  prdsco  17521  prdsvscafval  17533  prdsdsval2  17537  prdsdsval3  17538  pwsle  17546  pwsleval  17547  pwsvscaval  17549  imasbas  17566  imasds  17567  imasplusg  17571  imasmulr  17572  imassca  17573  imasvsca  17574  imasip  17575  imastset  17576  imasle  17577  imasvscafn  17591  imasvscaval  17592  qusin  17598  xpsvsca  17631  iscat  17728  iscatd  17729  iscatd2  17737  0catg  17744  homfeq  17750  homfeqd  17751  comfffval2  17757  comffval2  17758  comfeq  17762  comfeqd  17763  oppccatid  17775  2oppccomf  17781  moni  17793  rcaninv  17851  ssc2  17879  ssctr  17882  ssceq  17883  subcssc  17897  subccat  17905  subsubc  17910  funcres  17953  funcres2  17955  idfusubc  17957  funcres2c  17960  idffth  17992  cofull  17993  cofth  17994  ressffth  17997  isnat  18007  fuccofval  18019  fuccatid  18029  fucpropd  18037  elhomai  18090  coafval  18121  setcval  18134  setcbas  18135  setchomfval  18136  setccofval  18139  setcco  18140  setccatid  18141  setcepi  18145  funcsetcres2  18150  catcval  18157  catcbas  18158  catchomfval  18159  catccofval  18161  catcco  18162  catccatid  18163  catcfuccl  18175  estrcval  18180  estrcbas  18181  estrchomfval  18182  estrccofval  18185  estrcco  18186  estrccatid  18188  estrreslem2  18194  fullestrcsetc  18207  fullsetcestrc  18222  xpcbas  18234  xpchomfval  18235  xpccofval  18238  xpccatid  18244  prfval  18255  catcxpccl  18263  xpcpropd  18264  evlfval  18273  curfval  18279  curf1  18281  curf12  18283  curf2  18285  curf2val  18286  hofval  18308  hof2fval  18311  hofcllem  18314  oppchofcl  18316  oppcyon  18325  oyoncl  18326  yonedalem4a  18331  yonedalem4b  18332  yonedainv  18337  oduposb  18383  joinval  18431  meetval  18445  isdlat  18578  ipopos  18592  pfxchn  18666  chnind  18677  chnso  18680  chnccats1  18681  chnccat  18682  chnrev  18683  gsumpropd  18736  gsumpropd2lem  18737  gsumval1  18741  gsumval2a  18743  issgrp  18778  issgrpd  18788  prdssgrpd  18791  ismndd  18814  mndprop  18818  prdsmndd  18828  imasmnd2  18832  insubm  18877  mhmima  18884  frmdbas  18911  frmdmnd  18918  efmnd  18929  smndex1gid  18963  smndex1gidOLD  18964  smndex1n0mnd  18974  smndex2dlinvh  18979  sgrpnmndex  18994  resgrpplusfrn  19017  grpprop  19019  grpsubfval  19050  grpsubfvalALT  19051  grpsubpropd  19111  prdsgrpd  19116  imasgrp2  19121  imasgrp  19122  imasgrpf1  19123  mulgfval  19135  mulgfvalALT  19136  mulgnngsum  19145  mulgnn0gsum  19146  mulgpropd  19182  subgsub  19205  eqgfval  19244  qusgrp  19257  ghmqusnsglem1  19350  ghmqusnsglem2  19351  ghmqusnsg  19352  ghmquskerlem1  19353  ghmquskerlem2  19355  ghmquskerlem3  19356  ghmqusker  19357  oppgmnd  19424  oppgmndb  19425  oppggrp  19427  oppggrpb  19428  symgval  19441  symg1bas  19461  symg2bas  19463  symgvalstruct  19467  symggrp  19470  gsmsymgrfixlem1  19497  gsmsymgreqlem2  19501  symgfixels  19504  symgsssg  19537  symgfisg  19538  psgnunilem4  19567  psgnvalii  19579  oppglsm  19712  lsmelvalmi  19722  efgi0  19790  efgi1  19791  efgtf  19792  efgval2  19794  efginvrel2  19797  frgp0  19830  frgpup3lem  19847  ablprop  19863  subcmn  19907  gex2abl  19921  prdscmnd  19931  qusabl  19935  abl1  19936  cygabl  19961  gsumzf1o  19982  gsumzaddlem  19991  gsumzsplit  19997  gsumconst  20004  gsumconstf  20005  gsummptshft  20006  gsummhm2  20009  gsummptmhm  20010  gsumzunsnd  20026  gsumunsnfd  20027  gsumpt  20032  gsummptf1o  20033  gsummptun  20034  gsum2dlem2  20041  gsumcom2  20045  nn0gsumfz  20054  dprdval  20075  dprdssv  20088  dprdfeq0  20094  dprdsubg  20096  dprdspan  20099  dprdz  20102  subgdmdprd  20106  subgdprd  20107  gsumle  20215  elmgplsmd  20229  isrng  20232  isrngd  20251  prdsrngd  20254  imasrng  20255  issrg  20270  isring  20319  ringabl  20364  ringprop  20373  isringd  20374  prdsringd  20402  prdscrngd  20403  prds1  20404  pwspjmhmmgpd  20409  imasring  20412  opprrng  20427  opprrngb  20428  opprringb  20430  dvrfval  20484  rnghmf1o  20534  c0mgm  20541  c0mhm  20542  c0snmgmhm  20544  c0snmhm  20545  rngisomring1  20550  rhmf1o  20573  pwsco1rhm  20584  pwsco2rhm  20585  zrrnghm  20621  rhmimasubrng  20651  pwsdiagrhm  20692  rngcbas  20706  rngchomfval  20707  dfrngc2  20713  rnghmsscmap2  20714  rnghmsscmap  20715  rngccat  20719  rngcid  20720  funcrngcsetc  20725  funcrngcsetcALT  20726  zrinitorngc  20727  zrtermorngc  20728  ringcbas  20735  ringchomfval  20736  dfringc2  20742  rhmsscmap2  20743  rhmsscmap  20744  ringccat  20748  ringcid  20749  rngcresringcat  20754  funcringcsetc  20759  zrtermoringc  20760  rhmsubc  20774  drngprop  20828  isdrngd  20847  isdrngrd  20848  isdrngdOLD  20849  isdrngrdOLD  20850  abvtrivd  20913  idsrngd  20937  suborng  20957  islmodd  20965  lmodabl  21008  lss1  21037  lsssn0  21047  islss3  21058  lss1d  21062  lssintcl  21063  prdslmodd  21068  idlmhm  21140  invlmhm  21141  lmhmvsca  21144  lbsextlem2  21261  sralmod  21286  sralmod0  21287  rlm0  21294  rlmvneg  21305  rnglidlmsgrp  21354  rnglidlrng  21355  qus2idrng  21383  crngridl  21390  quscrng  21394  rhmqusnsg  21396  rngqiprngimf1lem  21405  rngqiprngimf1  21411  qsidomlem1  21449  qsidomlem2  21450  absabv  21543  pzriprnglem10  21609  zrhpropd  21633  fermltlchr  21648  znzrh  21661  znbas  21662  zncrng  21663  znzrhfo  21666  znf1o  21670  frgpcyg  21692  evpmodpmf1o  21715  isphld  21773  phlpropd  21774  phssip  21777  phlssphl  21778  pjfval  21825  dsmmval  21853  dsmmsubg  21862  frlmip  21897  frlmipval  21898  frlmphllem  21899  frlmphl  21900  islindf  21931  islindf4  21957  isassa  21975  isassad  21984  issubassa3  21985  asclfval  21997  ressascl  22015  psrval  22034  psrbaglesupp  22041  psrbagcon  22044  psrbaglefi  22045  psrbagleadd1  22047  psrbagconf1o  22048  gsumbagdiaglem  22050  psrass1lem  22052  psrbas  22053  psrplusg  22056  psrmulr  22061  psrsca  22066  psrvscafval  22067  psrvscaval  22069  psrlmod  22078  psrlidm  22080  psrdi  22083  psrdir  22084  psrcom  22086  psrring  22088  psrassa  22091  mplsubglem  22117  mpllsslem  22118  mplvscaval  22134  mplcoe1  22157  mplcoe3  22158  mplcoe5  22160  opsrcrng  22179  opsrassa  22180  mplmon2  22181  evlslem2  22199  evlslem1  22202  evlsvvval  22213  mplmapghm  22242  evlsmaprhm  22251  selvvvval  22262  selvadd  22263  selvmul  22264  mhpmulcl  22281  psdffval  22289  psdmplcl  22294  psdadd  22295  psdmul  22298  psdmvr  22301  ply1lss  22325  ply1subrg  22326  opsr0  22347  opsr1  22348  subrgply1  22361  psrplusgpropd  22364  psropprmul  22366  opsrring  22373  opsrlmod  22374  ply1mpl0  22385  ply1mpl1  22387  coe1z  22393  coe1mul2  22399  coe1tm  22403  coe1sclmulfv  22413  ply1coe  22427  evls1rhm  22451  evls1sca  22452  evl1rhm  22461  evl1sca  22463  evl1expd  22474  evl1gsumdlem  22485  evl1varpw  22490  evls1maplmhm  22506  mamufval  22518  mamudi  22529  mamudir  22530  mat0  22543  matinvg  22544  matlmod  22555  matinvgcell  22561  matring  22569  matassa  22570  mat0dimcrng  22596  mat1dim0  22599  mat1f1o  22604  dmatmulcl  22626  scmatval  22630  scmatscmiddistr  22634  scmataddcl  22642  scmatsubcl  22643  scmatmulcl  22644  scmatlss  22651  scmatrhmcl  22654  1mavmul  22674  mavmul0  22678  marepvfval  22691  submafval  22705  submaval  22707  mdetleib2  22714  mdet0pr  22718  m1detdiag  22723  mdetrsca  22729  mdetrsca2  22730  mdetrlin2  22733  mdetralt  22734  mdetralt2  22735  mdetunilem2  22739  mdetunilem5  22742  mdetunilem9  22746  mdetuni0  22747  m2detleib  22757  madufval  22763  symgmatr01lem  22779  symgmatr01  22780  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  smadiadetlem3  22794  smadiadetglem2  22798  smadiadetr  22801  mat2pmatghm  22856  cpm2mfval  22875  m2cpminvid  22879  m2cpminvid2lem  22880  m2cpminvid2  22881  decpmatval  22891  decpmataa0  22894  decpmatmul  22898  pmatcollpw1  22902  pmatcollpw2lem  22903  monmatcollpw  22905  pmatcollpwlem  22906  pmatcollpw  22907  pmatcollpwscmatlem2  22916  pm2mpval  22921  pm2mpcl  22923  pm2mpf1  22925  mptcoe1matfsupp  22928  mp2pm2mplem3  22934  mp2pm2mplem4  22935  pm2mpghm  22942  pm2mpmhmlem2  22945  chpmat1dlem  22961  chp0mat  22972  fvmptnn04ifa  22976  fvmptnn04ifb  22977  fvmptnn04ifc  22978  fvmptnn04ifd  22979  cpmadugsumlemB  23000  chcoeffeqlem  23011  epttop  23135  ordtbas2  23317  ordtopn1  23320  ordtopn2  23321  lmss  23424  2ndci  23574  2ndcsep  23585  dis2ndc  23586  1stcelcls  23587  dissnlocfin  23655  ptbasid  23701  xkoopn  23715  prdstopn  23754  ptrescn  23765  txlm  23774  lmcn2  23775  tx1stc  23776  xkopt  23781  cnmpt2c  23796  cnmptk1  23807  cnmpt1k  23808  cnmptkk  23809  qtopeu  23842  txswaphmeolem  23930  xpstopnlem1  23935  ptcmpfi  23939  xkohmeo  23941  rnelfmlem  24078  rnelfm  24079  hauspwpwf1  24113  lmflf  24131  flfcnp2  24133  alexsubb  24172  tmdgsum  24221  tgpconncomp  24239  qustgphaus  24249  tsmsfbas  24254  tsmspropd  24258  tsmssplit  24278  tsmsxplem1  24279  tsmsxplem2  24280  ustuqtop4  24370  imasdsf1olem  24499  blfvalps  24509  stdbdxmet  24641  met2ndci  24648  prdsxmslem2  24655  metustexhalf  24682  cfilucfil  24685  restmetu  24696  nmfval  24714  nmpropd  24720  nmpropd2  24721  subgnm  24759  tng0  24769  tngnm  24777  tnggrpr  24781  tngngp3  24782  tngnrg  24800  sranlm  24810  qdensere  24895  mpomulcn  24995  fsumcn  24998  cncfcompt2  25036  cncfmpt1f  25042  negfcncf  25051  oprpiece1res2  25080  htpyid  25105  phtpyid  25117  pcofval  25138  pcopt2  25151  om1bas  25159  om1plusg  25162  om1tset  25163  pi1bas  25166  pi1bas2  25169  pi1eluni  25170  pi1bas3  25171  pi1cpbl  25172  pi1addf  25175  pi1addval  25176  pi1grplem  25177  pi1xfr  25183  pi1xfrcnvlem  25184  pi1coghm  25189  cphassr  25340  tcphphl  25355  ipcau2  25362  cphipval  25371  lmnn  25391  iscau  25404  cmetcaulem  25416  iscmet3lem1  25419  causs  25426  lmclim  25431  srabn  25488  rrxprds  25517  rrxip  25518  rrxcph  25520  rrxds  25521  rrxmvallem  25532  rrxmval  25533  rrxdsfival  25541  ehl2eudisval  25551  divcncf  25575  ovollb2lem  25616  ovolfiniun  25629  ovolicc2lem4  25648  shftmbl  25666  volfiniun  25675  ioombl1lem4  25689  uniioombllem2  25711  uniioombllem6  25716  vitalilem4  25739  mbfmulc2lem  25775  mbfmulc2re  25776  mbfneg  25778  mbfaddlem  25788  mbfadd  25789  mbfsub  25790  mbfmulc2  25791  0plef  25800  0pledm  25801  itg1ge0  25814  i1faddlem  25821  i1fmullem  25822  i1fmulclem  25830  itg1mulc  25832  itg1lea  25840  itg1le  25841  mbfi1flimlem  25850  mbfmullem2  25852  mbfmul  25854  xrge0f  25859  itg2ge0  25863  itg2const  25868  itg2const2  25869  itg2uba  25871  itg2lea  25872  itg2splitlem  25876  itg2split  25877  itg2monolem1  25878  itg2mono  25881  itg2i1fseqle  25882  itg2i1fseq  25883  itg2addlem  25886  itg2gt0  25888  itg2cnlem1  25889  itg2cnlem2  25890  isibl2  25894  iblitg  25896  itgcl  25912  ibl0  25915  iblcnlem1  25916  itgcnlem  25918  iblss  25933  iblss2  25934  i1fibl  25936  itgitg1  25937  itgle  25938  itgeqa  25942  iblconst  25946  ibladdlem  25948  ibladd  25949  itgaddlem1  25951  itgfsum  25955  iblabslem  25956  iblabs  25957  iblabsr  25958  iblmulc2  25959  itgmulc2lem1  25960  itgsplit  25964  bddmulibl  25967  bddibl  25968  bddiblnc  25970  limccnp2  26020  limcco  26021  dvidlem  26043  dvcnp2  26048  dvaddbr  26066  dvmulbr  26067  dvaddf  26070  dvcmulf  26073  dvexp  26081  dvmptadd  26088  dvmptmul  26089  dvmptco  26100  dvmptfsum  26103  dvcnvlem  26104  dvef  26108  rolle  26118  mvth  26120  dvlip  26121  dvlipcn  26122  lhop1lem  26141  itgsubstlem  26176  itgpowd  26178  ply1divalg2  26265  uc1pmon1p  26278  q1pval  26281  r1pval  26284  elply2  26322  elplyr  26327  plypf1  26338  plyaddlem1  26339  coeeulem  26350  plyco  26367  coeaddlem  26375  coemulc  26381  dgradd2  26394  dgrcolem1  26399  dgrcolem2  26400  dgrco  26401  ofmulrt  26409  plymul02  26410  plymulidp  26412  plydivlem3  26425  plydivlem4  26426  plyrem  26435  iaa  26455  aareccl  26456  aannenlem2  26459  aaliou3lem3  26474  aaliou3lem7  26479  taylfval  26488  taylply2  26497  dvntaylp  26500  taylthlem2  26503  ulmclm  26516  ulmres  26517  ulmshftlem  26518  ulm0  26520  ulmcau  26524  ulmss  26526  ulmbdd  26527  ulmcn  26528  mtest  26533  mtestbdd  26534  iblulm  26536  itgulm  26537  pserulm  26551  pserdvlem2  26557  abelthlem5  26564  abelthlem6  26565  abelthlem8  26568  abelthlem9  26569  sincn  26573  coscn  26574  efcvx  26578  efabl  26681  logfac  26732  logcn  26778  chordthmlem  26963  chordthmlem5  26967  mcubic  26978  leibpi  27073  efrlim  27100  amgmlem  27120  lgamgulmlem2  27160  basellem7  27217  basellem9  27219  musum  27321  chtublem  27341  logexprlim  27355  dchrbas  27365  dchr1cl  27381  dchrabl  27384  dchrfi  27385  dchrhash  27401  bposlem6  27419  lgsdir2lem5  27459  gausslemma2dlem1  27496  lgseisenlem2  27506  lgseisenlem3  27507  lgseisenlem4  27508  lgsquad2lem2  27515  2lgslem1b  27522  2lgslem3b1  27531  2lgslem3c1  27532  2lgsoddprmlem4  27545  2sqlem8  27556  2sqlem11  27559  2sqreulem1  27576  2sqreunnlem1  27579  chtppilimlem2  27604  chebbnd2  27607  chpchtlim  27609  chpo1ub  27610  vmadivsum  27612  rpvmasumlem  27617  dchrisum0re  27643  dchrisum0  27650  mudivsum  27660  selberglem1  27675  selberglem2  27676  selberg2lem  27680  selberg2  27681  pntrsumo1  27695  selbergr  27698  abvcxp  27745  nosupfv  27836  noinffv  27851  madecut  28042  elons2  28417  oncutlt  28423  oniso  28430  seqsfn  28468  seqs1  28469  seqsp1  28470  n0fincut  28514  zcuts  28566  twocut  28582  expsval  28584  pw2cut2  28621  z12addscl  28636  z12shalf  28639  z12zsodd  28641  istrkgld  28694  istrkg2ld  28695  tgsegconeq  28721  tgbtwnouttr2  28730  ercgrg  28752  cgr3id  28754  tgbtwnxfr  28765  motgrp  28778  tgbtwnconn1lem3  28809  legov  28820  legid  28822  btwnleg  28823  legbtwn  28829  mirreu3  28893  mirinv  28905  miduniq1  28925  colmid  28927  krippenlem  28929  israg  28936  ragcgr  28946  motrag  28947  perpneq  28953  isperp2  28954  isperp2d  28955  footexALT  28957  footexlem1  28958  footexlem2  28959  foot  28961  perprag  28966  perpdragALT  28967  colperpexlem1  28970  mideulem2  28974  opphllem2  28988  opphllem3  28989  opphllem4  28990  plngval  29017  midbtwn  29046  midcom  29049  mirmid  29050  lmieu  29051  lmif  29052  islmib  29054  lmilmi  29056  lmieq  29058  lmiinv  29059  lmiisolem  29063  hypcgrlem1  29066  hypcgrlem2  29067  lmiopp  29069  trgcopyeu  29074  iscgra  29077  iscgra1  29078  iscgrad  29079  sacgr  29099  isinag  29110  isinagd  29111  inagflat  29112  inaghl  29117  isleag  29119  isleagd  29120  prlngref  29145  ttgval  29165  cchhllem  29177  usgredg4  29508  ushgredgedg  29520  ushgredgedgloop  29522  usgrstrrepe  29526  uspgr1e  29535  uhgrspan1  29594  usgrres1  29606  nbgrnself  29650  nbusgredgeu  29657  cusgrfilem2  29747  finsumvtxdg2size  29841  finsumvtxdgeven  29843  wlk1walk  29929  uspgr2wlkeq  29936  uspgr2wlkeqi  29938  wlkonwlk  29951  wlkonwlk1l  29952  usgr2trlncl  30050  crctcshwlkn0lem7  30106  wwlksnredwwlkn  30185  wwlksnextbij  30192  wwlksnextprop  30202  wwlksnwwlksnon  30205  elwwlks2ons3im  30244  clwlkclwwlk2  30295  clwlkclwwlkfo  30301  clwlkclwwlkf1  30302  clwwlkwwlksb  30346  clwlknf1oclwwlkn  30376  clwwlknonmpo  30381  clwwlknonex2lem2  30400  0pthon1  30420  uhgr3cyclex  30474  iseupth  30493  eupth0  30506  eupth2lem2  30511  frgr3vlem1  30565  3vfriswmgrlem  30569  2clwwlk2clwwlklem  30638  wlkl0  30659  numclwlk1lem2  30662  grpodivfval  30827  dipfval  30995  ipval2  31000  lnoval  31045  minvecolem3  31169  h2hcau  31272  h2hlm  31273  opsqrlem3  32435  opsqrlem4  32436  foresf1o  32791  disjnf  32856  disjdifprg  32861  iundisjf  32875  br8d  32894  fnfvor  32895  ofrco  32896  ofrn2  32926  off2  32927  ofresid  32928  fmptcof2  32943  aciunf1  32949  ofpreima  32951  f1ocnt  33086  prodindf  33123  indf1ofs  33127  wrdfsupp  33198  wrdpmcl  33199  pfxf1  33203  s1f1  33204  wrdt2ind  33214  swrdrn2  33215  ressnm  33225  abvpropd2  33226  ismntd  33245  dfmgc2lem  33256  pwrssmgc  33261  gsummpt2d  33310  gsummptf1od  33316  gsummptfsf1o  33321  gsumhashmul  33328  gsumwrd2dccat  33339  wrdpmtrlast  33354  psgnfzto1stlem  33361  fzto1st1  33363  tocycfv  33370  cycpmcl  33377  tocycf  33378  tocyc01  33379  cycpmco2f1  33385  cycpmco2rn  33386  cycpmco2lem1  33387  cycpmco2lem2  33388  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  cycpm3cl2  33397  cycpmconjv  33403  tocyccntz  33405  cyc3evpm  33411  cyc3genpm  33413  cycpmgcl  33414  cycpmconjslem2  33416  cyc3conja  33418  sgnsv  33421  inftmrel  33441  isinftm  33442  submarchi  33447  isslmd  33463  urpropd  33491  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem4  33506  elrgspn  33507  elrgspnsubrun  33510  erlval  33519  rlocval  33520  rlocbas  33529  rlocaddval  33530  rlocmulval  33531  rloccring  33532  rlocinvunit  33536  rlocisunit  33537  resv0g  33601  resvcmn  33603  imaslmod  33616  imasmhm  33617  imasghm  33618  imasrhm  33619  imaslmhm  33620  znfermltl  33624  islinds5  33625  ellspds  33626  linds2eq  33638  lindfpropd  33639  nsgmgclem  33664  nsgmgc  33665  rhmquskerlem  33677  elrspunsn  33681  idlinsubrg  33683  opprqusbas  33715  qsdrngi  33722  dflring2  33728  rprmval  33751  rprmnz  33755  rprmnunit  33756  unitmulrprm  33763  1arithidomlem1  33770  1arithidomlem2  33771  1arithidom  33772  1arithufdlem3  33781  dfufd2lem  33784  ply1dg1rt  33815  ply1mulrtss  33817  ply1degltlss  33831  ply1gsumz  33834  r1pquslmic  33845  0mplrim  33849  selvply1rhmlemb  33854  selvply1rhmlem2  33856  selvply1rhmlem4  33858  mplvrpmfgalem  33879  psrmonprod  33887  esplyfvaln  33909  esplyind  33910  vietalem  33914  sra1r  33916  sradrng  33917  sraidom  33918  srasubrg  33919  resssra  33922  drgext0g  33925  drgextlsp  33929  rlmdim  33945  tnglvec  33947  tngdim  33948  matdim  33950  ply1degltdimlem  33957  lbsdiflsp0  33961  dimkerim  33962  fedgmullem2  33965  lactlmhm  33969  extdg1id  34001  ccfldsrarelvec  34006  ccfldextdgrr  34007  fldextrspunlsplem  34008  fldextrspunlsp  34009  fldextrspunlem1  34010  fldextrspunfld  34011  fldextrspunlem2  34012  extdgfialglem1  34027  extdgfialglem2  34028  irredminply  34051  algextdeglem3  34054  algextdeglem4  34055  algextdeglem8  34059  constrsslem  34076  constrext2chnlem  34085  constrcon  34109  2sqr3nconstr  34116  cos9thpinconstrlem2  34125  1smat1  34139  submatres  34141  submateq  34144  lmatcl  34151  mdetlap1  34161  madjusmdetlem3  34164  circtopn  34172  locfinref  34176  tpr2rico  34247  lmdvglim  34289  qqhval  34307  esumeq1  34369  esumeq1d  34370  esumeq2d  34372  esumf1o  34385  esumsplit  34388  esumadd  34392  gsumesum  34394  esumlub  34395  esumaddf  34396  esumcst  34398  esumsnf  34399  esumpinfval  34408  esumcocn  34415  esummulc1  34416  esumcvg  34421  esum2d  34428  ofcval  34434  ofcfn  34435  ofcfeqd2  34436  ofcf  34438  ofcfval4  34440  ofcof  34442  sigapildsys  34497  sxval  34525  measvunilem0  34548  measvuni  34549  measiun  34553  meascnbl  34554  measinb  34556  volmeas  34566  sxbrsiga  34625  omssubadd  34635  fiunelcarsg  34651  itgeq12dv  34661  sitgval  34667  eulerpartlems  34695  eulerpartgbij  34707  eulerpartlemn  34716  sseqf  34727  sseqp1  34730  totprobd  34761  probfinmeasb  34763  probmeasb  34765  rrvadd  34787  dstfrvclim1  34813  gsumnunsn  34876  signsply0  34883  fdvneggt  34932  fdvnegge  34934  itgexpif  34938  reprpmtf1o  34958  circlemethhgt  34975  logdivsqrle  34982  hgt750lemg  34986  hgt750lemb  34988  hgt750lema  34989  f1resfz0f1d  35538  2cycl2d  35564  quartfull  35590  sconnpi1  35664  cvmliftphtlem  35742  cvmlift3lem2  35745  satfv1  35788  satfdmlem  35793  satf0suc  35801  satf0op  35802  sat1el2xp  35804  fmla  35806  fmlasuc0  35809  fmlafvel  35810  fmlasuc  35811  fmla1  35812  satffunlem1lem2  35828  satffunlem2lem2  35831  sategoelfvb  35844  satfv1fvfmla1  35848  2goelgoanfmla1  35849  elmsubrn  35953  msubco  35956  mthmpps  36007  r1peuqusdeg1  36068  sinccvg  36098  circum  36099  br8  36181  br4  36183  brsegle  36533  hilbert1.1  36579  itgeq2sdv  36655  ditgeq3sdv  36658  cbvoprab23davw  36711  cbvoprab13davw  36712  trer  36750  knoppcnlem4  37008  knoppcnlem9  37013  knoppcnlem11  37015  knoppndvlem6  37029  knoppf  37047  bj-imdirco  37756  bj-fvmptunsn2  37824  bj-finsumval0  37851  exrecfnlem  37947  finxpreclem1  37957  matunitlindflem1  38189  matunitlindflem2  38190  poimirlem1  38194  poimirlem2  38195  poimirlem4  38197  poimirlem5  38198  poimirlem6  38199  poimirlem7  38200  poimirlem10  38203  poimirlem11  38204  poimirlem12  38205  poimirlem16  38209  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem22  38215  poimirlem23  38216  poimirlem28  38221  poimirlem29  38222  poimirlem31  38224  broucube  38227  mblfinlem2  38231  volsupnfl  38238  itg2addnclem  38244  itg2addnclem3  38246  itg2addnc  38247  itg2gt0cn  38248  ibladdnclem  38249  itgaddnclem1  38251  itgaddnc  38253  iblabsnclem  38256  iblabsnc  38257  iblmulc2nc  38258  itgmulc2nclem1  38259  itgmulc2nclem2  38260  itgmulc2nc  38261  ftc1anclem2  38267  ftc1anclem4  38269  ftc1anclem5  38270  ftc1anclem6  38271  ftc1anclem7  38272  ftc1anclem8  38273  ftc1anc  38274  areacirc  38286  unirep  38287  upixp  38302  sdc  38317  lmclim2  38331  geomcau  38332  caures  38333  caushft  38334  prdsbnd2  38368  heibor1lem  38382  bfplem2  38396  rrncmslem  38405  isrngo  38470  iuneq2f  38729  dmec2d  38884  lflset  39757  islfld  39760  lfladdcl  39769  lflvscl  39775  lkrsc  39795  eqlkr2  39798  lshpkrlem1  39808  ldualset  39823  ldualvaddval  39829  ldualvsval  39836  ldualgrplem  39843  lduallmodlem  39850  cmtfvalN  39908  isoml  39936  iscvlat  40021  llni2  40210  lplni2  40235  lvoli3  40275  lvoli2  40279  paddfval  40495  lhpset  40693  ltrnfset  40815  trlfset  40858  cdleme21k  41036  cdlemeiota  41283  tgrpfset  41442  tgrpset  41443  tgrpabl  41449  tendo0cbv  41484  tendo02  41485  erngfset  41497  erngset  41498  erngfset-rN  41505  erngset-rN  41506  cdlemkid5  41633  cdlemkid  41634  dvafset  41702  dvaset  41703  diaffval  41728  dialss  41744  diaf11N  41747  dvhfset  41778  dvhset  41779  docaffvalN  41819  dibfval  41839  dibf11N  41859  diblss  41868  diclss  41891  dihord2cN  41919  dihord11b  41920  dihffval  41928  dihord6apre  41954  dihglblem2aN  41991  dihglblem2N  41992  dihjatcclem4  42119  lclkrs  42237  mapdh6dN  42437  mapdh6eN  42438  mapdh6fN  42439  mapdh6jN  42443  hvmapffval  42456  hvmapfval  42457  mapdh8a  42473  mapdh8ad  42477  mapdh8d0N  42480  mapdh8d  42481  mapdh8i  42484  mapdh8j  42485  mapdh9a  42487  mapdh9aOLDN  42488  hdmap1l6d  42511  hdmap1l6e  42512  hdmap1l6f  42513  hdmap1l6j  42517  hdmapval2  42530  hdmapeveclem  42532  hdmapval3lemN  42535  hdmap11lem1  42539  hgmapfval  42584  hlhils0  42643  hlhils1N  42644  hlhillvec  42649  hlhildrng  42650  hlhil0  42653  hlhillsm  42654  rhmzrhval  42663  zndvdchrrhm  42664  3factsumint1  42712  lcmineqlem12  42731  aks4d1p1p4  42762  aks4d1p1p7  42765  aks4d1p9  42779  isprimroot  42784  primrootsunit1  42788  posbezout  42791  primrootscoprbij  42793  remexz  42795  aks6d1c1p2  42800  aks6d1c1p3  42801  aks6d1c1p4  42802  aks6d1c1p5  42803  aks6d1c1p7  42804  evl1gprodd  42808  aks6d1c2p2  42810  hashscontpow  42813  aks6d1c2lem4  42818  aks6d1c2  42821  aks6d1c5lem2  42829  aks6d1c5  42830  deg1gprod  42831  2np3bcnp1  42835  2ap1caineq  42836  sticksstones8  42844  sticksstones10  42846  sticksstones12a  42848  sticksstones12  42849  sticksstones17  42854  sticksstones18  42855  sticksstones19  42856  sticksstones21  42858  sticksstones22  42859  aks6d1c6lem1  42861  aks6d1c6lem2  42862  aks6d1c6lem4  42864  aks6d1c6isolem1  42865  aks5lem3a  42880  grpods  42885  unitscyglem1  42886  unitscyglem2  42887  ofun  42930  redivcan2d  43132  redivcan3d  43133  sn-rediv0d  43138  sn-redividd  43139  rhmpsr1  43242  evlselv  43247  fsuppind  43248  mhphf  43255  3cubeslem3r  43344  eldiophb  43414  eldioph  43415  eldioph3  43423  rabren3dioph  43468  pellqrexplicit  43530  rmxycomplete  43570  rmxynorm  43571  acongrep  43633  jm2.26a  43653  jm2.26  43655  fnwe2lem2  43704  fnwe2lem3  43705  aomclem5  43711  aomclem8  43714  imasgim  43753  isnumbasgrplem1  43754  hbtlem5  43781  dgrsub2  43788  rgspnid  43821  rngunsnply  43822  mendval  43832  mendring  43841  mendlmod  43842  mendassa  43843  nnoeomeqom  43965  tfsconcatb0  43997  oaun3  44035  safesnsupfilb  44070  fsovrfovd  44661  fsovcnvlem  44665  mnring0gd  44871  mnringlmodd  44876  mnringmulrcld  44878  colleq1  44890  colleq2  44891  dvgrat  44948  radcnvrat  44950  hashnzfzclim  44958  caofcan  44959  ofsubid  44960  ofmul12  44961  ofdivrec  44962  ofdivcan4  44963  ofdivdiv2  44964  expgrowth  44971  binomcxplemnn0  44985  binomcxplemrat  44986  binomcxplemdvbinom  44989  binomcxplemnotnn0  44992  wessf1ornlem  45829  disjf1o  45835  ssnnf1octb  45838  mapss2  45848  icof  45861  mpteq1df  45877  infnsuprnmpt  45891  upbdrech  45950  divcan8d  45957  dmmcand  45958  suplesup  45981  ssuzfz  45991  supsubc  45995  xralrple2  45996  fprodabs2  46237  fprodcn  46242  clim1fr1  46243  climrec  46245  climexp  46247  climinf  46248  climsuse  46250  climneg  46252  divcnvg  46269  sumnnodd  46272  clim2f  46276  clim2f2  46310  fnlimfvre  46314  climleltrp  46316  climreclmpt  46324  climinf2mpt  46354  climinfmpt  46355  supcnvlimsup  46380  climuzlem  46383  climisp  46386  climrescn  46388  climxrrelem  46389  climxrre  46390  liminfvalxrmpt  46426  liminflbuz2  46455  cncfcompt  46523  dvsinax  46553  fperdvper  46559  dvcosax  46566  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnxpaek  46582  dvnmul  46583  dvmptfprodlem  46584  dvnprodlem1  46586  dvnprodlem2  46587  dvnprodlem3  46588  iblempty  46605  iblsplit  46606  itgcoscmulx  46609  itgsincmulx  46614  itgsubsticc  46616  sublevolico  46624  stoweidlem2  46642  stoweidlem17  46657  stoweidlem21  46661  stoweidlem32  46672  stoweidlem46  46686  stoweidlem55  46695  wallispi  46710  wallispi2lem1  46711  wallispi2lem2  46712  wallispi2  46713  stirlinglem3  46716  dirkercncflem2  46744  dirkercncflem4  46746  fourierdlem16  46763  fourierdlem18  46765  fourierdlem21  46768  fourierdlem22  46769  fourierdlem39  46786  fourierdlem53  46799  fourierdlem58  46804  fourierdlem59  46805  fourierdlem62  46808  fourierdlem73  46819  fourierdlem76  46822  fourierdlem81  46827  fourierdlem83  46829  fourierdlem93  46839  fourierdlem101  46847  fourierdlem103  46849  fourierdlem104  46850  fourierdlem111  46857  fourierdlem112  46858  fouriersw  46871  elaa2lem  46873  etransclem18  46892  etransclem32  46906  etransclem33  46907  etransclem46  46920  etransclem48  46922  rrxtopnfi  46927  rrxunitopnfi  46932  salincl  46964  sge0z  47015  sge0tsms  47020  sge0snmpt  47023  sge0sup  47031  sge0resplit  47046  sge0ss  47052  sge0isum  47067  sge0xp  47069  sge0xaddlem2  47074  sge0seq  47086  sge0reuzb  47088  meadjun  47102  meadjiun  47106  ismeannd  47107  meaiunlelem  47108  meaiininclem  47126  caragenunidm  47148  caragenuncllem  47152  omeiunltfirp  47159  carageniuncllem1  47161  caratheodorylem1  47166  0ome  47169  isomenndlem  47170  hoicvr  47188  hoicvrrex  47196  ovn0lem  47205  ovn0  47206  ovnsubaddlem1  47210  hoidmvval0  47227  hoidmvval0b  47230  hoidmv1lelem1  47231  hoidmv1le  47234  hoidmvlelem2  47236  hoidmvlelem3  47237  hoidmvlelem4  47238  hoidmvlelem5  47239  ovnhoilem1  47241  ovnhoilem2  47242  ovnhoi  47243  dmvon  47246  hspval  47249  ovnlecvr2  47250  hoiqssbllem2  47263  hspmbllem2  47267  hspmbl  47269  hoimbl  47271  ovnsubadd2lem  47285  ovolval4lem1  47289  ovnovollem1  47296  vonvolmbl  47301  vonvol2  47304  iccvonmbllem  47318  vonioolem2  47321  vonn0ioo2  47330  vonn0icc2  47332  smfpimltmpt  47386  issmfdmpt  47388  smfconst  47389  smfpimltxrmptf  47398  smflimlem2  47412  smflimlem3  47413  smflim  47417  smfpimgtmpt  47421  smfpimgtxrmptf  47424  smfsupmpt  47455  smfinfmpt  47459  smflimsuplem4  47463  fresfo  47708  fsetsnf  47711  fsetsnprcnex  47715  cfsetsnfsetf  47718  cfsetsnfsetfo  47720  3f1oss1  47735  f1cof1b  47737  funfocofob  47738  afveq1  47794  afveq2  47795  afvco2  47836  rspceaov  47857  faovcl  47860  afv2eq12d  47875  afv2eq1  47876  afv2eq2  47877  dfatcolem  47915  f1oresf1orab  47949  preimafvsnel  48051  preimafvelsetpreimafv  48060  fundcmpsurbijinjpreimafv  48079  fundcmpsurinjimaid  48083  fundcmpsurinjALT  48084  ichnreuop  48144  ichreuopeq  48145  prelspr  48158  sprsymrelf1lem  48163  sprsymrelfolem2  48165  prproropreud  48181  reuopreuprim  48198  fmtnofac2lem  48243  proththd  48289  requad01  48309  dfodd6  48325  nnsum3primesprm  48478  clnbgrvtxel  48517  isgrim  48570  grimid  48574  upgrimtrls  48594  isubgrgrim  48617  clnbgrgrim  48622  usgrgrtrirex  48638  stgrnbgr0  48652  isubgr3stgrlem6  48659  isgrlim  48670  uspgrlim  48680  grlimedgclnbgr  48683  grlimgrtri  48691  grilcbri2  48699  gpgedgiov  48753  gpg5gricstgr3  48778  gpg5grlim  48781  grlimedgnedg  48819  uspgrsprfo  48836  copissgrp  48856  copisnmnd  48857  isasslaw  48880  2zrngamgm  48933  cznrng  48949  rngcvalALTV  48953  rngcbasALTV  48954  rngchomfvalALTV  48955  rngccofvalALTV  48958  rngccoALTV  48959  rngccatidALTV  48960  rhmsubcALTV  48973  ringcvalALTV  48977  ringcbasALTV  48988  ringchomfvalALTV  48989  ringccofvalALTV  48992  ringccoALTV  48993  ringccatidALTV  48994  scmsuppss  49070  ply1mulgsum  49089  dflinc2  49109  lcoop  49110  lincvalsng  49115  lincvalpr  49117  lincvalsc0  49120  lcoc0  49121  lcoel0  49127  lincsum  49128  lincolss  49133  islininds  49145  lindslinindsimp1  49156  lindsrng01  49167  snlindsntorlem  49169  lincresunit3  49180  islindeps2  49182  lmod1lem3  49188  lmod1zr  49192  itcoval  49360  itcoval0  49361  itcoval1  49362  itcoval2  49363  itcoval3  49364  itcovalsuc  49366  itcovalsucov  49367  itcovalendof  49368  itcovalpclem2  49370  itcovalt2lem2  49375  ackvalsuc1mpt  49377  ackval1  49380  ackval2  49381  ackval3  49382  ackvalsucsucval  49387  affinecomb1  49401  rrx2plordisom  49422  lines  49430  line  49431  rrxline  49433  spheres  49445  line2xlem  49452  itsclc0yqsol  49463  itscnhlinecirc02p  49484  fmpod  49567  iscnrm3llem1  49646  iscnrm3llem2  49647  iscnrm3l  49648  glbsscl  49658  posjidm  49669  posmidm  49670  toslat  49679  ipolubdm  49684  ipoglbdm  49687  mreclat  49694  topclat  49695  iinfssc  49754  iinfsubc  49755  infsubc2  49758  iinfconstbas  49763  nelsubc3  49768  initc  49788  funchomf  49794  imaidfu2lem  49806  imaidfu  49807  imaidfu2  49808  cofidf2  49817  funcoppc4  49841  fthcomf  49854  idfth  49855  idsubc  49857  upciclem1  49863  upfval2  49874  upfval3  49875  isuplem  49876  oppcup3lem  49903  uobffth  49915  uobeqw  49916  uptr2  49918  initopropd  49940  termopropd  49941  dfswapf2  49958  swapfelvv  49960  swapf1vala  49963  swapf2fn  49965  swapf2  49971  tposcurf1cl  49993  tposcurf11  49994  tposcurf12  49995  tposcurf1  49996  tposcurf2  49997  tposcurf2val  49998  tposcurf2cl  49999  tposcurfcl  50000  fucoelvv  50017  fucofvalne  50022  fuco11  50023  fuco11cl  50024  fuco21  50033  fuco11b  50034  fuco11bALT  50035  fuco22natlem3  50041  fuco22natlem  50042  fuco23a  50049  fucofunc  50056  fucofunca  50057  fucolid  50058  fucorid  50059  postcofval  50061  precofval  50064  precofvalALT  50065  precoffunc  50069  prcofelvv  50077  reldmprcof1  50078  reldmprcof2  50079  prcoftposcurfuco  50080  prcoffunc  50082  prcoffunca  50083  fucoppcco  50106  fucoppccic  50110  oppfdiag1  50111  oppfdiag1a  50112  isthincd2lem1  50122  oppcthin  50135  oppcthinco  50136  subthinc  50140  fullthinc  50147  thincciso2  50152  indthinc  50159  prsthinc  50161  setcthin  50162  setc2othin  50163  setcsnterm  50187  setc1ocofval  50191  isinito2lem  50195  dfinito4  50198  idfudiag1  50222  arweuthinc  50226  diag1f1olem  50230  prstchomval  50256  prstcprs  50257  prstcthin  50258  prstchom2  50260  oduoppcciso  50263  postcpos  50264  postcposALT  50265  postc  50266  mndtccatid  50284  mndtcid  50286  oppgoppchom  50287  oppgoppcco  50288  oppgoppcid  50289  grptcmon  50290  grptcepi  50291  2arwcat  50297  lanfval  50310  ranfval  50311  lanpropd  50312  ranpropd  50313  rellan  50320  lanrcl5  50332  ranrcl5  50337  lanup  50338  ranup  50339  lmdfval  50346  cmdfval  50347  lmdpropd  50354  cmdpropd  50355  concom  50360  coccom  50361  islmd  50362  iscmd  50363  lmddu  50364  termolmd  50367  lmdran  50368  cmdlan  50369  aacllem  50509  amgmwlem  50510