Theorem eqidd 2757

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

Syntax hints:   → wi 4   = wceq 1554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-cleq 2748

This theorem is referenced by:  nfabd2  2941  neleq1  3061  neleq2  3062  elabd3  3625  nelrdva  3662  sbcbidv  3794  csbie2df  4391  reusngf  4627  rexreusng  4632  reuprg0  4655  iunxdif3  5046  mpteq1  5183  mpteq1i  5185  mpteq2da  5186  mpteq2dva  5187  nfcvb  5327  dfid2  5537  feq23d  6675  f10d  6830  fvmptdv2  6983  elrnrexdm  7059  f1ossf1o  7099  fmptco  7100  cofmpt  7103  fprg  7127  ftpg  7128  fmptsng  7141  fmptsnd  7142  f1dom3fv3dif  7241  f1dom3el3dif  7242  fliftfun  7285  fliftval  7289  nfriotad  7353  cbvmpo  7479  fconstmpo  7502  eqfnov2  7515  ovmpod  7537  ovmpodv2  7543  fvmpopr2d  7547  elovmporab  7631  elovmporab1w  7632  elovmporab1  7633  ovmpt3rab1  7643  elovmpt3rab  7646  ofval  7660  ofrval  7661  offn  7662  fnfvof  7666  off  7667  ofres  7668  coof  7673  ofco  7674  caofref  7680  caofid0l  7682  caofid0r  7683  caofid1  7684  caofid2  7685  caofrss  7688  caoftrn  7690  tfisi  7828  fsplitfpar  8085  fczsupp0  8161  suppssof1  8167  suppofss1d  8172  suppofss2d  8173  fvmpocurryd  8239  fpr3g  8254  iserd  8693  fsetfocdm  8831  ixpsnf1o  8909  mapxpen  9104  dffi3  9367  cantnf0  9620  cantnfp1  9626  cantnflem1  9634  ttrcltr  9661  axcclem  10404  ttukeylem3  10458  fpwwe2lem8  10586  ofsubeq0  12182  ofnegsub  12183  ofsubge0  12184  fzo0to3tp  13748  fzo1to4tp  13750  modsubmod  13932  seqid  14050  seqid2  14051  seqz  14053  seqof  14062  elovmptnn0wrd  14562  ccatdmss  14585  ccatws1ls  14637  pfxsuffeqwrdeq  14701  wrdind  14725  wrd2ind  14726  ccats1pfxeqbi  14745  repswsymb  14777  repswsymball  14782  repswsymballbi  14783  s3eq2  14873  swrds2m  14944  wrdl2exs2  14949  swrd2lsw  14955  wwlktovfo  14961  s3sndisj  14970  s3iunsndisj  14971  relexp0g  15025  relexpsucnnr  15028  relexp1g  15029  rtrclreclem1  15060  rtrclreclem4  15064  dfrtrcl2  15065  rlim2  15499  climcl  15502  rlimcl  15506  clim2  15507  rlimclim1  15548  rlimclim  15549  climrlim2  15550  climuni  15555  rlimres  15561  climeq  15570  2clim  15575  climshftlem  15577  climabs0  15588  climcn1  15595  climcn2  15596  o1of2  15616  o1rlimmul  15622  o1add2  15627  o1mul2  15628  o1sub2  15629  o1dif  15633  climsqz  15644  climsqz2  15645  rlimdiv  15649  isercoll  15671  climsup  15673  climcau  15674  caurcvgr  15677  caucvgb  15683  serf0  15684  iseralt  15688  sumz  15725  fsumss  15728  fsumsplitsn  15747  fsumsplit1  15748  fsumsplitsnun  15758  isumclim3  15762  isummulc2  15765  fsum2dlem  15773  fsumconst  15793  fsumabs  15805  fsumparts  15810  fsumrlim  15815  fsumo1  15816  seqabs  15818  cvgcmpce  15822  fsumiun  15825  ackbijnn  15834  isumshft  15845  isumltss  15854  climcndslem1  15855  climcndslem2  15856  climcnds  15857  mertenslem1  15890  mertenslem2  15891  prod1  15950  fprodss  15954  fprodconst  15984  fprod2dlem  15986  fprodsplitsn  15995  iprodclim3  16006  eftlcl  16115  reeftlcl  16116  eftlub  16117  efsep  16118  effsumlt  16119  eirrlem  16212  rpnnen2lem6  16227  rpnnen2lem7  16228  rpnnen2lem8  16229  rpnnen2lem9  16230  rpnnen2lem12  16233  2tp1odd  16362  sadasslem  16480  smupvallem  16493  smumul  16503  alginv  16585  algfx  16590  cncongr1  16677  qnumdencoprm  16756  qeqnumdivden  16757  vdwlem1  16993  vdwlem12  17004  vdwlem13  17005  prmodvdslcmf  17059  prmgap  17071  prmgaplcm  17072  prmgapprmo  17074  setsexstruct2  17187  setsstruct  17188  prdssca  17461  prdsbas  17462  prdsplusg  17463  prdsmulr  17464  prdsvsca  17465  prdsip  17466  prdsle  17467  prdsds  17469  prdstset  17471  prdshom  17472  prdsco  17473  prdsvscafval  17485  prdsdsval2  17489  prdsdsval3  17490  pwsle  17498  pwsleval  17499  pwsvscaval  17501  imasbas  17518  imasds  17519  imasplusg  17523  imasmulr  17524  imassca  17525  imasvsca  17526  imasip  17527  imastset  17528  imasle  17529  imasvscafn  17543  imasvscaval  17544  qusin  17550  xpsvsca  17583  iscat  17680  iscatd  17681  iscatd2  17689  0catg  17696  homfeq  17702  homfeqd  17703  comfffval2  17709  comffval2  17710  comfeq  17714  comfeqd  17715  oppccatid  17727  2oppccomf  17733  moni  17745  rcaninv  17803  ssc2  17831  ssctr  17834  ssceq  17835  subcssc  17849  subccat  17857  subsubc  17862  funcres  17905  funcres2  17907  idfusubc  17909  funcres2c  17912  idffth  17944  cofull  17945  cofth  17946  ressffth  17949  isnat  17959  fuccofval  17971  fuccatid  17981  fucpropd  17989  elhomai  18042  coafval  18073  setcval  18086  setcbas  18087  setchomfval  18088  setccofval  18091  setcco  18092  setccatid  18093  setcepi  18097  funcsetcres2  18102  catcval  18109  catcbas  18110  catchomfval  18111  catccofval  18113  catcco  18114  catccatid  18115  catcfuccl  18127  estrcval  18132  estrcbas  18133  estrchomfval  18134  estrccofval  18137  estrcco  18138  estrccatid  18140  estrreslem2  18146  fullestrcsetc  18159  fullsetcestrc  18174  xpcbas  18186  xpchomfval  18187  xpccofval  18190  xpccatid  18196  prfval  18207  catcxpccl  18215  xpcpropd  18216  evlfval  18225  curfval  18231  curf1  18233  curf12  18235  curf2  18237  curf2val  18238  hofval  18260  hof2fval  18263  hofcllem  18266  oppchofcl  18268  oppcyon  18277  oyoncl  18278  yonedalem4a  18283  yonedalem4b  18284  yonedainv  18289  oduposb  18335  joinval  18383  meetval  18397  isdlat  18530  ipopos  18544  pfxchn  18618  chnind  18629  chnso  18632  chnccats1  18633  chnccat  18634  chnrev  18635  gsumpropd  18688  gsumpropd2lem  18689  gsumval1  18693  gsumval2a  18695  issgrp  18730  issgrpd  18740  prdssgrpd  18743  ismndd  18766  mndprop  18770  prdsmndd  18780  imasmnd2  18784  insubm  18828  mhmima  18835  frmdbas  18862  frmdmnd  18869  efmnd  18880  smndex1gid  18914  smndex1gidOLD  18915  smndex1n0mnd  18925  smndex2dlinvh  18930  sgrpnmndex  18945  resgrpplusfrn  18968  grpprop  18970  grpsubfval  19001  grpsubfvalALT  19002  grpsubpropd  19063  prdsgrpd  19068  imasgrp2  19073  imasgrp  19074  imasgrpf1  19075  mulgfval  19087  mulgfvalALT  19088  mulgnngsum  19097  mulgnn0gsum  19098  mulgpropd  19134  subgsub  19156  eqgfval  19193  qusgrp  19203  ghmqusnsglem1  19296  ghmqusnsglem2  19297  ghmqusnsg  19298  ghmquskerlem1  19299  ghmquskerlem2  19301  ghmquskerlem3  19302  ghmqusker  19303  oppgmnd  19370  oppgmndb  19371  oppggrp  19373  oppggrpb  19374  symgval  19387  symg1bas  19407  symg2bas  19409  symgvalstruct  19413  symggrp  19416  gsmsymgrfixlem1  19443  gsmsymgreqlem2  19447  symgfixels  19450  symgsssg  19483  symgfisg  19484  psgnunilem4  19513  psgnvalii  19525  oppglsm  19658  lsmelvalmi  19668  efgi0  19736  efgi1  19737  efgtf  19738  efgval2  19740  efginvrel2  19743  frgp0  19776  frgpup3lem  19793  ablprop  19809  subcmn  19853  gex2abl  19867  prdscmnd  19877  qusabl  19881  abl1  19882  cygabl  19907  gsumzf1o  19928  gsumzaddlem  19937  gsumzsplit  19943  gsumconst  19950  gsumconstf  19951  gsummptshft  19952  gsummhm2  19955  gsummptmhm  19956  gsumzunsnd  19972  gsumunsnfd  19973  gsumpt  19978  gsummptf1o  19979  gsummptun  19980  gsum2dlem2  19987  gsumcom2  19991  nn0gsumfz  20000  dprdval  20021  dprdssv  20034  dprdfeq0  20040  dprdsubg  20042  dprdspan  20045  dprdz  20048  subgdmdprd  20052  subgdprd  20053  gsumle  20161  isrng  20176  isrngd  20195  prdsrngd  20198  imasrng  20199  issrg  20210  isring  20259  ringabl  20303  ringprop  20312  isringd  20313  prdsringd  20341  prdscrngd  20342  prds1  20343  pwspjmhmmgpd  20348  imasring  20351  opprrng  20366  opprrngb  20367  opprringb  20369  dvrfval  20423  rnghmf1o  20473  c0mgm  20480  c0mhm  20481  c0snmgmhm  20483  c0snmhm  20484  rngisomring1  20489  rhmf1o  20512  pwsco1rhm  20523  pwsco2rhm  20524  zrrnghm  20558  rhmimasubrng  20588  pwsdiagrhm  20629  rngcbas  20643  rngchomfval  20644  dfrngc2  20650  rnghmsscmap2  20651  rnghmsscmap  20652  rngccat  20656  rngcid  20657  funcrngcsetc  20662  funcrngcsetcALT  20663  zrinitorngc  20664  zrtermorngc  20665  ringcbas  20672  ringchomfval  20673  dfringc2  20679  rhmsscmap2  20680  rhmsscmap  20681  ringccat  20685  ringcid  20686  rngcresringcat  20691  funcringcsetc  20696  zrtermoringc  20697  rhmsubc  20711  drngprop  20766  isdrngd  20787  isdrngrd  20788  isdrngdOLD  20789  isdrngrdOLD  20790  abvtrivd  20854  idsrngd  20878  suborng  20898  islmodd  20906  lmodabl  20949  lss1  20978  lsssn0  20988  islss3  20999  lss1d  21003  lssintcl  21004  prdslmodd  21009  idlmhm  21081  invlmhm  21082  lmhmvsca  21085  lbsextlem2  21202  sralmod  21227  sralmod0  21228  rlm0  21235  rlmvneg  21246  rnglidlmsgrp  21289  rnglidlrng  21290  qus2idrng  21316  crngridl  21323  quscrng  21326  rhmqusnsg  21328  rngqiprngimf1lem  21337  rngqiprngimf1  21343  absabv  21449  pzriprnglem10  21515  zrhpropd  21539  fermltlchr  21554  znzrh  21567  znbas  21568  zncrng  21569  znzrhfo  21572  znf1o  21576  frgpcyg  21598  evpmodpmf1o  21621  isphld  21679  phlpropd  21680  phssip  21683  phlssphl  21684  pjfval  21731  dsmmval  21759  dsmmsubg  21768  frlmip  21803  frlmipval  21804  frlmphllem  21805  frlmphl  21806  islindf  21837  islindf4  21863  isassa  21881  isassad  21890  issubassa3  21891  asclfval  21903  ressascl  21921  psrval  21940  psrbaglesupp  21947  psrbagcon  21950  psrbaglefi  21951  psrbagleadd1  21953  psrbagconf1o  21954  gsumbagdiaglem  21956  psrass1lem  21958  psrbas  21959  psrplusg  21962  psrmulr  21967  psrsca  21972  psrvscafval  21973  psrvscaval  21975  psrlmod  21984  psrlidm  21986  psrdi  21989  psrdir  21990  psrcom  21992  psrring  21994  psrassa  21997  mplsubglem  22023  mpllsslem  22024  mplvscaval  22040  mplcoe1  22063  mplcoe3  22064  mplcoe5  22066  opsrcrng  22085  opsrassa  22086  mplmon2  22087  evlslem2  22105  evlslem1  22108  evlsvvval  22119  mplmapghm  22148  evlsmaprhm  22157  selvvvval  22168  selvadd  22169  selvmul  22170  mhpmulcl  22187  psdffval  22195  psdmplcl  22200  psdadd  22201  psdmul  22204  psdmvr  22207  ply1lss  22231  ply1subrg  22232  opsr0  22253  opsr1  22254  subrgply1  22267  psrplusgpropd  22270  psropprmul  22272  opsrring  22279  opsrlmod  22280  ply1mpl0  22291  ply1mpl1  22293  coe1z  22299  coe1mul2  22305  coe1tm  22309  coe1sclmulfv  22319  ply1coe  22334  evls1rhm  22358  evls1sca  22359  evl1rhm  22368  evl1sca  22370  evl1expd  22381  evl1gsumdlem  22392  evl1varpw  22397  evls1maplmhm  22413  mamufval  22425  mamudi  22436  mamudir  22437  mat0  22450  matinvg  22451  matlmod  22462  matinvgcell  22468  matring  22476  matassa  22477  mat0dimcrng  22503  mat1dim0  22506  mat1f1o  22511  dmatmulcl  22533  scmatval  22537  scmatscmiddistr  22541  scmataddcl  22549  scmatsubcl  22550  scmatmulcl  22551  scmatlss  22558  scmatrhmcl  22561  1mavmul  22581  mavmul0  22585  marepvfval  22598  submafval  22612  submaval  22614  mdetleib2  22621  mdet0pr  22625  m1detdiag  22630  mdetrsca  22636  mdetrsca2  22637  mdetrlin2  22640  mdetralt  22641  mdetralt2  22642  mdetunilem2  22646  mdetunilem5  22649  mdetunilem9  22653  mdetuni0  22654  m2detleib  22664  madufval  22670  symgmatr01lem  22686  symgmatr01  22687  gsummatr01lem3  22690  gsummatr01lem4  22691  gsummatr01  22692  smadiadetlem3  22701  smadiadetglem2  22705  smadiadetr  22708  mat2pmatghm  22763  cpm2mfval  22782  m2cpminvid  22786  m2cpminvid2lem  22787  m2cpminvid2  22788  decpmatval  22798  decpmataa0  22801  decpmatmul  22805  pmatcollpw1  22809  pmatcollpw2lem  22810  monmatcollpw  22812  pmatcollpwlem  22813  pmatcollpw  22814  pmatcollpwscmatlem2  22823  pm2mpval  22828  pm2mpcl  22830  pm2mpf1  22832  mptcoe1matfsupp  22835  mp2pm2mplem3  22841  mp2pm2mplem4  22842  pm2mpghm  22849  pm2mpmhmlem2  22852  chpmat1dlem  22868  chp0mat  22879  fvmptnn04ifa  22883  fvmptnn04ifb  22884  fvmptnn04ifc  22885  fvmptnn04ifd  22886  cpmadugsumlemB  22907  chcoeffeqlem  22918  epttop  23042  ordtbas2  23224  ordtopn1  23227  ordtopn2  23228  lmss  23331  2ndci  23481  2ndcsep  23492  dis2ndc  23493  1stcelcls  23494  dissnlocfin  23562  ptbasid  23608  xkoopn  23622  prdstopn  23661  ptrescn  23672  txlm  23681  lmcn2  23682  tx1stc  23683  xkopt  23688  cnmpt2c  23703  cnmptk1  23714  cnmpt1k  23715  cnmptkk  23716  qtopeu  23749  txswaphmeolem  23837  xpstopnlem1  23842  ptcmpfi  23846  xkohmeo  23848  rnelfmlem  23985  rnelfm  23986  hauspwpwf1  24020  lmflf  24038  flfcnp2  24040  alexsubb  24079  tmdgsum  24128  tgpconncomp  24146  qustgphaus  24156  tsmsfbas  24161  tsmspropd  24165  tsmssplit  24185  tsmsxplem1  24186  tsmsxplem2  24187  ustuqtop4  24277  imasdsf1olem  24406  blfvalps  24416  stdbdxmet  24548  met2ndci  24555  prdsxmslem2  24562  metustexhalf  24589  cfilucfil  24592  restmetu  24603  nmfval  24621  nmpropd  24627  nmpropd2  24628  subgnm  24666  tng0  24676  tngnm  24684  tnggrpr  24688  tngngp3  24689  tngnrg  24707  sranlm  24717  qdensere  24802  mpomulcn  24902  fsumcn  24905  cncfcompt2  24943  cncfmpt1f  24949  negfcncf  24958  oprpiece1res2  24987  htpyid  25012  phtpyid  25024  pcofval  25045  pcopt2  25058  om1bas  25066  om1plusg  25069  om1tset  25070  pi1bas  25073  pi1bas2  25076  pi1eluni  25077  pi1bas3  25078  pi1cpbl  25079  pi1addf  25082  pi1addval  25083  pi1grplem  25084  pi1xfr  25090  pi1xfrcnvlem  25091  pi1coghm  25096  cphassr  25247  tcphphl  25262  ipcau2  25269  cphipval  25278  lmnn  25298  iscau  25311  cmetcaulem  25323  iscmet3lem1  25326  causs  25333  lmclim  25338  srabn  25395  rrxprds  25424  rrxip  25425  rrxcph  25427  rrxds  25428  rrxmvallem  25439  rrxmval  25440  rrxdsfival  25448  ehl2eudisval  25458  divcncf  25482  ovollb2lem  25523  ovolfiniun  25536  ovolicc2lem4  25555  shftmbl  25573  volfiniun  25582  ioombl1lem4  25596  uniioombllem2  25618  uniioombllem6  25623  vitalilem4  25646  mbfmulc2lem  25682  mbfmulc2re  25683  mbfneg  25685  mbfaddlem  25695  mbfadd  25696  mbfsub  25697  mbfmulc2  25698  0plef  25707  0pledm  25708  itg1ge0  25721  i1faddlem  25728  i1fmullem  25729  i1fmulclem  25737  itg1mulc  25739  itg1lea  25747  itg1le  25748  mbfi1flimlem  25757  mbfmullem2  25759  mbfmul  25761  xrge0f  25766  itg2ge0  25770  itg2const  25775  itg2const2  25776  itg2uba  25778  itg2lea  25779  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  isibl2  25801  iblitg  25803  itgcl  25819  ibl0  25822  iblcnlem1  25823  itgcnlem  25825  iblss  25840  iblss2  25841  i1fibl  25843  itgitg1  25844  itgle  25845  itgeqa  25849  iblconst  25853  ibladdlem  25855  ibladd  25856  itgaddlem1  25858  itgfsum  25862  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgmulc2lem1  25867  itgsplit  25871  bddmulibl  25874  bddibl  25875  bddiblnc  25877  limccnp2  25927  limcco  25928  dvidlem  25950  dvcnp2  25955  dvaddbr  25973  dvmulbr  25974  dvaddf  25977  dvcmulf  25980  dvexp  25988  dvmptadd  25995  dvmptmul  25996  dvmptco  26007  dvmptfsum  26010  dvcnvlem  26011  dvef  26015  rolle  26025  mvth  26027  dvlip  26028  dvlipcn  26029  lhop1lem  26048  itgsubstlem  26083  itgpowd  26085  ply1divalg2  26172  uc1pmon1p  26185  q1pval  26188  r1pval  26191  elply2  26229  elplyr  26234  plypf1  26245  plyaddlem1  26246  coeeulem  26257  plyco  26274  coeaddlem  26282  coemulc  26288  dgradd2  26301  dgrcolem1  26306  dgrcolem2  26307  dgrco  26308  ofmulrt  26316  plydivlem3  26329  plydivlem4  26330  plyrem  26339  iaa  26359  aareccl  26360  aannenlem2  26363  aaliou3lem3  26378  aaliou3lem7  26383  taylfval  26392  taylply2  26401  dvntaylp  26404  taylthlem2  26407  ulmclm  26420  ulmres  26421  ulmshftlem  26422  ulm0  26424  ulmcau  26428  ulmss  26430  ulmbdd  26431  ulmcn  26432  mtest  26437  mtestbdd  26438  iblulm  26440  itgulm  26441  pserulm  26455  pserdvlem2  26461  abelthlem5  26468  abelthlem6  26469  abelthlem8  26472  abelthlem9  26473  sincn  26477  coscn  26478  efcvx  26482  efabl  26585  logfac  26636  logcn  26682  chordthmlem  26867  chordthmlem5  26871  mcubic  26882  leibpi  26977  efrlim  27004  amgmlem  27024  lgamgulmlem2  27064  basellem7  27121  basellem9  27123  musum  27225  chtublem  27245  logexprlim  27259  dchrbas  27269  dchr1cl  27285  dchrabl  27288  dchrfi  27289  dchrhash  27305  bposlem6  27323  lgsdir2lem5  27363  gausslemma2dlem1  27400  lgseisenlem2  27410  lgseisenlem3  27411  lgseisenlem4  27412  lgsquad2lem2  27419  2lgslem1b  27426  2lgslem3b1  27435  2lgslem3c1  27436  2lgsoddprmlem4  27449  2sqlem8  27460  2sqlem11  27463  2sqreulem1  27480  2sqreunnlem1  27483  chtppilimlem2  27508  chebbnd2  27511  chpchtlim  27513  chpo1ub  27514  vmadivsum  27516  rpvmasumlem  27521  dchrisum0re  27547  dchrisum0  27554  mudivsum  27564  selberglem1  27579  selberglem2  27580  selberg2lem  27584  selberg2  27585  pntrsumo1  27599  selbergr  27602  abvcxp  27649  nosupfv  27740  noinffv  27755  madecut  27946  elons2  28321  oncutlt  28327  oniso  28334  seqsfn  28372  seqs1  28373  seqsp1  28374  n0fincut  28418  zcuts  28470  twocut  28486  expsval  28488  pw2cut2  28525  z12addscl  28540  z12shalf  28543  z12zsodd  28545  istrkgld  28598  istrkg2ld  28599  tgsegconeq  28625  tgbtwnouttr2  28634  ercgrg  28656  cgr3id  28658  tgbtwnxfr  28669  motgrp  28682  tgbtwnconn1lem3  28713  legov  28724  legid  28726  btwnleg  28727  legbtwn  28733  mirreu3  28793  mirinv  28805  miduniq1  28825  colmid  28827  krippenlem  28829  israg  28836  ragcgr  28846  motrag  28847  perpneq  28853  isperp2  28854  isperp2d  28855  footexALT  28857  footexlem1  28858  footexlem2  28859  foot  28861  perprag  28865  perpdragALT  28866  colperpexlem1  28869  mideulem2  28873  opphllem2  28887  opphllem3  28888  opphllem4  28889  midbtwn  28918  midcom  28921  mirmid  28922  lmieu  28923  lmif  28924  islmib  28926  lmilmi  28928  lmieq  28930  lmiinv  28931  lmiisolem  28935  hypcgrlem1  28938  hypcgrlem2  28939  lmiopp  28941  trgcopyeu  28945  iscgra  28948  iscgra1  28949  iscgrad  28950  sacgr  28970  isinag  28977  isinagd  28978  inagflat  28979  inaghl  28984  isleag  28986  isleagd  28987  ttgval  29014  cchhllem  29026  usgredg4  29357  ushgredgedg  29369  ushgredgedgloop  29371  usgrstrrepe  29375  uspgr1e  29384  uhgrspan1  29443  usgrres1  29455  nbgrnself  29499  nbusgredgeu  29506  cusgrfilem2  29596  finsumvtxdg2size  29690  finsumvtxdgeven  29692  wlk1walk  29778  uspgr2wlkeq  29785  uspgr2wlkeqi  29787  wlkonwlk  29800  wlkonwlk1l  29801  usgr2trlncl  29899  crctcshwlkn0lem7  29955  wwlksnredwwlkn  30034  wwlksnextbij  30041  wwlksnextprop  30051  wwlksnwwlksnon  30054  elwwlks2ons3im  30093  clwlkclwwlk2  30144  clwlkclwwlkfo  30150  clwlkclwwlkf1  30151  clwwlkwwlksb  30195  clwlknf1oclwwlkn  30225  clwwlknonmpo  30230  clwwlknonex2lem2  30249  0pthon1  30269  uhgr3cyclex  30323  iseupth  30342  eupth0  30355  eupth2lem2  30360  frgr3vlem1  30414  3vfriswmgrlem  30418  2clwwlk2clwwlklem  30487  wlkl0  30508  numclwlk1lem2  30511  grpodivfval  30676  dipfval  30844  ipval2  30849  lnoval  30894  minvecolem3  31018  h2hcau  31121  h2hlm  31122  opsqrlem3  32284  opsqrlem4  32285  foresf1o  32645  disjnf  32712  disjdifprg  32717  iundisjf  32731  br8d  32753  fnfvor  32754  ofrco  32755  ofrn2  32785  off2  32786  ofresid  32787  fmptcof2  32802  aciunf1  32808  ofpreima  32810  f1ocnt  32945  sgnneg  32978  prodindf  32994  indf1ofs  32998  wrdfsupp  33069  wrdpmcl  33070  pfxf1  33074  s1f1  33075  wrdt2ind  33085  swrdrn2  33086  ressnm  33096  abvpropd2  33097  ismntd  33116  dfmgc2lem  33127  pwrssmgc  33132  gsummpt2d  33183  gsummptf1od  33189  gsummptfsf1o  33194  gsumhashmul  33201  gsumwrd2dccat  33212  wrdpmtrlast  33227  psgnfzto1stlem  33234  fzto1st1  33236  tocycfv  33243  cycpmcl  33250  tocycf  33251  tocyc01  33252  cycpmco2f1  33258  cycpmco2rn  33259  cycpmco2lem1  33260  cycpmco2lem2  33261  cycpmco2lem3  33262  cycpmco2lem4  33263  cycpmco2lem5  33264  cycpmco2lem6  33265  cycpmco2lem7  33266  cycpmco2  33267  cycpm3cl2  33270  cycpmconjv  33276  tocyccntz  33278  cyc3evpm  33284  cyc3genpm  33286  cycpmgcl  33287  cycpmconjslem2  33289  cyc3conja  33291  sgnsv  33294  inftmrel  33314  isinftm  33315  submarchi  33320  isslmd  33336  urpropd  33365  elrgspnlem1  33377  elrgspnlem2  33378  elrgspnlem4  33380  elrgspn  33381  elrgspnsubrun  33384  erlval  33393  rlocval  33394  rlocbas  33403  rlocaddval  33404  rlocmulval  33405  rloccring  33406  rlocinvunit  33410  rlocisunit  33411  resv0g  33478  resvcmn  33480  imaslmod  33493  imasmhm  33494  imasghm  33495  imasrhm  33496  imaslmhm  33497  znfermltl  33506  islinds5  33507  ellspds  33508  linds2eq  33521  lindfpropd  33522  elringlsmd  33534  nsgmgclem  33551  nsgmgc  33552  rhmquskerlem  33565  elrspunsn  33569  idlinsubrg  33571  qsidomlem1  33593  qsidomlem2  33594  opprqusbas  33630  qsdrngi  33637  dflring2  33643  rprmval  33666  rprmnz  33670  rprmnunit  33671  unitmulrprm  33678  1arithidomlem1  33685  1arithidomlem2  33686  1arithidom  33687  1arithufdlem3  33696  dfufd2lem  33699  ply1dg1rt  33730  ply1mulrtss  33732  ply1degltlss  33746  ply1gsumz  33749  r1pquslmic  33761  0mplrim  33765  selvply1rhmlemb  33770  selvply1rhmlem2  33772  selvply1rhmlem4  33774  mplvrpmfgalem  33795  psrmonprod  33803  esplyfvaln  33825  esplyind  33826  vietalem  33830  sra1r  33832  sradrng  33833  sraidom  33834  srasubrg  33835  resssra  33838  drgext0g  33841  drgextlsp  33845  rlmdim  33861  tnglvec  33863  tngdim  33864  matdim  33866  ply1degltdimlem  33873  lbsdiflsp0  33877  dimkerim  33878  fedgmullem2  33881  lactlmhm  33885  extdg1id  33917  ccfldsrarelvec  33922  ccfldextdgrr  33923  fldextrspunlsplem  33924  fldextrspunlsp  33925  fldextrspunlem1  33926  fldextrspunfld  33927  fldextrspunlem2  33928  extdgfialglem1  33943  extdgfialglem2  33944  irredminply  33967  algextdeglem3  33970  algextdeglem4  33971  algextdeglem8  33975  constrsslem  33992  constrext2chnlem  34001  constrcon  34025  2sqr3nconstr  34032  cos9thpinconstrlem2  34041  1smat1  34055  submatres  34057  submateq  34060  lmatcl  34067  mdetlap1  34077  madjusmdetlem3  34080  circtopn  34088  locfinref  34092  tpr2rico  34163  lmdvglim  34205  qqhval  34223  esumeq1  34285  esumeq1d  34286  esumeq2d  34288  esumf1o  34301  esumsplit  34304  esumadd  34308  gsumesum  34310  esumlub  34311  esumaddf  34312  esumcst  34314  esumsnf  34315  esumpinfval  34324  esumcocn  34331  esummulc1  34332  esumcvg  34337  esum2d  34344  ofcval  34350  ofcfn  34351  ofcfeqd2  34352  ofcf  34354  ofcfval4  34356  ofcof  34358  sigapildsys  34413  sxval  34441  measvunilem0  34464  measvuni  34465  measiun  34469  meascnbl  34470  measinb  34472  volmeas  34482  sxbrsiga  34541  omssubadd  34551  fiunelcarsg  34567  itgeq12dv  34577  sitgval  34583  eulerpartlems  34611  eulerpartgbij  34623  eulerpartlemn  34632  sseqf  34643  sseqp1  34646  totprobd  34677  probfinmeasb  34679  probmeasb  34681  rrvadd  34703  dstfrvclim1  34729  gsumnunsn  34792  plymul02  34797  plymulx  34799  signsply0  34802  fdvneggt  34851  fdvnegge  34853  itgexpif  34857  reprpmtf1o  34877  circlemethhgt  34894  logdivsqrle  34901  hgt750lemg  34905  hgt750lemb  34907  hgt750lema  34908  f1resfz0f1d  35412  2cycl2d  35437  quartfull  35463  sconnpi1  35537  cvmliftphtlem  35615  cvmlift3lem2  35618  satfv1  35661  satfdmlem  35666  satf0suc  35674  satf0op  35675  sat1el2xp  35677  fmla  35679  fmlasuc0  35682  fmlafvel  35683  fmlasuc  35684  fmla1  35685  satffunlem1lem2  35701  satffunlem2lem2  35704  sategoelfvb  35717  satfv1fvfmla1  35721  2goelgoanfmla1  35722  elmsubrn  35826  msubco  35829  mthmpps  35880  r1peuqusdeg1  35941  sinccvg  35971  circum  35972  br8  36054  br4  36056  brsegle  36406  hilbert1.1  36452  itgeq2sdv  36528  ditgeq3sdv  36531  cbvoprab23davw  36584  cbvoprab13davw  36585  trer  36624  knoppcnlem4  36882  knoppcnlem9  36887  knoppcnlem11  36889  knoppndvlem6  36903  knoppf  36921  bj-imdirco  37630  bj-fvmptunsn2  37698  bj-finsumval0  37725  exrecfnlem  37821  finxpreclem1  37831  matunitlindflem1  38063  matunitlindflem2  38064  poimirlem1  38068  poimirlem2  38069  poimirlem3  38070  poimirlem4  38071  poimirlem5  38072  poimirlem6  38073  poimirlem7  38074  poimirlem10  38077  poimirlem11  38078  poimirlem12  38079  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem22  38089  poimirlem23  38090  poimirlem28  38095  poimirlem29  38096  poimirlem31  38098  broucube  38101  mblfinlem2  38105  volsupnfl  38112  itg2addnclem  38118  itg2addnclem3  38120  itg2addnc  38121  itg2gt0cn  38122  ibladdnclem  38123  itgaddnclem1  38125  itgaddnc  38127  iblabsnclem  38130  iblabsnc  38131  iblmulc2nc  38132  itgmulc2nclem1  38133  itgmulc2nclem2  38134  itgmulc2nc  38135  ftc1anclem2  38141  ftc1anclem4  38143  ftc1anclem5  38144  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  areacirc  38160  unirep  38161  upixp  38176  sdc  38191  lmclim2  38205  geomcau  38206  caures  38207  caushft  38208  prdsbnd2  38242  heibor1lem  38256  bfplem2  38270  rrncmslem  38279  isrngo  38344  iuneq2f  38603  dmec2d  38758  lflset  39631  islfld  39634  lfladdcl  39643  lflvscl  39649  lkrsc  39669  eqlkr2  39672  lshpkrlem1  39682  ldualset  39697  ldualvaddval  39703  ldualvsval  39710  ldualgrplem  39717  lduallmodlem  39724  cmtfvalN  39782  isoml  39810  iscvlat  39895  llni2  40084  lplni2  40109  lvoli3  40149  lvoli2  40153  paddfval  40369  lhpset  40567  ltrnfset  40689  trlfset  40732  cdleme21k  40910  cdlemeiota  41157  tgrpfset  41316  tgrpset  41317  tgrpabl  41323  tendo0cbv  41358  tendo02  41359  erngfset  41371  erngset  41372  erngfset-rN  41379  erngset-rN  41380  cdlemkid5  41507  cdlemkid  41508  dvafset  41576  dvaset  41577  diaffval  41602  dialss  41618  diaf11N  41621  dvhfset  41652  dvhset  41653  docaffvalN  41693  dibfval  41713  dibf11N  41733  diblss  41742  diclss  41765  dihord2cN  41793  dihord11b  41794  dihffval  41802  dihord6apre  41828  dihglblem2aN  41865  dihglblem2N  41866  dihjatcclem4  41993  lclkrs  42111  mapdh6dN  42311  mapdh6eN  42312  mapdh6fN  42313  mapdh6jN  42317  hvmapffval  42330  hvmapfval  42331  mapdh8a  42347  mapdh8ad  42351  mapdh8d0N  42354  mapdh8d  42355  mapdh8i  42358  mapdh8j  42359  mapdh9a  42361  mapdh9aOLDN  42362  hdmap1l6d  42385  hdmap1l6e  42386  hdmap1l6f  42387  hdmap1l6j  42391  hdmapval2  42404  hdmapeveclem  42406  hdmapval3lemN  42409  hdmap11lem1  42413  hgmapfval  42458  hlhils0  42517  hlhils1N  42518  hlhillvec  42523  hlhildrng  42524  hlhil0  42527  hlhillsm  42528  rhmzrhval  42537  zndvdchrrhm  42538  3factsumint1  42586  lcmineqlem12  42605  aks4d1p1p4  42636  aks4d1p1p7  42639  aks4d1p9  42653  isprimroot  42658  primrootsunit1  42662  posbezout  42665  primrootscoprbij  42667  remexz  42669  aks6d1c1p2  42674  aks6d1c1p3  42675  aks6d1c1p4  42676  aks6d1c1p5  42677  aks6d1c1p7  42678  evl1gprodd  42682  aks6d1c2p2  42684  hashscontpow  42687  aks6d1c2lem4  42692  aks6d1c2  42695  aks6d1c5lem2  42703  aks6d1c5  42704  deg1gprod  42705  2np3bcnp1  42709  2ap1caineq  42710  sticksstones8  42718  sticksstones10  42720  sticksstones12a  42722  sticksstones12  42723  sticksstones17  42728  sticksstones18  42729  sticksstones19  42730  sticksstones21  42732  sticksstones22  42733  aks6d1c6lem1  42735  aks6d1c6lem2  42736  aks6d1c6lem4  42738  aks6d1c6isolem1  42739  aks5lem3a  42754  grpods  42759  unitscyglem1  42760  unitscyglem2  42761  ofun  42802  redivcan2d  43004  redivcan3d  43005  sn-rediv0d  43010  sn-redividd  43011  rhmpsr1  43114  evlselv  43119  fsuppind  43120  mhphf  43127  3cubeslem3r  43216  eldiophb  43286  eldioph  43287  eldioph3  43295  rabren3dioph  43340  pellqrexplicit  43402  rmxycomplete  43442  rmxynorm  43443  acongrep  43505  jm2.26a  43525  jm2.26  43527  fnwe2lem2  43576  fnwe2lem3  43577  aomclem5  43583  aomclem8  43586  imasgim  43625  isnumbasgrplem1  43626  hbtlem5  43653  dgrsub2  43660  rgspnid  43693  rngunsnply  43694  mendval  43704  mendring  43713  mendlmod  43714  mendassa  43715  nnoeomeqom  43837  tfsconcatb0  43869  oaun3  43907  safesnsupfilb  43942  fsovrfovd  44533  fsovcnvlem  44537  mnring0gd  44745  mnringlmodd  44750  mnringmulrcld  44752  colleq1  44778  colleq2  44779  dvgrat  44836  radcnvrat  44838  hashnzfzclim  44846  caofcan  44847  ofsubid  44848  ofmul12  44849  ofdivrec  44850  ofdivcan4  44851  ofdivdiv2  44852  expgrowth  44859  binomcxplemnn0  44873  binomcxplemrat  44874  binomcxplemdvbinom  44877  binomcxplemnotnn0  44880  wessf1ornlem  45711  disjf1o  45717  ssnnf1octb  45720  mapss2  45730  icof  45743  mpteq1df  45759  infnsuprnmpt  45773  upbdrech  45832  divcan8d  45839  dmmcand  45840  suplesup  45863  ssuzfz  45873  supsubc  45877  xralrple2  45878  fprodabs2  46119  fprodcn  46124  clim1fr1  46125  climrec  46127  climexp  46129  climinf  46130  climsuse  46132  climneg  46134  divcnvg  46151  sumnnodd  46154  clim2f  46158  clim2f2  46192  fnlimfvre  46196  climleltrp  46198  climreclmpt  46206  climinf2mpt  46236  climinfmpt  46237  supcnvlimsup  46262  climuzlem  46265  climisp  46268  climrescn  46270  climxrrelem  46271  climxrre  46272  liminfvalxrmpt  46308  liminflbuz2  46337  cncfcompt  46405  dvsinax  46435  fperdvper  46441  dvcosax  46448  ioodvbdlimc1lem2  46454  ioodvbdlimc2lem  46456  dvnxpaek  46464  dvnmul  46465  dvmptfprodlem  46466  dvnprodlem1  46468  dvnprodlem2  46469  dvnprodlem3  46470  iblempty  46487  iblsplit  46488  itgcoscmulx  46491  itgsincmulx  46496  itgsubsticc  46498  sublevolico  46506  stoweidlem2  46524  stoweidlem17  46539  stoweidlem21  46543  stoweidlem32  46554  stoweidlem46  46568  stoweidlem55  46577  wallispi  46592  wallispi2lem1  46593  wallispi2lem2  46594  wallispi2  46595  stirlinglem3  46598  dirkercncflem2  46626  dirkercncflem4  46628  fourierdlem16  46645  fourierdlem18  46647  fourierdlem21  46650  fourierdlem22  46651  fourierdlem39  46668  fourierdlem53  46681  fourierdlem58  46686  fourierdlem59  46687  fourierdlem62  46690  fourierdlem73  46701  fourierdlem76  46704  fourierdlem81  46709  fourierdlem83  46711  fourierdlem93  46721  fourierdlem101  46729  fourierdlem103  46731  fourierdlem104  46732  fourierdlem111  46739  fourierdlem112  46740  fouriersw  46753  elaa2lem  46755  etransclem18  46774  etransclem32  46788  etransclem33  46789  etransclem46  46802  etransclem48  46804  rrxtopnfi  46809  rrxunitopnfi  46814  salincl  46846  sge0z  46897  sge0tsms  46902  sge0snmpt  46905  sge0sup  46913  sge0resplit  46928  sge0ss  46934  sge0isum  46949  sge0xp  46951  sge0xaddlem2  46956  sge0seq  46968  sge0reuzb  46970  meadjun  46984  meadjiun  46988  ismeannd  46989  meaiunlelem  46990  meaiininclem  47008  caragenunidm  47030  caragenuncllem  47034  omeiunltfirp  47041  carageniuncllem1  47043  caratheodorylem1  47048  0ome  47051  isomenndlem  47052  hoicvr  47070  hoicvrrex  47078  ovn0lem  47087  ovn0  47088  ovnsubaddlem1  47092  hoidmvval0  47109  hoidmvval0b  47112  hoidmv1lelem1  47113  hoidmv1le  47116  hoidmvlelem2  47118  hoidmvlelem3  47119  hoidmvlelem4  47120  hoidmvlelem5  47121  ovnhoilem1  47123  ovnhoilem2  47124  ovnhoi  47125  dmvon  47128  hspval  47131  ovnlecvr2  47132  hoiqssbllem2  47145  hspmbllem2  47149  hspmbl  47151  hoimbl  47153  ovnsubadd2lem  47167  ovolval4lem1  47171  ovnovollem1  47178  vonvolmbl  47183  vonvol2  47186  iccvonmbllem  47200  vonioolem2  47203  vonn0ioo2  47212  vonn0icc2  47214  smfpimltmpt  47268  issmfdmpt  47270  smfconst  47271  smfpimltxrmptf  47280  smflimlem2  47294  smflimlem3  47295  smflim  47299  smfpimgtmpt  47303  smfpimgtxrmptf  47306  smfsupmpt  47337  smfinfmpt  47341  smflimsuplem4  47345  fresfo  47590  fsetsnf  47593  fsetsnprcnex  47597  cfsetsnfsetf  47600  cfsetsnfsetfo  47602  3f1oss1  47617  f1cof1b  47619  funfocofob  47620  afveq1  47676  afveq2  47677  afvco2  47718  rspceaov  47739  faovcl  47742  afv2eq12d  47757  afv2eq1  47758  afv2eq2  47759  dfatcolem  47797  f1oresf1orab  47831  preimafvsnel  47933  preimafvelsetpreimafv  47942  fundcmpsurbijinjpreimafv  47961  fundcmpsurinjimaid  47965  fundcmpsurinjALT  47966  ichnreuop  48026  ichreuopeq  48027  prelspr  48040  sprsymrelf1lem  48045  sprsymrelfolem2  48047  prproropreud  48063  reuopreuprim  48080  fmtnofac2lem  48125  proththd  48171  requad01  48191  dfodd6  48207  nnsum3primesprm  48360  clnbgrvtxel  48399  isgrim  48452  grimid  48456  upgrimtrls  48476  isubgrgrim  48499  clnbgrgrim  48504  usgrgrtrirex  48520  stgrnbgr0  48534  isubgr3stgrlem6  48541  isgrlim  48552  uspgrlim  48562  grlimedgclnbgr  48565  grlimgrtri  48573  grilcbri2  48581  gpgedgiov  48635  gpg5gricstgr3  48660  gpg5grlim  48663  grlimedgnedg  48701  uspgrsprfo  48718  copissgrp  48738  copisnmnd  48739  isasslaw  48762  2zrngamgm  48815  cznrng  48831  rngcvalALTV  48835  rngcbasALTV  48836  rngchomfvalALTV  48837  rngccofvalALTV  48840  rngccoALTV  48841  rngccatidALTV  48842  rhmsubcALTV  48855  ringcvalALTV  48859  ringcbasALTV  48870  ringchomfvalALTV  48871  ringccofvalALTV  48874  ringccoALTV  48875  ringccatidALTV  48876  scmsuppss  48941  ply1mulgsum  48960  dflinc2  48980  lcoop  48981  lincvalsng  48986  lincvalpr  48988  lincvalsc0  48991  lcoc0  48992  lcoel0  48998  lincsum  48999  lincolss  49004  islininds  49016  lindslinindsimp1  49027  lindsrng01  49038  snlindsntorlem  49040  lincresunit3  49051  islindeps2  49053  lmod1lem3  49059  lmod1zr  49063  itcoval  49231  itcoval0  49232  itcoval1  49233  itcoval2  49234  itcoval3  49235  itcovalsuc  49237  itcovalsucov  49238  itcovalendof  49239  itcovalpclem2  49241  itcovalt2lem2  49246  ackvalsuc1mpt  49248  ackval1  49251  ackval2  49252  ackval3  49253  ackvalsucsucval  49258  affinecomb1  49272  rrx2plordisom  49293  lines  49301  line  49302  rrxline  49304  spheres  49316  line2xlem  49323  itsclc0yqsol  49334  itscnhlinecirc02p  49355  fmpod  49439  iscnrm3llem1  49518  iscnrm3llem2  49519  iscnrm3l  49520  glbsscl  49530  posjidm  49541  posmidm  49542  toslat  49551  ipolubdm  49556  ipoglbdm  49559  mreclat  49566  topclat  49567  iinfssc  49626  iinfsubc  49627  infsubc2  49630  iinfconstbas  49635  nelsubc3  49640  initc  49660  funchomf  49666  imaidfu2lem  49678  imaidfu  49679  imaidfu2  49680  cofidf2  49689  funcoppc4  49713  fthcomf  49726  idfth  49727  idsubc  49729  upciclem1  49735  upfval2  49746  upfval3  49747  isuplem  49748  oppcup3lem  49775  uobffth  49787  uobeqw  49788  uptr2  49790  initopropd  49812  termopropd  49813  dfswapf2  49830  swapfelvv  49832  swapf1vala  49835  swapf2fn  49837  swapf2  49843  tposcurf1cl  49865  tposcurf11  49866  tposcurf12  49867  tposcurf1  49868  tposcurf2  49869  tposcurf2val  49870  tposcurf2cl  49871  tposcurfcl  49872  fucoelvv  49889  fucofvalne  49894  fuco11  49895  fuco11cl  49896  fuco21  49905  fuco11b  49906  fuco11bALT  49907  fuco22natlem3  49913  fuco22natlem  49914  fuco23a  49921  fucofunc  49928  fucofunca  49929  fucolid  49930  fucorid  49931  postcofval  49933  precofval  49936  precofvalALT  49937  precoffunc  49941  prcofelvv  49949  reldmprcof1  49950  reldmprcof2  49951  prcoftposcurfuco  49952  prcoffunc  49954  prcoffunca  49955  fucoppcco  49978  fucoppccic  49982  oppfdiag1  49983  oppfdiag1a  49984  isthincd2lem1  49994  oppcthin  50007  oppcthinco  50008  subthinc  50012  fullthinc  50019  thincciso2  50024  indthinc  50031  prsthinc  50033  setcthin  50034  setc2othin  50035  setcsnterm  50059  setc1ocofval  50063  isinito2lem  50067  dfinito4  50070  idfudiag1  50094  arweuthinc  50098  diag1f1olem  50102  prstchomval  50128  prstcprs  50129  prstcthin  50130  prstchom2  50132  oduoppcciso  50135  postcpos  50136  postcposALT  50137  postc  50138  mndtccatid  50156  mndtcid  50158  oppgoppchom  50159  oppgoppcco  50160  oppgoppcid  50161  grptcmon  50162  grptcepi  50163  2arwcat  50169  lanfval  50182  ranfval  50183  lanpropd  50184  ranpropd  50185  rellan  50192  lanrcl5  50204  ranrcl5  50209  lanup  50210  ranup  50211  lmdfval  50218  cmdfval  50219  lmdpropd  50226  cmdpropd  50227  concom  50232  coccom  50233  islmd  50234  iscmd  50235  lmddu  50236  termolmd  50239  lmdran  50240  cmdlan  50241  aacllem  50370  amgmwlem  50371