Theorem eqidd 2732

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 2731	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  nfabd2  2918  neleq1  3038  neleq2  3039  cbvraldvaOLD  3316  cbvrexdvaOLD  3317  rspcedeq1vd  3584  rspcedeq2vd  3585  elabd3  3626  nelrdva  3664  sbcbidv  3797  csbie2df  4393  reusngf  4627  rexreusng  4632  reuprg0  4655  iunxdif3  5043  mpteq1  5180  mpteq1i  5182  mpteq2da  5183  mpteq2dva  5184  nfcvb  5314  dfid2  5513  feq23d  6646  f10d  6797  fvmptdv2  6947  elrnrexdm  7022  f1ossf1o  7061  fmptco  7062  cofmpt  7065  fprg  7088  ftpg  7089  fmptsng  7102  fmptsnd  7103  f1dom3fv3dif  7202  f1dom3el3dif  7203  fliftfun  7246  fliftval  7250  nfriotad  7314  cbvmpo  7440  fconstmpo  7463  eqfnov2  7476  ovmpod  7498  ovmpodv2  7504  fvmpopr2d  7508  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  ovmpt3rab1  7604  elovmpt3rab  7607  ofval  7621  ofrval  7622  offn  7623  fnfvof  7627  off  7628  ofres  7629  coof  7634  ofco  7635  caofref  7641  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  caofrss  7649  caoftrn  7651  tfisi  7789  fsplitfpar  8048  fczsupp0  8123  suppssof1  8129  suppofss1d  8134  suppofss2d  8135  fvmpocurryd  8201  fpr3g  8215  iserd  8648  fsetfocdm  8785  ixpsnf1o  8862  mapxpen  9056  dffi3  9315  cantnf0  9565  cantnfp1  9571  cantnflem1  9579  ttrcltr  9606  axcclem  10345  ttukeylem3  10399  fpwwe2lem8  10526  ofsubeq0  12119  ofnegsub  12120  ofsubge0  12121  fzo0to3tp  13649  fzo1to4tp  13651  modsubmod  13833  seqid  13951  seqid2  13952  seqz  13954  seqof  13963  elovmptnn0wrd  14463  ccatdmss  14486  ccatws1ls  14538  pfxsuffeqwrdeq  14602  wrdind  14626  wrd2ind  14627  ccats1pfxeqbi  14646  repswsymb  14678  repswsymball  14683  repswsymballbi  14684  s3eq2  14774  swrds2m  14845  wrdl2exs2  14850  swrd2lsw  14856  wwlktovfo  14862  s3sndisj  14871  s3iunsndisj  14872  relexp0g  14926  relexpsucnnr  14929  relexp1g  14930  rtrclreclem1  14961  rtrclreclem4  14965  dfrtrcl2  14966  rlim2  15400  climcl  15403  rlimcl  15407  clim2  15408  rlimclim1  15449  rlimclim  15450  climrlim2  15451  climuni  15456  rlimres  15462  climeq  15471  2clim  15476  climshftlem  15478  climabs0  15489  climcn1  15496  climcn2  15497  o1of2  15517  o1rlimmul  15523  o1add2  15528  o1mul2  15529  o1sub2  15530  o1dif  15534  climsqz  15545  climsqz2  15546  rlimdiv  15550  isercoll  15572  climsup  15574  climcau  15575  caurcvgr  15578  caucvgb  15584  serf0  15585  iseralt  15589  sumz  15626  fsumss  15629  fsumsplitsn  15648  fsumsplit1  15649  fsumsplitsnun  15659  isumclim3  15663  isummulc2  15666  fsum2dlem  15674  fsumconst  15694  fsumabs  15705  fsumparts  15710  fsumrlim  15715  fsumo1  15716  seqabs  15718  cvgcmpce  15722  fsumiun  15725  ackbijnn  15732  isumshft  15743  isumltss  15752  climcndslem1  15753  climcndslem2  15754  climcnds  15755  mertenslem1  15788  mertenslem2  15789  prod1  15848  fprodss  15852  fprodconst  15882  fprod2dlem  15884  fprodsplitsn  15893  iprodclim3  15904  eftlcl  16013  reeftlcl  16014  eftlub  16015  efsep  16016  effsumlt  16017  eirrlem  16110  rpnnen2lem6  16125  rpnnen2lem7  16126  rpnnen2lem8  16127  rpnnen2lem9  16128  rpnnen2lem12  16131  2tp1odd  16260  sadasslem  16378  smupvallem  16391  smumul  16401  alginv  16483  algfx  16488  cncongr1  16575  qnumdencoprm  16653  qeqnumdivden  16654  vdwlem1  16890  vdwlem12  16901  vdwlem13  16902  prmodvdslcmf  16956  prmgap  16968  prmgaplcm  16969  prmgapprmo  16971  setsexstruct2  17083  setsstruct  17084  prdssca  17357  prdsbas  17358  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  prdsip  17362  prdsle  17363  prdsds  17365  prdstset  17367  prdshom  17368  prdsco  17369  prdsvscafval  17381  prdsdsval2  17385  prdsdsval3  17386  pwsle  17393  pwsleval  17394  pwsvscaval  17396  imasbas  17413  imasds  17414  imasplusg  17418  imasmulr  17419  imassca  17420  imasvsca  17421  imasip  17422  imastset  17423  imasle  17424  imasvscafn  17438  imasvscaval  17439  qusin  17445  xpsvsca  17478  iscat  17575  iscatd  17576  iscatd2  17584  0catg  17591  homfeq  17597  homfeqd  17598  comfffval2  17604  comffval2  17605  comfeq  17609  comfeqd  17610  oppccatid  17622  2oppccomf  17628  moni  17640  rcaninv  17698  ssc2  17726  ssctr  17729  ssceq  17730  subcssc  17744  subccat  17752  subsubc  17757  funcres  17800  funcres2  17802  idfusubc  17804  funcres2c  17807  idffth  17839  cofull  17840  cofth  17841  ressffth  17844  isnat  17854  fuccofval  17866  fuccatid  17876  fucpropd  17884  elhomai  17937  coafval  17968  setcval  17981  setcbas  17982  setchomfval  17983  setccofval  17986  setcco  17987  setccatid  17988  setcepi  17992  funcsetcres2  17997  catcval  18004  catcbas  18005  catchomfval  18006  catccofval  18008  catcco  18009  catccatid  18010  catcfuccl  18022  estrcval  18027  estrcbas  18028  estrchomfval  18029  estrccofval  18032  estrcco  18033  estrccatid  18035  estrreslem2  18041  fullestrcsetc  18054  fullsetcestrc  18069  xpcbas  18081  xpchomfval  18082  xpccofval  18085  xpccatid  18091  prfval  18102  catcxpccl  18110  xpcpropd  18111  evlfval  18120  curfval  18126  curf1  18128  curf12  18130  curf2  18132  curf2val  18133  hofval  18155  hof2fval  18158  hofcllem  18161  oppchofcl  18163  oppcyon  18172  oyoncl  18173  yonedalem4a  18178  yonedalem4b  18179  yonedainv  18184  oduposb  18230  joinval  18278  meetval  18292  isdlat  18425  ipopos  18439  pfxchn  18513  chnind  18524  chnso  18527  chnccats1  18528  chnccat  18529  chnrev  18530  gsumpropd  18583  gsumpropd2lem  18584  gsumval1  18588  gsumval2a  18590  issgrp  18625  issgrpd  18635  prdssgrpd  18638  ismndd  18661  mndprop  18665  prdsmndd  18675  imasmnd2  18679  insubm  18723  mhmima  18730  frmdbas  18757  frmdmnd  18764  efmnd  18775  smndex1gid  18808  smndex1n0mnd  18817  smndex2dlinvh  18822  sgrpnmndex  18837  resgrpplusfrn  18860  grpprop  18862  grpsubfval  18893  grpsubfvalALT  18894  grpsubpropd  18955  prdsgrpd  18960  imasgrp2  18965  imasgrp  18966  imasgrpf1  18967  mulgfval  18979  mulgfvalALT  18980  mulgnngsum  18989  mulgnn0gsum  18990  mulgpropd  19026  subgsub  19048  eqgfval  19086  qusgrp  19096  ghmqusnsglem1  19190  ghmqusnsglem2  19191  ghmqusnsg  19192  ghmquskerlem1  19193  ghmquskerlem2  19195  ghmquskerlem3  19196  ghmqusker  19197  oppgmnd  19264  oppgmndb  19265  oppggrp  19267  oppggrpb  19268  symgval  19281  symg1bas  19301  symg2bas  19303  symgvalstruct  19307  symggrp  19310  gsmsymgrfixlem1  19337  gsmsymgreqlem2  19341  symgfixels  19344  symgsssg  19377  symgfisg  19378  psgnunilem4  19407  psgnvalii  19419  oppglsm  19552  lsmelvalmi  19562  efgi0  19630  efgi1  19631  efgtf  19632  efgval2  19634  efginvrel2  19637  frgp0  19670  frgpup3lem  19687  ablprop  19703  subcmn  19747  gex2abl  19761  prdscmnd  19771  qusabl  19775  abl1  19776  cygabl  19801  gsumzf1o  19822  gsumzaddlem  19831  gsumzsplit  19837  gsumconst  19844  gsumconstf  19845  gsummptshft  19846  gsummhm2  19849  gsummptmhm  19850  gsumzunsnd  19866  gsumunsnfd  19867  gsumpt  19872  gsummptf1o  19873  gsummptun  19874  gsum2dlem2  19881  gsumcom2  19885  nn0gsumfz  19894  dprdval  19915  dprdssv  19928  dprdfeq0  19934  dprdsubg  19936  dprdspan  19939  dprdz  19942  subgdmdprd  19946  subgdprd  19947  gsumle  20055  isrng  20070  isrngd  20089  prdsrngd  20092  imasrng  20093  issrg  20104  isring  20153  ringabl  20197  ringprop  20206  isringd  20207  prdsringd  20237  prdscrngd  20238  prds1  20239  pwspjmhmmgpd  20244  imasring  20246  opprrng  20261  opprrngb  20262  opprringb  20264  dvrfval  20318  rnghmf1o  20368  c0mgm  20375  c0mhm  20376  c0snmgmhm  20378  c0snmhm  20379  rngisomring1  20384  rhmf1o  20406  pwsco1rhm  20415  pwsco2rhm  20416  zrrnghm  20449  rhmimasubrng  20479  pwsdiagrhm  20520  rngcbas  20534  rngchomfval  20535  dfrngc2  20541  rnghmsscmap2  20542  rnghmsscmap  20543  rngccat  20547  rngcid  20548  funcrngcsetc  20553  funcrngcsetcALT  20554  zrinitorngc  20555  zrtermorngc  20556  ringcbas  20563  ringchomfval  20564  dfringc2  20570  rhmsscmap2  20571  rhmsscmap  20572  ringccat  20576  ringcid  20577  rngcresringcat  20582  funcringcsetc  20587  zrtermoringc  20588  rhmsubc  20602  drngprop  20657  isdrngd  20678  isdrngrd  20679  isdrngdOLD  20680  isdrngrdOLD  20681  abvtrivd  20745  idsrngd  20769  suborng  20789  islmodd  20797  lmodabl  20840  lss1  20869  lsssn0  20879  islss3  20890  lss1d  20894  lssintcl  20895  prdslmodd  20900  idlmhm  20973  invlmhm  20974  lmhmvsca  20977  lbsextlem2  21094  sralmod  21119  sralmod0  21120  rlm0  21127  rlmvneg  21138  rnglidlmsgrp  21181  rnglidlrng  21182  qus2idrng  21208  crngridl  21215  quscrng  21218  rhmqusnsg  21220  rngqiprngimf1lem  21229  rngqiprngimf1  21235  dfcnfldOLD  21305  absabv  21359  pzriprnglem10  21425  zrhpropd  21449  fermltlchr  21464  znzrh  21477  znbas  21478  zncrng  21479  znzrhfo  21482  znf1o  21486  frgpcyg  21508  evpmodpmf1o  21531  isphld  21589  phlpropd  21590  phssip  21593  phlssphl  21594  pjfval  21641  dsmmval  21669  dsmmsubg  21678  frlmip  21713  frlmipval  21714  frlmphllem  21715  frlmphl  21716  islindf  21747  islindf4  21773  isassa  21791  isassad  21800  issubassa3  21801  sraassaOLD  21805  asclfval  21814  ressascl  21831  psrval  21850  psrbaglesupp  21857  psrbagcon  21860  psrbaglefi  21861  psrbagleadd1  21863  psrbagconf1o  21864  gsumbagdiaglem  21865  psrass1lem  21867  psrbas  21868  psrplusg  21871  psrmulr  21877  psrsca  21882  psrvscafval  21883  psrvscaval  21885  psrgrpOLD  21892  psrlmod  21895  psrlidm  21897  psrdi  21900  psrdir  21901  psrcom  21903  psrring  21905  psrassa  21908  mplsubglem  21934  mpllsslem  21935  mplvscaval  21951  mplcoe1  21970  mplcoe3  21971  mplcoe5  21973  opsrcrng  21992  opsrassa  21993  mplmon2  21994  evlslem2  22012  evlslem1  22015  mhpmulcl  22062  psdffval  22070  psdmplcl  22075  psdadd  22076  psdmul  22079  psdmvr  22082  ply1lss  22107  ply1subrg  22108  opsr0  22129  opsr1  22130  subrgply1  22143  psrplusgpropd  22146  psropprmul  22148  opsrring  22155  opsrlmod  22156  ply1mpl0  22167  ply1mpl1  22169  coe1z  22175  coe1mul2  22181  coe1tm  22185  coe1sclmulfv  22195  ply1coe  22211  evls1rhm  22235  evls1sca  22236  evl1rhm  22245  evl1sca  22247  evl1expd  22258  evl1gsumdlem  22269  evl1varpw  22274  evls1maplmhm  22290  mamufval  22305  mamudi  22316  mamudir  22317  mat0  22330  matinvg  22331  matlmod  22342  matinvgcell  22348  matring  22356  matassa  22357  mat0dimcrng  22383  mat1dim0  22386  mat1f1o  22391  dmatmulcl  22413  scmatval  22417  scmatscmiddistr  22421  scmataddcl  22429  scmatsubcl  22430  scmatmulcl  22431  scmatlss  22438  scmatrhmcl  22441  1mavmul  22461  mavmul0  22465  marepvfval  22478  submafval  22492  submaval  22494  mdetleib2  22501  mdet0pr  22505  m1detdiag  22510  mdetrsca  22516  mdetrsca2  22517  mdetrlin2  22520  mdetralt  22521  mdetralt2  22522  mdetunilem2  22526  mdetunilem5  22529  mdetunilem9  22533  mdetuni0  22534  m2detleib  22544  madufval  22550  symgmatr01lem  22566  symgmatr01  22567  gsummatr01lem3  22570  gsummatr01lem4  22571  gsummatr01  22572  smadiadetlem3  22581  smadiadetglem2  22585  smadiadetr  22588  mat2pmatghm  22643  cpm2mfval  22662  m2cpminvid  22666  m2cpminvid2lem  22667  m2cpminvid2  22668  decpmatval  22678  decpmataa0  22681  decpmatmul  22685  pmatcollpw1  22689  pmatcollpw2lem  22690  monmatcollpw  22692  pmatcollpwlem  22693  pmatcollpw  22694  pmatcollpwscmatlem2  22703  pm2mpval  22708  pm2mpcl  22710  pm2mpf1  22712  mptcoe1matfsupp  22715  mp2pm2mplem3  22721  mp2pm2mplem4  22722  pm2mpghm  22729  pm2mpmhmlem2  22732  chpmat1dlem  22748  chp0mat  22759  fvmptnn04ifa  22763  fvmptnn04ifb  22764  fvmptnn04ifc  22765  fvmptnn04ifd  22766  cpmadugsumlemB  22787  chcoeffeqlem  22798  epttop  22922  ordtbas2  23104  ordtopn1  23107  ordtopn2  23108  lmss  23211  2ndci  23361  2ndcsep  23372  dis2ndc  23373  1stcelcls  23374  dissnlocfin  23442  ptbasid  23488  xkoopn  23502  prdstopn  23541  ptrescn  23552  txlm  23561  lmcn2  23562  tx1stc  23563  xkopt  23568  cnmpt2c  23583  cnmptk1  23594  cnmpt1k  23595  cnmptkk  23596  qtopeu  23629  txswaphmeolem  23717  xpstopnlem1  23722  ptcmpfi  23726  xkohmeo  23728  rnelfmlem  23865  rnelfm  23866  hauspwpwf1  23900  lmflf  23918  flfcnp2  23920  alexsubb  23959  tmdgsum  24008  tgpconncomp  24026  qustgphaus  24036  tsmsfbas  24041  tsmspropd  24045  tsmssplit  24065  tsmsxplem1  24066  tsmsxplem2  24067  ustuqtop4  24157  imasdsf1olem  24286  blfvalps  24296  stdbdxmet  24428  met2ndci  24435  prdsxmslem2  24442  metustexhalf  24469  cfilucfil  24472  restmetu  24483  nmfval  24501  nmpropd  24507  nmpropd2  24508  subgnm  24546  tng0  24556  tngnm  24564  tnggrpr  24568  tngngp3  24569  tngnrg  24587  sranlm  24597  qdensere  24682  mpomulcn  24783  fsumcn  24786  cncfcompt2  24826  cncfmpt1f  24832  negfcncf  24842  oprpiece1res2  24875  htpyid  24901  phtpyid  24913  pcofval  24935  pcopt2  24948  om1bas  24956  om1plusg  24959  om1tset  24960  pi1bas  24963  pi1bas2  24966  pi1eluni  24967  pi1bas3  24968  pi1cpbl  24969  pi1addf  24972  pi1addval  24973  pi1grplem  24974  pi1xfr  24980  pi1xfrcnvlem  24981  pi1coghm  24986  cphassr  25137  tcphphl  25152  ipcau2  25159  cphipval  25168  lmnn  25188  iscau  25201  cmetcaulem  25213  iscmet3lem1  25216  causs  25223  lmclim  25228  srabn  25285  rrxprds  25314  rrxip  25315  rrxcph  25317  rrxds  25318  rrxmvallem  25329  rrxmval  25330  rrxdsfival  25338  ehl2eudisval  25348  divcncf  25373  ovollb2lem  25414  ovolfiniun  25427  ovolicc2lem4  25446  shftmbl  25464  volfiniun  25473  ioombl1lem4  25487  uniioombllem2  25509  uniioombllem6  25514  vitalilem4  25537  mbfmulc2lem  25573  mbfmulc2re  25574  mbfneg  25576  mbfaddlem  25586  mbfadd  25587  mbfsub  25588  mbfmulc2  25589  0plef  25598  0pledm  25599  itg1ge0  25612  i1faddlem  25619  i1fmullem  25620  i1fmulclem  25628  itg1mulc  25630  itg1lea  25638  itg1le  25639  mbfi1flimlem  25648  mbfmullem2  25650  mbfmul  25652  xrge0f  25657  itg2ge0  25661  itg2const  25666  itg2const2  25667  itg2uba  25669  itg2lea  25670  itg2splitlem  25674  itg2split  25675  itg2monolem1  25676  itg2mono  25679  itg2i1fseqle  25680  itg2i1fseq  25681  itg2addlem  25684  itg2gt0  25686  itg2cnlem1  25687  itg2cnlem2  25688  isibl2  25692  iblitg  25694  itgcl  25710  ibl0  25713  iblcnlem1  25714  itgcnlem  25716  iblss  25731  iblss2  25732  i1fibl  25734  itgitg1  25735  itgle  25736  itgeqa  25740  iblconst  25744  ibladdlem  25746  ibladd  25747  itgaddlem1  25749  itgfsum  25753  iblabslem  25754  iblabs  25755  iblabsr  25756  iblmulc2  25757  itgmulc2lem1  25758  itgsplit  25762  bddmulibl  25765  bddibl  25766  bddiblnc  25768  limccnp2  25818  limcco  25819  dvidlem  25841  dvcnp2  25846  dvcnp2OLD  25847  dvaddbr  25865  dvmulbr  25866  dvmulbrOLD  25867  dvaddf  25870  dvcmulf  25873  dvexp  25882  dvmptadd  25889  dvmptmul  25890  dvmptco  25901  dvmptfsum  25904  dvcnvlem  25905  dvef  25909  rolle  25919  mvth  25922  dvlip  25923  dvlipcn  25924  lhop1lem  25943  itgsubstlem  25980  itgpowd  25982  ply1divalg2  26069  uc1pmon1p  26082  q1pval  26085  r1pval  26088  elply2  26126  elplyr  26131  plypf1  26142  plyaddlem1  26143  coeeulem  26154  plyco  26171  coeaddlem  26179  coemulc  26185  dgradd2  26199  dgrcolem1  26204  dgrcolem2  26205  dgrco  26206  ofmulrt  26214  plydivlem3  26228  plydivlem4  26229  plyrem  26238  iaa  26258  aareccl  26259  aannenlem2  26262  aaliou3lem3  26277  aaliou3lem7  26282  taylfval  26291  taylply2  26300  taylply2OLD  26301  dvntaylp  26304  taylthlem2  26307  taylthlem2OLD  26308  ulmclm  26321  ulmres  26322  ulmshftlem  26323  ulm0  26325  ulmcau  26329  ulmss  26331  ulmbdd  26332  ulmcn  26333  mtest  26338  mtestbdd  26339  iblulm  26341  itgulm  26342  pserulm  26356  pserdvlem2  26363  abelthlem5  26370  abelthlem6  26371  abelthlem8  26374  abelthlem9  26375  sincn  26379  coscn  26380  efcvx  26384  efabl  26484  logfac  26535  logcn  26581  chordthmlem  26767  chordthmlem5  26771  mcubic  26782  leibpi  26877  efrlim  26904  efrlimOLD  26905  amgmlem  26925  lgamgulmlem2  26965  basellem7  27022  basellem9  27024  musum  27126  chtublem  27147  logexprlim  27161  dchrbas  27171  dchr1cl  27187  dchrabl  27190  dchrfi  27191  dchrhash  27207  bposlem6  27225  lgsdir2lem5  27265  gausslemma2dlem1  27302  lgseisenlem2  27312  lgseisenlem3  27313  lgseisenlem4  27314  lgsquad2lem2  27321  2lgslem1b  27328  2lgslem3b1  27337  2lgslem3c1  27338  2lgsoddprmlem4  27351  2sqlem8  27362  2sqlem11  27365  2sqreulem1  27382  2sqreunnlem1  27385  chtppilimlem2  27410  chebbnd2  27413  chpchtlim  27415  chpo1ub  27416  vmadivsum  27418  rpvmasumlem  27423  dchrisum0re  27449  dchrisum0  27456  mudivsum  27466  selberglem1  27481  selberglem2  27482  selberg2lem  27486  selberg2  27487  pntrsumo1  27501  selbergr  27504  abvcxp  27551  nosupfv  27643  noinffv  27658  madecut  27826  elons2  28193  onscutlt  28199  onsiso  28203  seqsfn  28237  seqs1  28238  seqsp1  28239  n0sfincut  28280  zscut  28329  twocut  28344  expsval  28346  pw2cut2  28380  zs12addscl  28385  zs12half  28388  zs12zodd  28390  istrkgld  28435  istrkg2ld  28436  tgsegconeq  28462  tgbtwnouttr2  28471  ercgrg  28493  cgr3id  28495  tgbtwnxfr  28506  motgrp  28519  tgbtwnconn1lem3  28550  legov  28561  legid  28563  btwnleg  28564  legbtwn  28570  mirreu3  28630  mirinv  28642  miduniq1  28662  colmid  28664  krippenlem  28666  israg  28673  ragcgr  28683  motrag  28684  perpneq  28690  isperp2  28691  isperp2d  28692  footexALT  28694  footexlem1  28695  footexlem2  28696  foot  28698  perprag  28702  perpdragALT  28703  colperpexlem1  28706  mideulem2  28710  opphllem2  28724  opphllem3  28725  opphllem4  28726  midbtwn  28755  midcom  28758  mirmid  28759  lmieu  28760  lmif  28761  islmib  28763  lmilmi  28765  lmieq  28767  lmiinv  28768  lmiisolem  28772  hypcgrlem1  28775  hypcgrlem2  28776  lmiopp  28778  trgcopyeu  28782  iscgra  28785  iscgra1  28786  iscgrad  28787  sacgr  28807  isinag  28814  isinagd  28815  inagflat  28816  inaghl  28821  isleag  28823  isleagd  28824  ttgval  28851  cchhllem  28863  usgredg4  29193  ushgredgedg  29205  ushgredgedgloop  29207  usgrstrrepe  29211  uspgr1e  29220  uhgrspan1  29279  usgrres1  29291  nbgrnself  29335  nbusgredgeu  29342  cusgrfilem2  29433  finsumvtxdg2size  29527  finsumvtxdgeven  29529  wlk1walk  29615  uspgr2wlkeq  29622  uspgr2wlkeqi  29624  wlkonwlk  29637  wlkonwlk1l  29638  usgr2trlncl  29736  crctcshwlkn0lem7  29792  wwlksnredwwlkn  29871  wwlksnextbij  29878  wwlksnextprop  29888  wwlksnwwlksnon  29891  elwwlks2ons3im  29930  clwlkclwwlk2  29978  clwlkclwwlkfo  29984  clwlkclwwlkf1  29985  clwwlkwwlksb  30029  clwlknf1oclwwlkn  30059  clwwlknonmpo  30064  clwwlknonex2lem2  30083  0pthon1  30103  uhgr3cyclex  30157  iseupth  30176  eupth0  30189  eupth2lem2  30194  frgr3vlem1  30248  3vfriswmgrlem  30252  2clwwlk2clwwlklem  30321  wlkl0  30342  numclwlk1lem2  30345  grpodivfval  30509  dipfval  30677  ipval2  30682  lnoval  30727  minvecolem3  30851  h2hcau  30954  h2hlm  30955  opsqrlem3  32117  opsqrlem4  32118  foresf1o  32479  disjnf  32545  disjdifprg  32550  iundisjf  32564  br8d  32586  fnfvor  32587  ofrco  32588  ofrn2  32617  off2  32618  ofresid  32619  fmptcof2  32634  aciunf1  32640  ofpreima  32642  padct  32696  f1ocnt  32777  sgnneg  32811  prodindf  32839  indf1ofs  32842  wrdfsupp  32913  wrdpmcl  32914  pfxf1  32918  s1f1  32919  wrdt2ind  32929  swrdrn2  32930  ressnm  32940  abvpropd2  32941  ismntd  32960  dfmgc2lem  32971  pwrssmgc  32976  gsummpt2d  33024  gsummptfsf1o  33029  gsumhashmul  33036  gsumwrd2dccat  33042  wrdpmtrlast  33057  psgnfzto1stlem  33064  fzto1st1  33066  tocycfv  33073  cycpmcl  33080  tocycf  33081  tocyc01  33082  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem1  33090  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cycpm3cl2  33100  cycpmconjv  33106  tocyccntz  33108  cyc3evpm  33114  cyc3genpm  33116  cycpmgcl  33117  cycpmconjslem2  33119  cyc3conja  33121  sgnsv  33124  inftmrel  33144  isinftm  33145  submarchi  33150  isslmd  33166  urpropd  33194  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem4  33207  elrgspn  33208  elrgspnsubrun  33211  erlval  33220  rlocval  33221  rlocbas  33229  rlocaddval  33230  rlocmulval  33231  rloccring  33232  resv0g  33298  resvcmn  33300  imaslmod  33313  imasmhm  33314  imasghm  33315  imasrhm  33316  imaslmhm  33317  znfermltl  33326  islinds5  33327  ellspds  33328  linds2eq  33341  lindfpropd  33342  elringlsmd  33354  nsgmgclem  33371  nsgmgc  33372  rhmquskerlem  33385  elrspunsn  33389  idlinsubrg  33391  qsidomlem1  33412  qsidomlem2  33413  opprqusbas  33448  qsdrngi  33455  rprmval  33476  rprmnz  33480  rprmnunit  33481  unitmulrprm  33488  1arithidomlem1  33495  1arithidomlem2  33496  1arithidom  33497  1arithufdlem3  33506  dfufd2lem  33509  ply1dg1rt  33538  ply1mulrtss  33540  ply1degltlss  33552  ply1gsumz  33554  r1pquslmic  33566  mplvrpmfgalem  33569  sra1r  33588  sradrng  33589  sraidom  33590  srasubrg  33591  resssra  33594  drgext0g  33597  drgextlsp  33601  rlmdim  33617  rgmoddimOLD  33618  tnglvec  33620  tngdim  33621  matdim  33623  ply1degltdimlem  33630  lbsdiflsp0  33634  dimkerim  33635  fedgmullem2  33638  lactlmhm  33642  extdg1id  33674  ccfldsrarelvec  33679  ccfldextdgrr  33680  fldextrspunlsplem  33681  fldextrspunlsp  33682  fldextrspunlem1  33683  fldextrspunfld  33684  fldextrspunlem2  33685  extdgfialglem1  33700  extdgfialglem2  33701  irredminply  33724  algextdeglem3  33727  algextdeglem4  33728  algextdeglem8  33732  constrsslem  33749  constrext2chnlem  33758  constrcon  33782  2sqr3nconstr  33789  cos9thpinconstrlem2  33798  1smat1  33812  submatres  33814  submateq  33817  lmatcl  33824  mdetlap1  33834  madjusmdetlem3  33837  circtopn  33845  locfinref  33849  tpr2rico  33920  lmdvglim  33962  qqhval  33980  esumeq1  34042  esumeq1d  34043  esumeq2d  34045  esumf1o  34058  esumsplit  34061  esumadd  34065  gsumesum  34067  esumlub  34068  esumaddf  34069  esumcst  34071  esumsnf  34072  esumpinfval  34081  esumcocn  34088  esummulc1  34089  esumcvg  34094  esum2d  34101  ofcval  34107  ofcfn  34108  ofcfeqd2  34109  ofcf  34111  ofcfval4  34113  ofcof  34115  sigapildsys  34170  sxval  34198  measvunilem0  34221  measvuni  34222  measiun  34226  meascnbl  34227  measinb  34229  volmeas  34239  sxbrsiga  34298  omssubadd  34308  fiunelcarsg  34324  itgeq12dv  34334  sitgval  34340  eulerpartlems  34368  eulerpartgbij  34380  eulerpartlemn  34389  sseqf  34400  sseqp1  34403  totprobd  34434  probfinmeasb  34436  probmeasb  34438  rrvadd  34460  dstfrvclim1  34486  gsumnunsn  34549  plymul02  34554  plymulx  34556  signsply0  34559  fdvneggt  34608  fdvnegge  34610  itgexpif  34614  reprpmtf1o  34634  circlemethhgt  34651  logdivsqrle  34658  hgt750lemg  34662  hgt750lemb  34664  hgt750lema  34665  f1resfz0f1d  35146  2cycl2d  35171  quartfull  35197  sconnpi1  35271  cvmliftphtlem  35349  cvmlift3lem2  35352  satfv1  35395  satfdmlem  35400  satf0suc  35408  satf0op  35409  sat1el2xp  35411  fmla  35413  fmlasuc0  35416  fmlafvel  35417  fmlasuc  35418  fmla1  35419  satffunlem1lem2  35435  satffunlem2lem2  35438  sategoelfvb  35451  satfv1fvfmla1  35455  2goelgoanfmla1  35456  elmsubrn  35560  msubco  35563  mthmpps  35614  r1peuqusdeg1  35675  sinccvg  35705  circum  35706  br8  35788  br4  35790  brsegle  36141  hilbert1.1  36187  itgeq2sdv  36253  ditgeq3sdv  36256  cbvoprab23davw  36309  cbvoprab13davw  36310  trer  36349  knoppcnlem4  36529  knoppcnlem9  36534  knoppcnlem11  36536  knoppndvlem6  36550  knoppf  36568  bj-imdirco  37223  bj-fvmptunsn2  37291  bj-finsumval0  37318  exrecfnlem  37412  finxpreclem1  37422  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem28  37687  poimirlem29  37688  poimirlem31  37690  broucube  37693  mblfinlem2  37697  volsupnfl  37704  itg2addnclem  37710  itg2addnclem3  37712  itg2addnc  37713  itg2gt0cn  37714  ibladdnclem  37715  itgaddnclem1  37717  itgaddnc  37719  iblabsnclem  37722  iblabsnc  37723  iblmulc2nc  37724  itgmulc2nclem1  37725  itgmulc2nclem2  37726  itgmulc2nc  37727  ftc1anclem2  37733  ftc1anclem4  37735  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  areacirc  37752  unirep  37753  upixp  37768  sdc  37783  lmclim2  37797  geomcau  37798  caures  37799  caushft  37800  prdsbnd2  37834  heibor1lem  37848  bfplem2  37862  rrncmslem  37871  isrngo  37936  iuneq2f  38195  dmec2d  38338  lflset  39097  islfld  39100  lfladdcl  39109  lflvscl  39115  lkrsc  39135  eqlkr2  39138  lshpkrlem1  39148  ldualset  39163  ldualvaddval  39169  ldualvsval  39176  ldualgrplem  39183  lduallmodlem  39190  cmtfvalN  39248  isoml  39276  iscvlat  39361  llni2  39550  lplni2  39575  lvoli3  39615  lvoli2  39619  paddfval  39835  lhpset  40033  ltrnfset  40155  trlfset  40198  cdleme21k  40376  cdlemeiota  40623  tgrpfset  40782  tgrpset  40783  tgrpabl  40789  tendo0cbv  40824  tendo02  40825  erngfset  40837  erngset  40838  erngfset-rN  40845  erngset-rN  40846  cdlemkid5  40973  cdlemkid  40974  dvafset  41042  dvaset  41043  diaffval  41068  dialss  41084  diaf11N  41087  dvhfset  41118  dvhset  41119  docaffvalN  41159  dibfval  41179  dibf11N  41199  diblss  41208  diclss  41231  dihord2cN  41259  dihord11b  41260  dihffval  41268  dihord6apre  41294  dihglblem2aN  41331  dihglblem2N  41332  dihjatcclem4  41459  lclkrs  41577  mapdh6dN  41777  mapdh6eN  41778  mapdh6fN  41779  mapdh6jN  41783  hvmapffval  41796  hvmapfval  41797  mapdh8a  41813  mapdh8ad  41817  mapdh8d0N  41820  mapdh8d  41821  mapdh8i  41824  mapdh8j  41825  mapdh9a  41827  mapdh9aOLDN  41828  hdmap1l6d  41851  hdmap1l6e  41852  hdmap1l6f  41853  hdmap1l6j  41857  hdmapval2  41870  hdmapeveclem  41872  hdmapval3lemN  41875  hdmap11lem1  41879  hgmapfval  41924  hlhils0  41983  hlhils1N  41984  hlhillvec  41989  hlhildrng  41990  hlhil0  41993  hlhillsm  41994  rhmzrhval  42003  zndvdchrrhm  42004  3factsumint1  42053  lcmineqlem12  42072  aks4d1p1p4  42103  aks4d1p1p7  42106  aks4d1p9  42120  isprimroot  42125  primrootsunit1  42129  posbezout  42132  primrootscoprbij  42134  remexz  42136  aks6d1c1p2  42141  aks6d1c1p3  42142  aks6d1c1p4  42143  aks6d1c1p5  42144  aks6d1c1p7  42145  evl1gprodd  42149  aks6d1c2p2  42151  hashscontpow  42154  aks6d1c2lem4  42159  aks6d1c2  42162  aks6d1c5lem2  42170  aks6d1c5  42171  deg1gprod  42172  2np3bcnp1  42176  2ap1caineq  42177  sticksstones8  42185  sticksstones10  42187  sticksstones12a  42189  sticksstones12  42190  sticksstones17  42195  sticksstones18  42196  sticksstones19  42197  sticksstones21  42199  sticksstones22  42200  aks6d1c6lem1  42202  aks6d1c6lem2  42203  aks6d1c6lem4  42205  aks6d1c6isolem1  42206  aks5lem3a  42221  grpods  42226  unitscyglem1  42227  unitscyglem2  42228  ofun  42268  redivcan2d  42478  redivcan3d  42479  rhmpsr1  42585  mplmapghm  42588  evlsvvval  42595  evlsmaprhm  42602  selvvvval  42617  evlselv  42619  selvadd  42620  selvmul  42621  fsuppind  42622  mhphf  42629  3cubeslem3r  42719  eldiophb  42789  eldioph  42790  eldioph3  42798  rabren3dioph  42847  pellqrexplicit  42909  rmxycomplete  42949  rmxynorm  42950  acongrep  43012  jm2.26a  43032  jm2.26  43034  fnwe2lem2  43083  fnwe2lem3  43084  aomclem5  43090  aomclem8  43093  imasgim  43132  isnumbasgrplem1  43133  hbtlem5  43160  dgrsub2  43167  rgspnid  43200  rngunsnply  43201  mendval  43211  mendring  43220  mendlmod  43221  mendassa  43222  nnoeomeqom  43344  tfsconcatb0  43376  oaun3  43414  safesnsupfilb  43450  fsovrfovd  44041  fsovcnvlem  44045  mnring0gd  44253  mnringlmodd  44258  mnringmulrcld  44260  colleq1  44286  colleq2  44287  dvgrat  44344  radcnvrat  44346  hashnzfzclim  44354  caofcan  44355  ofsubid  44356  ofmul12  44357  ofdivrec  44358  ofdivcan4  44359  ofdivdiv2  44360  expgrowth  44367  binomcxplemnn0  44381  binomcxplemrat  44382  binomcxplemdvbinom  44385  binomcxplemnotnn0  44388  wessf1ornlem  45221  disjf1o  45227  ssnnf1octb  45230  mapss2  45241  icof  45255  mpteq1df  45272  infnsuprnmpt  45286  upbdrech  45345  divcan8d  45352  dmmcand  45353  suplesup  45377  ssuzfz  45387  supsubc  45391  xralrple2  45392  fprodabs2  45634  fprodcn  45639  clim1fr1  45640  climrec  45642  climexp  45644  climinf  45645  climsuse  45647  climneg  45649  divcnvg  45666  sumnnodd  45669  clim2f  45673  clim2f2  45707  fnlimfvre  45711  climleltrp  45713  climreclmpt  45721  climinf2mpt  45751  climinfmpt  45752  supcnvlimsup  45777  climuzlem  45780  climisp  45783  climrescn  45785  climxrrelem  45786  climxrre  45787  liminfvalxrmpt  45823  liminflbuz2  45852  cncfcompt  45920  dvsinax  45950  fperdvper  45956  dvcosax  45963  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnxpaek  45979  dvnmul  45980  dvmptfprodlem  45981  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  iblempty  46002  iblsplit  46003  itgcoscmulx  46006  itgsincmulx  46011  itgsubsticc  46013  sublevolico  46021  stoweidlem2  46039  stoweidlem17  46054  stoweidlem21  46058  stoweidlem32  46069  stoweidlem46  46083  stoweidlem55  46092  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  wallispi2  46110  stirlinglem3  46113  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem16  46160  fourierdlem18  46162  fourierdlem21  46165  fourierdlem22  46166  fourierdlem39  46183  fourierdlem53  46196  fourierdlem58  46201  fourierdlem59  46202  fourierdlem62  46205  fourierdlem73  46216  fourierdlem76  46219  fourierdlem81  46224  fourierdlem83  46226  fourierdlem93  46236  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  fouriersw  46268  elaa2lem  46270  etransclem18  46289  etransclem32  46303  etransclem33  46304  etransclem46  46317  etransclem48  46319  rrxtopnfi  46324  rrxunitopnfi  46329  salincl  46361  sge0z  46412  sge0tsms  46417  sge0snmpt  46420  sge0sup  46428  sge0resplit  46443  sge0ss  46449  sge0isum  46464  sge0xp  46466  sge0xaddlem2  46471  sge0seq  46483  sge0reuzb  46485  meadjun  46499  meadjiun  46503  ismeannd  46504  meaiunlelem  46505  meaiininclem  46523  caragenunidm  46545  caragenuncllem  46549  omeiunltfirp  46556  carageniuncllem1  46558  caratheodorylem1  46563  0ome  46566  isomenndlem  46567  hoicvr  46585  hoicvrrex  46593  ovn0lem  46602  ovn0  46603  ovnsubaddlem1  46607  hoidmvval0  46624  hoidmvval0b  46627  hoidmv1lelem1  46628  hoidmv1le  46631  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoidmvlelem5  46636  ovnhoilem1  46638  ovnhoilem2  46639  ovnhoi  46640  dmvon  46643  hspval  46646  ovnlecvr2  46647  hoiqssbllem2  46660  hspmbllem2  46664  hspmbl  46666  hoimbl  46668  ovnsubadd2lem  46682  ovolval4lem1  46686  ovnovollem1  46693  vonvolmbl  46698  vonvol2  46701  iccvonmbllem  46715  vonioolem2  46718  vonn0ioo2  46727  vonn0icc2  46729  smfpimltmpt  46783  issmfdmpt  46785  smfconst  46786  smfpimltxrmptf  46795  smflimlem2  46809  smflimlem3  46810  smflim  46814  smfpimgtmpt  46818  smfpimgtxrmptf  46821  smfsupmpt  46852  smfinfmpt  46856  smflimsuplem4  46860  fresfo  47078  fsetsnf  47081  fsetsnprcnex  47085  cfsetsnfsetf  47088  cfsetsnfsetfo  47090  3f1oss1  47105  f1cof1b  47107  funfocofob  47108  afveq1  47164  afveq2  47165  afvco2  47206  rspceaov  47227  faovcl  47230  afv2eq12d  47245  afv2eq1  47246  afv2eq2  47247  dfatcolem  47285  f1oresf1orab  47319  preimafvsnel  47409  preimafvelsetpreimafv  47418  fundcmpsurbijinjpreimafv  47437  fundcmpsurinjimaid  47441  fundcmpsurinjALT  47442  ichnreuop  47502  ichreuopeq  47503  prelspr  47516  sprsymrelf1lem  47521  sprsymrelfolem2  47523  prproropreud  47539  reuopreuprim  47556  fmtnofac2lem  47598  proththd  47644  requad01  47651  dfodd6  47667  nnsum3primesprm  47820  clnbgrvtxel  47859  isgrim  47912  grimid  47916  upgrimtrls  47936  isubgrgrim  47959  clnbgrgrim  47964  usgrgrtrirex  47980  stgrnbgr0  47994  isubgr3stgrlem6  48001  isgrlim  48012  uspgrlim  48022  grlimedgclnbgr  48025  grlimgrtri  48033  grilcbri2  48041  gpgedgiov  48095  gpg5gricstgr3  48120  gpg5grlim  48123  grlimedgnedg  48161  uspgrsprfo  48178  copissgrp  48198  copisnmnd  48199  isasslaw  48222  2zrngamgm  48275  cznrng  48291  rngcvalALTV  48295  rngcbasALTV  48296  rngchomfvalALTV  48297  rngccofvalALTV  48300  rngccoALTV  48301  rngccatidALTV  48302  rhmsubcALTV  48315  ringcvalALTV  48319  ringcbasALTV  48330  ringchomfvalALTV  48331  ringccofvalALTV  48334  ringccoALTV  48335  ringccatidALTV  48336  scmsuppss  48401  ply1mulgsum  48421  dflinc2  48441  lcoop  48442  lincvalsng  48447  lincvalpr  48449  lincvalsc0  48452  lcoc0  48453  lcoel0  48459  lincsum  48460  lincolss  48465  islininds  48477  lindslinindsimp1  48488  lindsrng01  48499  snlindsntorlem  48501  lincresunit3  48512  islindeps2  48514  lmod1lem3  48520  lmod1zr  48524  itcoval  48692  itcoval0  48693  itcoval1  48694  itcoval2  48695  itcoval3  48696  itcovalsuc  48698  itcovalsucov  48699  itcovalendof  48700  itcovalpclem2  48702  itcovalt2lem2  48707  ackvalsuc1mpt  48709  ackval1  48712  ackval2  48713  ackval3  48714  ackvalsucsucval  48719  affinecomb1  48733  rrx2plordisom  48754  lines  48762  line  48763  rrxline  48765  spheres  48777  line2xlem  48784  itsclc0yqsol  48795  itscnhlinecirc02p  48816  fmpod  48900  iscnrm3llem1  48979  iscnrm3llem2  48980  iscnrm3l  48981  glbsscl  48991  posjidm  49002  posmidm  49003  toslat  49012  ipolubdm  49017  ipoglbdm  49020  mreclat  49027  topclat  49028  iinfssc  49088  iinfsubc  49089  infsubc2  49092  iinfconstbas  49097  nelsubc3  49102  initc  49122  funchomf  49128  imaidfu2lem  49140  imaidfu  49141  imaidfu2  49142  cofidf2  49151  funcoppc4  49175  fthcomf  49188  idfth  49189  idsubc  49191  upciclem1  49197  upfval2  49208  upfval3  49209  isuplem  49210  oppcup3lem  49237  uobffth  49249  uobeqw  49250  uptr2  49252  initopropd  49274  termopropd  49275  dfswapf2  49292  swapfelvv  49294  swapf1vala  49297  swapf2fn  49299  swapf2  49305  tposcurf1cl  49327  tposcurf11  49328  tposcurf12  49329  tposcurf1  49330  tposcurf2  49331  tposcurf2val  49332  tposcurf2cl  49333  tposcurfcl  49334  fucoelvv  49351  fucofvalne  49356  fuco11  49357  fuco11cl  49358  fuco21  49367  fuco11b  49368  fuco11bALT  49369  fuco22natlem3  49375  fuco22natlem  49376  fuco23a  49383  fucofunc  49390  fucofunca  49391  fucolid  49392  fucorid  49393  postcofval  49395  precofval  49398  precofvalALT  49399  precoffunc  49403  prcofelvv  49411  reldmprcof1  49412  reldmprcof2  49413  prcoftposcurfuco  49414  prcoffunc  49416  prcoffunca  49417  fucoppcco  49440  fucoppccic  49444  oppfdiag1  49445  oppfdiag1a  49446  isthincd2lem1  49456  oppcthin  49469  oppcthinco  49470  subthinc  49474  fullthinc  49481  thincciso2  49486  indthinc  49493  prsthinc  49495  setcthin  49496  setc2othin  49497  setcsnterm  49521  setc1ocofval  49525  isinito2lem  49529  dfinito4  49532  idfudiag1  49556  arweuthinc  49560  diag1f1olem  49564  prstchomval  49590  prstcprs  49591  prstcthin  49592  prstchom2  49594  oduoppcciso  49597  postcpos  49598  postcposALT  49599  postc  49600  mndtccatid  49618  mndtcid  49620  oppgoppchom  49621  oppgoppcco  49622  oppgoppcid  49623  grptcmon  49624  grptcepi  49625  2arwcat  49631  lanfval  49644  ranfval  49645  lanpropd  49646  ranpropd  49647  rellan  49654  lanrcl5  49666  ranrcl5  49671  lanup  49672  ranup  49673  lmdfval  49680  cmdfval  49681  lmdpropd  49688  cmdpropd  49689  concom  49694  coccom  49695  islmd  49696  iscmd  49697  lmddu  49698  termolmd  49701  lmdran  49702  cmdlan  49703  aacllem  49832  amgmwlem  49833