Theorem syl5eq 2668

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
syl5eq.1	|- A = B
syl5eq.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5eq	|- ( ph -> A = C )

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 |- A = B
2	1	a1i 11	. 2 |- ( ph -> A = B )
3		syl5eq.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrd 2656	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  syl5req  2669  syl5eqr  2670  3eqtr3a  2680  3eqtr4g  2681  csbtt  3544  csbie2g  3564  rabbi2dva  3821  csbprcOLD  3981  csbvarg  4003  csbsng  4243  csbprg  4244  disjpr2  4248  disjpr2OLD  4249  disjprsn  4250  disjtpsn  4251  disjtp2  4252  rabsnif  4258  prprc2  4301  difprsn2  4331  difsnid  4341  dfopg  4400  csbopg  4420  opprc  4424  csbuni  4466  intsng  4512  riinn0  4595  iinxsng  4600  iunxprg  4607  propeqop  4970  csbmpt12  5010  xpriindi  5258  relop  5272  dmxp  5344  riinint  5382  csbres  5399  resabs1  5427  resabs2  5429  resima2OLD  5433  xpssres  5434  dmressnsn  5438  resopab2  5448  imasng  5487  djudisj  5561  rnxp  5564  xpima  5576  xpima1  5577  xpima2  5578  dmsnsnsn  5613  rnsnopg  5614  rnpropg  5615  mptiniseg  5629  dfco2a  5635  relcoi2  5663  relcoi1  5664  unixp  5668  predep  5706  onfr  5763  iotaval  5862  iotanul  5866  funtp  5945  fnun  5997  fnresdisj  6001  fnima  6010  fnimaeq0  6013  fresaunres2  6076  fresaunres1  6077  fcoi1  6078  f1orescnv  6152  foun  6155  resdif  6157  f1oprswap  6180  tz6.12-2  6182  fveu  6183  tz6.12-1  6210  csbfv12  6231  csbfv2g  6232  fvun  6268  fvun2  6270  fvopab3ig  6278  fvmptnf  6302  fvopab5  6309  intpreima  6346  fimacnvinrn  6348  fimacnvinrn2  6349  fveqressseq  6355  f1oresrab  6395  residpr  6409  ressnop0  6420  fvunsn  6445  fsnunfv  6453  fvpr1  6456  fvpr2  6457  fvpr1g  6458  fvpr2g  6459  fvtp1  6460  fvtp2  6461  fvtp3  6462  fvtp1g  6463  fvtp2g  6464  fvtp3g  6465  tpres  6466  fpropnf1  6524  f12dfv  6529  f13dfv  6530  nvof1o  6536  fveqf1o  6557  f1oiso2  6602  riotaund  6647  ovprc  6683  csbov12g  6689  resoprab2  6757  fnoprabg  6761  ovidig  6778  ovigg  6781  ov6g  6798  ovconst2  6814  nssdmovg  6816  ndmovg  6817  offval2f  6909  offval2  6914  orduniss2  7033  1stnpr  7172  2ndnpr  7173  ot1stg  7182  ot2ndg  7183  ot3rdg  7184  opabn1stprc  7228  brovpreldm  7254  bropopvvv  7255  bropfvvvvlem  7256  fmpt2co  7260  curry1  7269  curry2  7272  fparlem3  7279  fparlem4  7280  fnwelem  7292  suppsnop  7309  supp0cosupp0  7334  imacosupp  7335  tpostpos2  7373  mpt2curryd  7395  wfrlem4  7418  wfrlem13  7427  tz7.44-2  7503  tz7.44-3  7504  rdgsucmptnf  7525  rdglim2  7528  fr0g  7531  frsucmptn  7534  seqom0g  7551  oa1suc  7611  om1  7622  oe1  7624  oarec  7642  oacomf1o  7645  nnm1  7728  nnm2  7729  dfec2  7745  errn  7764  ralxpmap  7907  ixpsnval  7911  ixpint  7935  domunsncan  8060  enfixsn  8069  domunsn  8110  fodomr  8111  domss2  8119  mapen  8124  xpmapenlem  8127  phplem2  8140  unxpdomlem1  8164  findcard2  8200  domunfican  8233  mapfien  8313  marypha1lem  8339  marypha2lem4  8344  supval2  8361  supsn  8378  eqinf  8390  infval  8392  infsn  8410  infempty  8412  ordtypecbv  8422  ordtypelem3  8425  oi0  8433  wemapso2  8458  brwdom2  8478  infdifsn  8554  cantnfs  8563  cantnfval  8565  cantnflt  8569  cantnff  8571  cantnfp1  8578  oemapso  8579  wemapwe  8594  cnfcomlem  8596  cnfcom2lem  8598  cnfcom3lem  8600  rankxplim2  8743  infxpenlem  8836  infxpenc  8841  infxpenc2lem1  8842  fseqenlem1  8847  dfac12r  8968  kmlem11  8982  pwcda1  9016  onacda  9019  ackbij1lem1  9042  ackbij1lem2  9043  ackbij1lem14  9055  ackbij1lem16  9057  ackbij1lem18  9059  ackbij2lem3  9063  fictb  9067  cfsmolem  9092  cfsmo  9093  infpssrlem1  9125  enfin2i  9143  fin23lem19  9158  fin23lem30  9164  isf32lem4  9178  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  isf34lem7  9201  isf34lem6  9202  fin1a2lem11  9232  ituniiun  9244  hsmexlem2  9249  hsmexlem4  9251  domtriomlem  9264  domtriom  9265  axdc3lem4  9275  zorn2g  9325  axdc  9343  fpwwe2lem13  9464  fpwwe  9468  canthwelem  9472  canthp1lem1  9474  pwfseqlem2  9481  pwfseqlem3  9482  wunex2  9560  wuncval2  9569  nqereu  9751  recrecnq  9789  ltaddnq  9796  halfnq  9798  ltrnq  9801  archnq  9802  addclprlem1  9838  addclprlem2  9839  mulclprlem  9841  distrlem4pr  9848  1idpr  9851  prlem934  9855  ltexprlem7  9864  ltaprlem  9866  prlem936  9869  mulcmpblnrlem  9891  0idsr  9918  1idsr  9919  recexsrlem  9924  sqgt0sr  9927  map2psrpr  9931  mulresr  9960  ax1rid  9982  axcnre  9985  ssxr  10107  addid2  10219  negid  10328  subneg  10330  negneg  10331  dfinfre  11004  infrenegsup  11006  2times  11145  rpnnen1  11820  rexneg  12042  xaddpnf2  12058  xaddmnf2  12060  x2times  12129  supxrmnf  12147  prunioo  12301  ioojoin  12303  fzpreddisj  12390  fseq1p1m1  12414  prednn  12462  prednn0  12463  fz0add1fz1  12537  quoremz  12654  quoremnn0ALT  12656  intfracq  12658  uzenom  12763  axdc4uzlem  12782  mptnn0fsuppd  12798  seq1i  12815  seqp1i  12817  seqf1olem2  12841  seqof  12858  sqval  12922  iexpcyc  12969  binom3  12985  faclbnd  13077  faclbnd2  13078  bcn1  13100  hashkf  13119  hashgval  13120  hashdom  13168  hashxplem  13220  hashfun  13224  hashbclem  13236  hashbc  13237  hashf1lem1  13239  hashf1lem2  13240  fz1isolem  13245  csbwrdg  13334  ccatlid  13369  ccatalpha  13375  s1val  13378  swrd00  13418  swrd0  13434  cats1fvn  13603  cats1fv  13604  s2prop  13652  s3tpop  13654  s4prop  13655  s4dom  13664  ofccat  13708  ofs2  13710  dfid6  13768  relexpcnv  13775  relexpnnrn  13785  relexpaddg  13793  shftlem  13808  shftuz  13809  shftidt  13822  reim0  13858  remullem  13868  sqrlem5  13987  resqrex  13991  absexpz  14045  absimle  14049  sqreulem  14099  amgm2  14109  rlimdm  14282  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  summo  14448  fsum  14451  sumsnf  14473  sumsn  14475  sumsns  14479  isumge0  14497  fsump1i  14500  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsumrlim  14543  fsumo1  14544  fsumiun  14553  hashrabrex  14557  hashuni  14558  ackbijnn  14560  binom11  14564  incexclem  14568  incexc  14569  isumsplit  14572  geo2sum  14604  geomulcvg  14607  mertens  14618  prodmo  14666  fprod  14671  prodsn  14692  prodsnf  14694  prodsns  14702  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  0risefac  14769  bpolylem  14779  bpolyval  14780  bpoly1  14782  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  efgt1p2  14844  efgt1p  14845  resinval  14865  recosval  14866  cosadd  14895  ef01bndlem  14914  eirrlem  14932  rpnnen2lem11  14953  ruclem1  14960  ruclem4  14963  ruclem6  14964  ruclem7  14965  divalglem1  15117  divalglem9  15124  bits0  15150  bitsinv2  15165  sadaddlem  15188  bitsres  15195  smup0  15201  smuval2  15204  bezoutlem2  15257  bezoutlem4  15259  seq1st  15284  algr0  15285  eucalg  15300  phiprmpw  15481  phiprm  15482  crth  15483  eulerthlem2  15487  prmdiv  15490  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  pceu  15551  pcmpt  15596  pcfac  15603  prmpwdvds  15608  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmrec  15626  4sqlem5  15646  mul4sqlem  15657  vdwap1  15681  vdwlem6  15690  vdwlem10  15694  vdwlem12  15696  hashbcval  15706  0hashbc  15711  ramub1lem2  15731  ramcl  15733  cshwsiun  15806  cshws0  15808  ndxid  15883  setsdm  15892  setsfun0  15894  setscom  15903  setsnid  15915  elbasfv  15920  elbasov  15921  ressval  15927  ressbas  15930  ressbasss  15932  resslem  15933  ressinbas  15936  firest  16093  topnval  16095  prdsval  16115  prdsdsval2  16144  prdsdsval3  16145  pwsval  16146  pwsplusgval  16150  pwsmulrval  16151  pwsle  16152  pwsvscafval  16154  imasdsval2  16176  imasaddvallem  16189  divsfval  16207  xpsc0  16220  xpsc1  16221  xpsval  16232  mrcfval  16268  mrisval  16290  mreexmrid  16303  mreexexlem2d  16305  mreexexlem4d  16307  cidfval  16337  homffval  16350  homfeqval  16357  comfffval  16358  comfeqval  16368  oppcval  16373  oppchomfval  16374  oppcbas  16378  monfval  16392  oppcmon  16398  oppcepi  16399  sectffval  16410  invffval  16418  invf  16428  oppcinv  16440  rescval  16487  idfuval  16536  idfu2nd  16537  resf2nd  16555  funcres2c  16561  ressffth  16598  fucval  16618  fucbas  16620  fuchom  16621  fucid  16631  homarcl  16678  homafval  16679  homaval  16681  homadm  16690  homacd  16691  arwval  16693  idafval  16707  setcval  16727  setcid  16736  catcval  16746  catchomfval  16748  catcid  16753  estrcval  16764  estrcid  16774  xpcval  16817  xpcbas  16818  xpchomfval  16819  xpccofval  16822  xpccatid  16828  xpcid  16829  1stfval  16831  2ndfval  16834  prfval  16839  xpcpropd  16848  evlfval  16857  evlf2  16858  curfval  16863  curf1  16865  curf2  16869  uncfval  16874  uncf1  16876  uncf2  16877  diagval  16880  diag11  16883  diag12  16884  diag2  16885  curf2ndf  16887  hofval  16892  yonval  16901  oppcyon  16909  oyoncl  16910  yonedalem21  16913  yonedalem22  16918  yonedalem3b  16919  pltfval  16959  lubfun  16980  glbfun  16993  joinfval  17001  joinval  17005  meetfval  17015  meetval  17019  p0val  17041  p1val  17042  oduglb  17139  odumeet  17140  odulub  17141  odujoin  17142  oduclatb  17144  ipoval  17154  ipopos  17160  psref  17208  psrn  17209  dirref  17235  dirge  17237  plusffval  17247  mgm1  17257  grpidval  17260  gsumpropd2lem  17273  gsum0  17278  sgrp1  17293  ismnd  17297  prdsidlem  17322  mnd1  17331  mnd1id  17332  subsubm  17357  pwspjmhm  17368  frmdval  17388  frmdbas  17389  frmdplusg  17391  frmdadd  17392  vrmdfval  17393  frmd0  17397  grpinvfval  17460  grpsubfval  17464  grp1  17522  prdsinvlem  17524  pwsinvg  17528  mulgfval  17542  mulg2  17550  subsubg  17617  cycsubgcl  17620  eqgfval  17642  conjsubg  17692  cntrval  17752  cntzfval  17753  cntzval  17754  cntzrcl  17760  oppgplusfval  17778  oppgmnd  17784  oppggrp  17787  oppginv  17789  symgval  17799  symgbas  17800  symghash  17805  symgplusg  17809  symg1hash  17815  symg1bas  17816  symg2hash  17817  symg2bas  17818  lactghmga  17824  fvcosymgeq  17849  f1omvdco2  17868  pmtrfval  17870  pmtrfrn  17878  symggen  17890  pmtr3ncomlem1  17893  pmtrdifellem2  17897  psgnunilem2  17915  psgnunilem4  17917  psgnfval  17920  psgneldm2  17924  psgnfvalfi  17933  psgnsn  17940  odfval  17952  gexval  17993  sylow1  18018  subgslw  18031  sylow2b  18038  sylow3lem5  18046  sylow3  18048  lsmfval  18053  oppglsm  18057  lsmdisj3  18096  lsmdisj2r  18098  lsmdisj3r  18099  lsmdisj2a  18100  lsmdisj2b  18101  pj1fval  18107  pj2f  18111  pj1id  18112  efgrcl  18128  efgtf  18135  efgredleme  18156  frgpval  18171  vrgpfval  18179  frgpupf  18186  frgpup1  18188  frgpup2  18189  frgpup3lem  18190  subcmn  18242  frgpnabllem1  18276  frgpnabllem2  18277  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzaddlem  18321  gsumconstf  18335  gsumzunsnd  18355  gsum2dlem1  18369  gsum2dlem2  18370  gsum2d  18371  gsum2d2  18373  gsumxp  18375  pwsgsum  18378  dprdf1o  18431  dprdcntz2  18437  dprd2da  18441  dprd2d2  18443  dpjfval  18454  ablfac1lem  18467  pgpfac1lem3  18476  pgpfac1lem4  18477  pgpfaclem1  18480  ablfaclem3  18486  ablfac2  18488  mgpplusg  18493  mgpress  18500  ringidval  18503  srgbinomlem4  18543  ring1  18602  gsumdixp  18609  prdsmgp  18610  pwsmgp  18618  opprmulfval  18625  opprring  18631  dvdsrval  18645  isunit  18657  unitmulcl  18664  unitgrp  18667  invrfval  18673  dvrfval  18684  isirred  18699  isdrng2  18757  isdrngrd  18773  subrguss  18795  subrgunit  18798  subsubrg  18806  abvfval  18818  staffval  18847  scaffval  18881  lmodpropd  18926  mptscmfsupp0  18928  lssset  18934  islss  18935  lssuni  18940  lsslss  18961  lspfval  18973  lmhmvsca  19045  pwssplit1  19059  lmhmpropd  19073  islbs  19076  lsppr  19093  lbsextlem4  19161  lidlmcl  19217  2idlval  19233  2idlcpbl  19234  crngridl  19238  rrgval  19287  assapropd  19327  aspval  19328  asclfval  19334  psrval  19362  psrbaglefi  19372  psrass1lem  19377  psrbas  19378  psrplusg  19381  psradd  19382  psrmulr  19384  psrvscafval  19390  resspsrbas  19415  mvrfval  19420  mplval  19428  mplsubglem2  19436  mpl0  19441  mpl1  19444  mplmonmul  19464  mplcoe1  19465  ltbval  19471  ltbwe  19472  opsrval  19474  opsrle  19475  opsrtoslem2  19485  mplascl  19496  mplasclf  19497  mplmon2cl  19500  mplmon2mul  19501  mplind  19502  evlseu  19516  mpfrcl  19518  evlsval  19519  evlsscasrng  19526  vr1val  19562  ply1val  19564  coe1fval  19575  mptcoe1fsupp  19585  psr1sca2  19621  ply10s0  19626  ply1ascl  19628  ply1coe  19666  coe1fzgsumdlem  19671  gsummoncoe1  19674  lply1binomsc  19677  evls1fval  19684  evls1rhmlem  19686  evl1fval  19692  evl1val  19693  evl1fval1  19695  evls1var  19702  evls1scasrng  19703  evl1vsd  19708  evl1expd  19709  pf1rcl  19713  pf1mpf  19716  pf1ind  19719  evl1gsumdlem  19720  evl1gsumd  19721  evl1gsumadd  19722  evl1varpw  19725  evl1gsummon  19729  expmhm  19815  mulgrhm  19846  zrhval2  19857  zlmval  19864  zlmlem  19865  zlmvsca  19870  chrval  19873  znval  19883  znzrh2  19894  znf1o  19900  frgpcyg  19922  ipffval  19993  phssip  20003  ocvfval  20010  ocvval  20011  elocv  20012  cssval  20026  thlval  20039  thlbas  20040  thlle  20041  thloc  20043  pjfval  20050  dsmmbas2  20081  dsmmfi  20082  frlmval  20092  frlmpws  20094  frlmlss  20095  frlmbas  20099  frlmplusgval  20107  frlmsubgval  20108  frlmvscafval  20109  frlmgsum  20111  frlmsslss  20113  frlmsslss2  20114  frlmip  20117  frlmphl  20120  uvcfval  20123  frlmssuvc1  20133  frlmssuvc2  20134  frlmsslsp  20135  mamufval  20191  mamuvs1  20211  mamuvs2  20212  matval  20217  matrcl  20218  matvscl  20237  matsubgcell  20240  mat1ov  20254  matsc  20256  mamutpos  20264  mat0dim0  20273  mat0dimid  20274  mat0dimscm  20275  mat1dimmul  20282  mat1rhmelval  20286  dmatval  20298  scmatval  20310  scmatscmide  20313  scmatscmiddistr  20314  scmatscm  20319  scmataddcl  20322  scmatsubcl  20323  smatvscl  20330  scmatghm  20339  mat1scmat  20345  mvmulfval  20348  marrepfval  20366  marepvfval  20371  mulmarep1el  20378  submafval  20385  mdetfval  20392  nfimdetndef  20395  mdetfval1  20396  mdetrlin  20408  mdet0  20412  mdetralt  20414  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  madufval  20443  maducoeval2  20446  madutpos  20448  madugsum  20449  madurid  20450  minmar1fval  20452  invrvald  20482  cramer0  20496  cpmat  20514  mat2pmatfval  20528  mat2pmat1  20537  cpm2mfval  20554  decpmataa0  20573  decpmatid  20575  decpmatmulsumfsupp  20578  monmatcollpw  20584  pmatcollpwfi  20587  pmatcollpwscmatlem1  20594  pm2mpval  20600  idpm2idmp  20606  mp2pm2mplem4  20614  pm2mpmhmlem2  20624  monmat2matmon  20629  chmatval  20634  chpmatfval  20635  chp0mat  20651  fvmptnn04if  20654  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  cayleyhamilton0  20694  istps  20738  tgidm  20784  iuncld  20849  clsval2  20854  tgrest  20963  restcld  20976  resstopn  20990  ordtval  20993  ordtbas2  20995  ordtrest  21006  ordtrest2lem  21007  lecldbas  21023  iscnp2  21043  ssidcn  21059  pnrmopn  21147  nrmsep  21161  isreg2  21181  imacmp  21200  cmpsub  21203  cmpfi  21211  comppfsc  21335  kgeni  21340  llycmpkgen2  21353  kgencn3  21361  elptr2  21377  ptbasfi  21384  ptuni  21397  ptval2  21404  ptpjcn  21414  ptpjopn  21415  ptclsg  21418  xkoccn  21422  ptcnp  21425  txcnmpt  21427  txcn  21429  pthaus  21441  hausdiag  21448  xkohaus  21456  xkoptsub  21457  cnmptk2  21489  cnmpt2k  21491  idqtop  21509  qtoprest  21520  kqval  21529  kqdisj  21535  kqcldsat  21536  pt1hmeo  21609  ptunhmeo  21611  trfil2  21691  uzrest  21701  trufil  21714  txflf  21810  fclsrest  21828  ptcmplem1  21856  tmdmulg  21896  tmdgsum  21899  tmdgsum2  21900  subgntr  21910  opnsubg  21911  clsnsg  21913  cldsubg  21914  snclseqg  21919  qustgphaus  21926  tsmsres  21947  tsmsmhm  21949  tsmsxplem1  21956  ustssco  22018  trust  22033  restutopopn  22042  utopsnneiplem  22051  ussval  22063  isusp  22065  ressuss  22067  ressust  22068  tuslem  22071  tustopn  22075  fmucndlem  22095  prdsdsf  22172  prdsxmet  22174  ressprdsds  22176  imasdsf1olem  22178  xpsdsval  22186  blres  22236  mopnval  22243  tmsval  22286  tmstopn  22290  blcld  22310  ressxms  22330  ressms  22331  prdsmslem1  22332  prdsxmslem1  22333  prdsxmslem2  22334  tmsxpsmopn  22342  metustid  22359  metucn  22376  nmfval  22393  nmfval2  22395  tngval  22443  tnglem  22444  tngbas  22445  tngplusg  22446  tng0  22447  tngmulr  22448  tngsca  22449  tngvsca  22450  tngip  22451  tngds  22452  tngtset  22453  tngngp  22458  tngngp3  22460  tngnrg  22478  ngpocelbl  22508  nmofval  22518  nghmfval  22526  isnghm  22527  remetdval  22592  iccntr  22624  icccmplem2  22626  metdseq0  22657  metnrmlem3  22664  expcn  22675  divccncf  22709  cncfmet  22711  cncfcn  22712  pcoptcl  22821  pcopt  22822  pcopt2  22823  pcorevlem  22826  pcophtb  22829  om1val  22830  pi1val  22837  pi1xfrcnv  22857  isncvsngp  22949  ncvsm1  22954  cphsubrglem  22977  ipcau2  23033  bcth  23126  rrxval  23175  ehlval  23193  minveclem2  23197  minveclem3a  23198  minveclem3b  23199  minveclem4  23203  minveclem6  23205  pjthlem1  23208  ovolfsval  23239  elovolmr  23244  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem2  23271  ovolicc1  23284  mblvol  23298  inmbl  23310  difmbl  23311  volfiniun  23315  voliunlem1  23318  voliunlem2  23319  voliunlem3  23320  iunmbl  23321  voliun  23322  icombl  23332  ioombl  23333  ovolioo  23336  volioo  23337  ioorinv2  23343  uniiccdif  23346  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  dyadmbl  23368  vitali  23382  mbfconstlem  23396  mbfss  23413  mbfposb  23420  ismbf3d  23421  mbfinf  23432  mbflimsup  23433  0pval  23438  i1f0rn  23449  itg1addlem5  23467  i1fpos  23473  i1fposd  23474  itg1climres  23481  mbfi1fseq  23488  itg2const  23507  itg2monolem1  23517  itg2i1fseq  23522  isibl  23532  isibl2  23533  itg0  23546  iblcnlem1  23554  itgcnlem  23556  iblss2  23572  iblconst  23584  itgconst  23585  itgfsum  23593  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2lem1  23598  itgmulc2  23600  itgabs  23601  itgsplitioo  23604  bddmulibl  23605  ditgpos  23620  ditgneg  23621  ellimc2  23641  limcflf  23645  limcmpt2  23648  dvbsss  23666  perfdvf  23667  dvreslem  23673  dvres2lem  23674  dvres3a  23678  cpnres  23700  dvaddbr  23701  dvmulbr  23702  dvexp  23716  dvmptres3  23719  dvmptfsum  23738  dvsincos  23744  dvlipcn  23757  dvlip2  23758  dvivthlem1  23771  dvne0  23774  lhop1lem  23776  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcvx  23783  dvfsumrlim  23794  ftc1a  23800  ftc1lem4  23802  ftc1lem6  23804  itgparts  23810  itgsubstlem  23811  tdeglem4  23820  mdegfval  23822  mdegvscale  23835  uc1pval  23899  mon1pval  23901  q1pval  23913  r1pval  23916  ply1remlem  23922  fta1blem  23928  ig1pval  23932  elplyd  23958  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  dgrub  23990  dgrlb  23992  coeid  23994  dgreq0  24021  dgrcolem1  24029  dgrcolem2  24030  plycjlem  24032  plydivlem3  24050  plydivlem4  24051  plydiveu  24053  plydivalg  24054  plyremlem  24059  plyrem  24060  quotcan  24064  vieta1lem2  24066  elqaalem2  24075  qaa  24078  aareccl  24081  aaliou3lem3  24099  taylfval  24113  itgulm2  24163  pserval  24164  pserulm  24176  psercn  24180  pserdvlem2  24182  abelthlem6  24190  abelthlem9  24194  ef2kpi  24230  sin2pim  24237  cos2pim  24238  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  sinhalfpip  24244  sinhalfpim  24245  coshalfpip  24246  coshalfpim  24247  tangtx  24257  tanregt0  24285  efif1olem4  24291  logneg  24334  abslogle  24364  dvrelog  24383  logcnlem3  24390  dvlog  24397  efopnlem2  24403  logtayl  24406  1cxp  24418  ecxp  24419  cxpsqrt  24449  dvsqrt  24483  dvcnsqrt  24485  root1eq1  24496  cxpeq  24498  logb1  24507  elogb  24508  ang180lem1  24539  ang180lem2  24540  lawcos  24546  heron  24565  dcubic2  24571  mcubic  24574  cubic2  24575  binom4  24577  dquartlem1  24578  quart1lem  24582  quart1  24583  quartlem1  24584  asinlem  24595  asinlem2  24596  efiasin  24615  asinsin  24619  atancj  24637  atanlogaddlem  24640  atanlogsublem  24642  efiatan2  24644  2efiatan  24645  atantan  24650  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  atantayl3  24666  leibpi  24669  log2tlbnd  24672  birthdaylem2  24679  birthdaylem3  24680  rlimcnp  24692  amgmlem  24716  emcllem5  24726  wilthlem2  24795  wilthlem3  24796  ftalem2  24800  ftalem4  24802  ftalem5  24803  ftalem7  24805  basellem2  24808  basellem3  24809  basellem8  24814  basellem9  24815  vmappw  24842  0sgm  24870  mule1  24874  mumul  24907  sqff1o  24908  fsumdvdscom  24911  musum  24917  musumsum  24918  muinv  24919  fsumdvdsmul  24921  1sgmprm  24924  1sgm2ppw  24925  ppiub  24929  chtub  24937  fsumvma  24938  dchrval  24959  dchrrcl  24965  dchrinvcl  24978  dchrptlem1  24989  dchrptlem2  24990  dchrpt  24992  dchrsum2  24993  sumdchr2  24995  bposlem9  25017  lgslem1  25022  lgsdilem  25049  lgsqrlem1  25071  lgsqrlem4  25074  gausslemma2dlem4  25094  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  m1lgs  25113  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2sqlem8  25151  dchrisum  25181  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem2a  25206  logdivsum  25222  mulog2sumlem1  25223  2vmadivsumlem  25229  logsqvma2  25232  log2sumbnd  25233  selberglem1  25234  selberg  25237  chpdifbndlem1  25242  selberg3lem1  25246  selberg4lem1  25249  pntrmax  25253  pntsval  25261  pntsval2  25265  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem3  25281  pntlemd  25283  pntlemc  25284  pntlemb  25286  pntlemr  25291  pntlemf  25294  pntlemk  25295  pntlemo  25296  padicabvcxp  25321  ostth2lem4  25325  ostth3  25327  iscgrg  25407  tgcgr4  25426  tglng  25441  legval  25479  ishlg  25497  mirval  25550  mirfv  25551  mirf  25555  midexlem  25587  lmif  25677  islmib  25679  ttglem  25756  axsegconlem1  25797  axlowdimlem9  25830  axlowdimlem12  25833  axlowdimlem17  25838  opvtxval  25883  opiedgval  25886  funvtxdmge2val  25891  funiedgdmge2val  25892  funvtxdm2val  25893  funiedgdm2val  25894  structiedg0val  25911  snstriedgval  25930  edgopval  25944  edgov  25945  edgstruct  25946  edg0iedg0OLD  25950  upgredg  26032  edglnl  26038  usgrf1oedg  26099  ushgredgedg  26121  ushgredgedgloop  26123  lfuhgr1v0e  26146  griedg0ssusgr  26157  subgrprop3  26168  0uhgrsubgr  26171  nbupgruvtxres  26308  cplgr3v  26331  cplgrop  26333  cusgrexi  26339  structtocusgr  26342  cusgrsize  26350  vtxdgfval  26363  vtxdun  26377  vtxdlfgrval  26381  vtxd0nedgb  26384  1hevtxdg1  26402  1egrvtxdg1  26405  1egrvtxdg0  26407  uspgrloopvtx  26411  uspgrloopiedg  26413  uspgrloopedg  26414  umgr2v2evtx  26417  umgr2v2eiedg  26419  vdegp1ai  26432  vdegp1bi  26433  vtxdginducedm1lem3  26437  vtxdginducedm1  26439  finsumvtxdg2size  26446  rgrusgrprc  26485  edginwlkOLD  26531  upgriswlk  26537  wlkres  26567  wlkp1lem5  26574  wlkp1lem6  26575  wlkp1lem7  26576  wlkp1lem8  26577  trlreslem  26596  upgrtrls  26598  upgrspthswlk  26634  pthdlem2  26664  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  crctcshlem4  26712  wwlks  26727  wwlksnextwrd  26792  2wlkdlem3  26823  2wlkond  26833  clwwlknclwwlkdifnum  26874  clwwlks  26879  clwwlksn2  26910  clwwlksnscsh  26940  clwlksfoclwwlk  26963  clwlksf1clwwlklem0  26964  clwlksf1clwwlk  26969  clwwlksndisj  26973  0wlkon  26981  1wlkdlem4  27000  1pthond  27004  3wlkdlem3  27021  3cycld  27038  3cyclpd  27039  eupthvdres  27095  eupth2lem3  27096  eucrct2eupth  27105  frgrwopregasn  27180  frgrwopregbsn  27181  numclwlk1lem2foalem  27222  numclwwlk3lem  27241  numclwwlk5  27246  numclwwlk7  27249  ex-ima  27299  ex-ceil  27305  grpoidval  27367  grpoinvfval  27376  grpodivfval  27388  vafval  27458  smfval  27460  vsfval  27488  nvm1  27520  nvmtri  27526  imsmet  27546  smcn  27553  dipfval  27557  dipcj  27569  sspval  27578  lnoval  27607  nmoofval  27617  bloval  27636  0ofval  27642  nmlno0  27650  nmlnoubi  27651  blocnilem  27659  ajfval  27664  hmoval  27665  dipdir  27697  dipass  27700  pythi  27705  ajfun  27716  ubthlem3  27728  ubth  27729  minvecolem2  27731  htth  27775  hv2times  27918  bcseqi  27977  normpythi  27999  hhssnvt  28122  hhsssh  28126  pjhthlem1  28250  chsupid  28271  pjoc1i  28290  h1de2i  28412  spanunsni  28438  cmcmlem  28450  cmbr3i  28459  fh1  28477  fh2  28478  nonbooli  28510  hoival  28614  hoico1  28615  hoico2  28616  hosubid1  28657  ho2times  28678  eigposi  28695  nmcopexi  28886  lnfnmuli  28903  nmcfnexi  28910  pjnmopi  29007  pjclem3  29056  pjadj2coi  29063  pj3lem1  29065  strlem3a  29111  strlem4  29113  hstrlem3a  29119  hstrlem4  29121  dmdbr5  29167  mdexchi  29194  superpos  29213  atomli  29241  atcvatlem  29244  chirredlem2  29250  chirredlem3  29251  atabsi  29260  mdsymlem1  29262  dmdbr6ati  29282  difuncomp  29369  disjuniel  29410  xpdisjres  29411  difres  29413  imadifxp  29414  funresdm1  29416  fcoinver  29418  opabdm  29423  opabrn  29424  fnresin  29430  elimampt  29438  acunirnmpt2f  29461  ofpreima  29465  funcnvmptOLD  29467  funcnvmpt  29468  padct  29497  hashunif  29562  fsumiunle  29575  dpval  29597  dpfrac1  29599  dpfrac1OLD  29600  ressnm  29651  sgnsv  29727  archirngz  29743  archiabllem2c  29749  gsummpt2co  29780  resvval  29827  resvsca  29830  resvlem  29831  resv0g  29836  pmtridf1o  29856  pmtridfv1  29857  pmtridfv2  29858  smatrcl  29862  smatlem  29863  submatminr1  29876  lmatfval  29880  lmatcl  29882  lmat22e11  29884  locfinref  29908  prsss  29962  ordtprsval  29964  ordtrestNEW  29967  ordtrest2NEWlem  29968  ordtconnlem1  29970  xrge0iifhom  29983  xrge0pluscn  29986  zlmnm  30010  nmmulg  30012  qqh0  30028  qqh1  30029  qqhre  30064  esumval  30108  esumfzf  30131  esumpfinval  30137  esumpfinvalf  30138  esumcvg  30148  esum2dlem  30154  ldgenpisyslem1  30226  measun  30274  volmeas  30294  ddemeas  30299  oms0  30359  omssubadd  30362  0elcarsg  30369  difelcarsg  30372  carsgclctunlem1  30379  sibf0  30396  sibff  30398  sitgclg  30404  eulerpartlemgu  30439  eulerpartlemgs2  30442  sseqfn  30452  sseqf  30454  probfinmeasbOLD  30490  probmeasb  30492  dstrvprob  30533  ballotlem4  30560  ballotlem1c  30569  ballotlemgun  30586  ccatmulgnn0dir  30619  ofcs2  30622  ftc2re  30676  repr0  30689  reprlt  30697  chtvalz  30707  hgt750lemb  30734  brafs  30750  bnj941  30843  bnj1143  30861  bnj98  30937  bnj944  31008  bnj966  31014  bnj1416  31107  bnj1463  31123  derangsn  31152  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  subfaclim  31170  erdszelem10  31182  erdsze  31184  erdsze2lem2  31186  kur14  31198  pconnconn  31213  txpconn  31214  txsconnlem  31222  cvxpconn  31224  cvmscbv  31240  cvmscld  31255  cvmsss2  31256  cvmliftlem8  31274  cvmliftlem10  31276  cvmliftlem13  31278  cvmliftlem15  31280  cvmlift2  31298  cvmliftphtlem  31299  cvmlift3  31310  mrexval  31398  mexval  31399  mexval2  31400  mdvval  31401  mvrsval  31402  mrsubffval  31404  mrsubfval  31405  mrsubrn  31410  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  mrsubco  31418  mrsubvrs  31419  msubffval  31420  msubfval  31421  elmsubrn  31425  msubrn  31426  msubf  31429  mvhfval  31430  mpstval  31432  msrfval  31434  msrf  31439  mstaval  31441  mclsrcl  31458  mclsval  31460  mppsval  31469  mthmval  31472  sinccvglem  31566  circum  31568  faclimlem1  31629  rdgprc0  31699  dfrdg2  31701  trpredtr  31730  trpredmintr  31731  trpred0  31736  trpredrec  31738  frrlem4  31783  noextend  31819  noextendlt  31822  nolesgn2ores  31825  nodense  31842  nosupdm  31850  nosupbday  31851  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  noetalem2  31864  noetalem3  31865  rankaltopb  32086  fvtransport  32139  fvray  32248  fvline  32251  cldbnd  32321  clsun  32323  neibastop2  32356  bj-csbprc  32904  bj-xpima1sn  32943  bj-xpima2sn  32945  bj-ndxarg  33029  bj-ndxid  33030  bj-finsumval0  33147  csbpredg  33172  csbwrecsg  33173  csbrdgg  33175  csboprabg  33176  mptsnunlem  33185  dissneqlem  33187  rdgeqoa  33218  csbfinxpg  33225  finxpreclem4  33231  curf  33387  uncf  33388  lindsdom  33403  lindsenlbs  33404  ptrest  33408  poimirlem2  33411  poimirlem3  33412  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem30  33439  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  voliunnfl  33453  mbfposadd  33457  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  itgaddnclem2  33469  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem1  33476  itgmulc2nc  33478  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  dvasin  33496  areacirclem1  33500  areacirclem5  33504  areacirc  33505  cocnv  33520  sstotbnd2  33573  sstotbnd  33574  equivbnd2  33591  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  cnpwstotbnd  33596  ismtyres  33607  heiborlem3  33612  heiborlem4  33613  heibor  33620  repwsmet  33633  rrnequiv  33634  iccbnd  33639  idrval  33656  ismndo2  33673  exidcl  33675  exidreslem  33676  fsumshftd  34237  lshpset  34265  lsatset  34277  lcvfbr  34307  lflset  34346  lkrfval  34374  lfl1dim  34408  ldualset  34412  ldualsmul  34422  cmtfvalN  34497  cvrfval  34555  pats  34572  glbconxN  34664  llnset  34791  lplnset  34815  lvolset  34858  dalem4  34951  dalem6  34954  dalem7  34955  dalem11  34960  dalem12  34961  dalem24  34983  dalem56  35014  lineset  35024  pointsetN  35027  psubspset  35030  pmapfval  35042  pmapglb  35056  paddfval  35083  pmod2iN  35135  pclfvalN  35175  polfvalN  35190  psubclsetN  35222  osumcllem3N  35244  watfvalN  35278  lhpset  35281  4atexlemswapqr  35349  4atexlemc  35355  lautset  35368  pautsetN  35384  ldilset  35395  ltrnset  35404  dilfsetN  35439  trnfsetN  35442  trlset  35448  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme5  35527  cdleme7c  35532  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme11g  35552  cdleme15b  35562  cdleme17a  35573  cdleme19a  35591  cdleme20aN  35597  cdleme20bN  35598  cdleme22e  35632  cdleme22eALTN  35633  cdleme23c  35639  cdleme25b  35642  cdleme27a  35655  cdleme29b  35663  cdleme31sde  35673  cdlemefr27cl  35691  cdleme35b  35738  cdleme35c  35739  cdleme37m  35750  cdleme39a  35753  cdleme40v  35757  cdleme42f  35768  cdleme42h  35770  cdleme43dN  35780  cdlemeg46rjgN  35810  cdlemeg46v1v2  35814  cdlemg2kq  35890  cdlemg4b1  35897  cdlemg4b2  35898  cdlemg4  35905  trlcoabs2N  36010  cdlemg46  36023  tgrpset  36033  tendoset  36047  erngset  36088  erngset-rN  36096  cdlemh1  36103  cdlemi2  36107  cdlemk2  36120  cdlemk8  36126  cdlemk13  36140  cdlemk33N  36197  cdlemk34  36198  cdlemk40  36205  cdlemk41  36208  cdlemkid1  36210  cdlemkfid2N  36211  cdlemkid3N  36221  cdlemk42  36229  cdlemk45  36235  cdlemk55a  36247  dvaset  36293  dvabase  36295  dvafplusg  36296  dvafmulr  36299  diafval  36320  dvhset  36370  dvhbase  36372  dvhfmulr  36374  dvhfvadd  36380  dvhlveclem  36397  cdlemm10N  36407  docafvalN  36411  djafvalN  36423  dibfval  36430  diblss  36459  dicfval  36464  dihfval  36520  dihmeetlem11N  36606  dihmeetlem19N  36614  dih1dimatlem0  36617  dihglb2  36631  dochfval  36639  djhfval  36686  dihprrnlem1N  36713  dihprrnlem2  36714  dihprrn  36715  dvh3dim  36735  dvh3dim3N  36738  lpolsetN  36771  lclkrlem2m  36808  lclkrlem2v  36817  lcfrvalsnN  36830  lcfrlem1  36831  lcf1o  36840  lcfrlem18  36849  lcfrlem23  36854  lcfrlem33  36864  lcdval  36878  lcdvbase  36882  lcdsca  36888  lcdsmul  36891  lcd0v  36900  lcdlss  36908  lcdlsp  36910  mapdfval  36916  hvmapfval  37048  hdmap1fval  37086  hdmapfval  37119  hgmapfval  37178  hdmapip1  37208  hlhilset  37226  hlhilslem  37230  hlhilsbase2  37234  hlhilsplus2  37235  hlhilsmul2  37236  hlhils0  37237  hlhils1N  37238  hlhilnvl  37242  hlhil0  37247  hlhillsm  37248  elrfi  37257  elrfirn2  37259  istopclsd  37263  mzpcompact2lem  37314  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  diophin  37336  diophun  37337  rexrabdioph  37358  eldioph4b  37375  diophren  37377  pell1qr1  37435  reglog1  37460  rmspecfund  37474  jm2.17a  37527  jm2.17b  37528  jm2.27c  37574  fnwe2lem2  37621  kelac2  37635  lnmlsslnm  37651  lmhmlnmsplit  37657  pwssplit4  37659  pwslnmlem2  37663  lnrfg  37689  hbtlem1  37693  hbtlem7  37695  mendbas  37754  mendplusgfval  37755  mendmulrfval  37757  mendvscafval  37760  acsfn1p  37769  cntzsdrg  37772  proot1hash  37778  arearect  37801  areaquad  37802  conrel1d  37955  iunrelexp0  37994  relexpaddss  38010  trclfvdecomr  38020  rntrclfvRP  38023  dfrtrcl4  38030  frege131d  38056  rfovfvd  38296  rfovfvfvd  38297  rfovcnvf1od  38298  fsovfvd  38304  fsovfvfvd  38305  fsovfd  38306  fsovcnvlem  38307  dssmapfvd  38311  dssmapfv2d  38312  dssmapfv3d  38313  ntrclscls00  38364  clsneicnv  38403  neicvgnvo  38413  ntrf  38421  dssmapntrcls  38426  k0004val0  38452  radcnvrat  38513  hashnzfz2  38520  dvsid  38530  expgrowthi  38532  expgrowth  38534  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  compneOLD  38644  isosctrlem1ALT  39170  sumsnd  39185  inabs3  39224  fzisoeu  39514  upbdrech2  39522  fmul01  39812  expcnfg  39823  limcresiooub  39874  limcresioolb  39875  sublimc  39884  divlimc  39888  supcnvlimsupmpt  39973  cncfshiftioo  40105  cncfiooicc  40107  dvmptresicc  40134  dvdivbd  40138  dvbdfbdioolem2  40144  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem2  40162  itgsin0pilem1  40165  ditgeq3d  40180  itgioocnicc  40193  itgiccshift  40196  itgperiod  40197  stoweidlem17  40234  stoweidlem21  40238  stoweidlem27  40244  stoweidlem32  40249  stoweidlem36  40253  stoweidlem40  40257  stoweidlem47  40264  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem3  40322  dirkercncflem4  40323  fourierdlem32  40356  fourierdlem33  40357  fourierdlem60  40383  fourierdlem61  40384  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem87  40410  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem96  40419  fourierdlem99  40422  fourierdlem101  40424  fourierdlem107  40430  fourierdlem112  40435  fourierdlem113  40436  fourierdlem115  40438  fourierswlem  40447  fouriercn  40449  etransclem2  40453  etransclem5  40456  etransclem6  40457  etransclem11  40462  etransclem14  40465  etransclem17  40468  etransclem46  40497  etransclem47  40498  caragenel  40709  ovnsubadd  40786  afvfundmfveq  41218  afvnfundmuv  41219  rlimdmafv  41257  aovnfundmuv  41262  ndmaov  41263  nfunsnaov  41266  aovprc  41268  m1mod0mod1  41339  setsidel  41346  setsnidel  41347  iccelpart  41369  fargshiftfo  41378  pfx00  41384  pfx0  41385  pfxccatpfx2  41428  pwdif  41501  m1expevenALTV  41560  bits0ALTV  41590  upgrwlkupwlk  41721  subsubmgm  41797  c0rhm  41912  c0rnghm  41913  rngcvalALTV  41961  rngcval  41962  rngchomfval  41966  rngcid  41979  rngchomfvalALTV  41984  rngcidALTV  41991  rngcifuestrc  41997  ringcvalALTV  42007  ringcval  42008  ringchomfval  42012  ringcid  42025  ringchomfvalALTV  42047  ringcidALTV  42054  rhmsubclem4  42089  xpprsng  42110  fdmdifeqresdif  42120  ply1vr1smo  42169  ply1sclrmsm  42171  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  lineval  42182  dmatALTval  42189  dmatALTbas  42190  lincvalsn  42206  lincvalpr  42207  lincsum  42218  lmod1lem2  42277  lmod1lem3  42278  lmod1zr  42282  zlmodzxznm  42286  zlmodzxzldeplem4  42292  aacllem  42547