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

Theorem sylibr 224
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
sylibr.1 (𝜑𝜓)
sylibr.2 (𝜒𝜓)
Assertion
Ref Expression
sylibr (𝜑𝜒)

Proof of Theorem sylibr
StepHypRef Expression
1 sylibr.1 . 2 (𝜑𝜓)
2 sylibr.2 . . 3 (𝜒𝜓)
32biimpri 218 . 2 (𝜓𝜒)
41, 3syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  sylbbr  226  pm5.74rd  263  3imtr4i  281  con2bid  343  sylanbrc  572  oplem1  1043  anifp  1057  3jca  1122  3mix1  1414  3mix2  1415  syl3anbrc  1428  xornan2  1621  inegd  1651  cad11  1706  nfd  1864  nftht  1866  nfntht  1867  nfntht2  1868  nfxfrd  1930  nfxfrdOLD  1990  nfdvOLD  2042  19.39  2068  19.24  2069  19.34  2070  equvelvOLD  2119  hbim1  2289  nfdOLD  2355  hbim1OLD  2389  nfan1OLD  2398  nfeqf2OLD  2453  exmo  2643  eumo  2647  mo3  2656  2exeu  2698  2eu6  2707  eqrdv  2769  abbi2dv  2891  nfcd  2908  nfcxfrd  2912  neqned  2950  necon3ai  2968  3netr4g  3022  neneor  3042  alral  3077  hbralrimi  3103  rgen2a  3126  rspe  3151  r19.27v  3218  r19.29imd  3222  mormo  3307  nrexrmo  3312  cgsex2g  3391  cgsex4g  3392  spc2egv  3446  spc3egv  3448  rspce  3455  elrabd  3517  mo2icl  3537  reu3  3548  reu6i  3549  sbc5  3612  rspesbca  3669  rmo2i  3676  ssrd  3757  ssrdv  3758  eqrd  3771  3sstr4g  3795  syl5eqss  3798  ss2abdv  3824  abssdv  3825  rabssdv  3831  ss2rabdv  3832  ssun1  3927  unssad  3941  unssbd  3942  uneqin  4027  reuss2  4055  euelss  4062  reximdva0  4080  eqeuel  4088  sbcne12  4130  sbnfc2  4151  uneqdifeq  4199  falseral0  4220  elpwunsn  4362  disjsn2  4384  absneu  4399  rabsneu  4400  tppreqb  4471  opthprneg  4531  elunii  4579  uniss2  4606  unidif  4607  ssunieq  4608  pwuni  4610  intab  4641  eliuni  4660  iunss2  4699  iunxdif2  4702  riinrab  4730  invdisj  4772  disjiun  4774  disjord  4775  disjiund  4777  disjxiun  4783  3brtr4g  4820  trin  4896  triun  4899  truni  4900  trint  4901  axnulALT  4921  iinexg  4955  class2seteq  4964  notzfaus  4971  eusvnf  4992  eusvnfb  4993  eusv2nf  4995  ralxfr2d  5010  rabxfrd  5017  reuhypd  5023  snelpwi  5040  copsex2t  5084  euotd  5106  opthwiener  5107  otsndisj  5112  otiunsndisj  5113  ispod  5178  sotric  5196  isso2i  5202  somo  5204  exse  5213  frc  5215  fr2nr  5227  epfrc  5235  otel3xp  5293  0nelrel  5302  eqrelrdv  5356  xpsspw  5372  relint  5381  relopabi  5384  relop  5411  eqbrrdva  5430  ssrelrn  5453  opeldm  5466  elres  5576  relssres  5578  restidsingOLD  5600  issref  5650  trin2  5660  dminss  5688  imainss  5689  xpnz  5694  xpdifid  5703  dmmptg  5776  relrelss  5803  cnviin  5816  elpredim  5835  trssord  5883  ordelord  5888  ordtri1  5899  orddisj  5905  suctr  5951  suctrOLD  5952  funmo  6047  funco  6071  funun  6075  fununmo  6076  fununfun  6077  funprg  6083  funtpg  6084  funtp  6086  fntpg  6089  funcnvpr  6091  funcnvtp  6092  funcnvqp  6093  fununi  6104  funimaexg  6115  isarep2  6118  fnunsn  6138  2elresin  6142  fnimadisj  6152  dmmptd  6164  fco  6198  funssxp  6201  fssres  6210  feu  6220  fimacnvdisj  6223  f00  6227  f0rn0  6230  f1co  6251  fores  6265  foco  6266  foconst  6267  f1ores  6292  foimacnv  6295  f1oun  6297  f1oco  6300  fo00  6313  brprcneu  6325  fv3  6347  eliman0  6364  nfunsn  6366  dffv2  6413  funfvbrb  6473  respreima  6487  iinpreima  6488  fvn0ssdmfun  6493  fvelrn  6495  dff2  6514  dff3  6515  dffo4  6518  exfo  6520  mptex2  6526  frnssb  6533  ffvresb  6536  f1oresrab  6537  fsn  6545  fpr  6564  ftpg  6566  fmptsnd  6579  fsnunf  6595  fsnunfv  6597  tpres  6610  elabrex  6644  fpropnf1  6667  dff1o6  6674  foeqcnvco  6698  fveqf1o  6700  fliftel1  6703  isof1oopb  6718  soisoi  6721  isocnv3  6725  isores1  6727  isoini2  6732  knatar  6750  riotasbc  6769  fvmptopab  6844  brfvopab  6847  oprabv  6850  eloprabga  6894  fnoprabg  6908  ndmovass  6969  ndmovdistr  6970  elovmpt3rab1  7040  ofmpteq  7063  sorpssi  7090  sorpssuni  7093  sorpssint  7094  sorpsscmpl  7095  snnex  7113  pwnex  7115  eldifpw  7123  elpwun  7124  iunpw  7125  fr3nr  7126  ordon  7129  ssorduni  7132  onint0  7143  onminex  7154  suceloni  7160  ordsucss  7165  ordsucelsuc  7169  ordsucuniel  7171  nlimsucg  7189  ordunisuc2  7191  ordzsl  7192  tfi  7200  peano5  7236  exse2  7252  soex  7256  funcnvuni  7266  fabexg  7269  fun11iun  7273  zfrep6  7281  wemoiso  7300  wemoiso2  7301  oprabexd  7302  fo1stres  7341  fo2ndres  7342  unielxp  7353  1st2ndbr  7366  opabn1stprc  7377  fmpt2co  7411  1stconst  7416  2ndconst  7417  curry1  7420  cnvf1olem  7426  frxp  7438  poxp  7440  soxp  7441  fnse  7445  suppsnop  7460  ressuppssdif  7467  mpt2xopxnop0  7493  reldmtpos  7512  tposfun  7520  dftpos4  7523  undefnel  7556  wfrlem5  7572  wfrlem13  7580  wfrlem17  7584  onfununi  7591  onnseq  7594  smores  7602  smores2  7604  smogt  7617  dfrecs3  7622  tfrlem1  7625  tfrlem9a  7635  tfrlem10  7636  tfr3  7648  tz7.48lem  7689  tz7.48-1  7691  tz7.49  7693  tz7.49c  7694  seqomlem2  7699  seqomlem4  7701  2oconcl  7737  oawordeulem  7788  oalimcl  7794  oacomf1o  7799  omlimcl  7812  omeulem1  7816  oelim2  7829  oeeulem  7835  oaabslem  7877  oaabs2  7879  omabslem  7880  omabs  7881  brdifun  7925  swoso  7929  ecelqsdm  7969  iiner  7971  qsdisj2  7977  eroveu  7995  erovlem  7996  ecopovtrn  8003  pmsspw  8044  map0b  8049  mapsnd  8051  mapsncnv  8058  ixpf  8084  uniixp  8085  ixpexg  8086  resixp  8097  relsdom  8116  f1oen3g  8125  ssdomg  8155  domtr  8162  domdifsn  8199  omxpenlem  8217  omf1o  8219  sbthlem2  8227  sbthlem3  8228  sbthlem7  8232  sbthlem8  8233  2pwuninel  8271  domss2  8275  xpf1o  8278  xpmapenlem  8283  limenpsi  8291  infensuc  8294  php3  8302  1sdom  8319  ominf  8328  isinf  8329  fineqvlem  8330  pssnn  8334  ssnnfi  8335  ssfi  8336  xpfir  8338  dif1en  8349  findcard  8355  findcard2  8356  findcard3  8359  ac6sfi  8360  frfi  8361  unblem1  8368  unblem2  8369  nnsdomg  8375  unfi  8383  domunfican  8389  fodomfi  8395  unifi2  8412  pwfilem  8416  fissuni  8427  fipreima  8428  finsschain  8429  indexfi  8430  funsnfsupp  8455  fival  8474  fiin  8484  dffi2  8485  fisn  8489  dffi3  8493  marypha1lem  8495  supmo  8514  suppr  8533  infmo  8557  infpr  8565  ordtypelem2  8580  ordtypelem3  8581  ordtypelem9  8587  hartogslem1  8603  wemapsolem  8611  wemapso2lem  8613  wemapso2  8614  card2inf  8616  wdom2d  8641  wdomd  8642  xpwdomg  8646  ixpiunwdom  8652  elnel  8670  inf3lem3  8691  inf3lem6  8694  infdifsn  8718  cantnflt  8733  cantnff  8735  cantnfp1lem3  8741  cantnflem1b  8747  cantnflem1  8750  cantnf  8754  wemapwe  8758  oef1o  8759  cnfcom2lem  8762  cnfcom2  8763  cnfcom3lem  8764  cnfcom3  8765  trcl  8768  setind  8774  tcmin  8781  r1ordg  8805  r1pwss  8811  r1val1  8813  tz9.12lem1  8814  tz9.12lem3  8816  tz9.13  8818  r1elwf  8823  rankdmr1  8828  pwwf  8834  unwf  8837  uniwf  8846  rankr1c  8848  rankpwi  8850  rankval3b  8853  rankonidlem  8855  r1pwALT  8873  r1pwcl  8874  rankuni2b  8880  rankxplim3  8908  rankxpsuc  8909  tcwf  8910  tcrank  8911  scottex  8912  scott0  8913  hta  8924  djuss  8946  djuunxp  8947  djuun  8952  updjud  8960  cardf2  8969  isnumi  8972  tskwe  8976  cardid2  8979  carden2b  8993  cardsn  8995  cardprclem  9005  harval2  9023  dif1card  9033  r0weon  9035  infxpenlem  9036  infxpenc  9041  dfac8clem  9055  ac5num  9059  ondomen  9060  acni2  9069  finacn  9073  acndom2  9077  infpwfien  9085  alephnbtwn  9094  alephsucdom  9102  infenaleph  9114  dfac5lem4  9149  dfac5  9151  dfac2a  9152  dfac2b  9153  dfac2OLD  9155  dfac9  9160  dfacacn  9165  dfac13  9166  dfac12lem2  9168  kmlem4  9177  kmlem6  9179  kmlem8  9181  kmlem13  9186  cda1en  9199  cdainflem  9215  pwsdompw  9228  infdif  9233  infmap2  9242  ackbij1lem18  9261  cff  9272  cflm  9274  cardcf  9276  cfsuc  9281  cff1  9282  cfflb  9283  cflim3  9286  cflim2  9287  cfss  9289  cfslb  9290  cofsmo  9293  cfsmolem  9294  coftr  9297  fin23lem7  9340  enfin2i  9345  fin23lem26  9349  fin23lem30  9366  fin23lem32  9368  fin23lem38  9373  fin23lem40  9375  fin23lem41  9376  isf32lem2  9378  isf32lem3  9379  compsscnvlem  9394  compssiso  9398  isf34lem5  9402  isf34lem7  9403  isf34lem6  9404  isfin1-2  9409  isfin1-3  9410  fin56  9417  fin1a2lem11  9434  fin1a2lem13  9436  fin1a2s  9438  hsmexlem2  9451  domtriomlem  9466  dcomex  9471  axdc2lem  9472  axdc3lem  9474  axdc3lem2  9475  axdc3lem4  9477  axdc4lem  9479  axcclem  9481  ac6c4  9505  zorn2lem6  9525  zorn2lem7  9526  zorng  9528  ttukeylem1  9533  ttukeylem6  9538  ttukeylem7  9539  axdclem  9543  brdom3  9552  brdom5  9553  brdom4  9554  iunfo  9563  iundom2g  9564  entric  9581  entri2  9582  ondomon  9587  ficard  9589  konigthlem  9592  alephval2  9596  pwcfsdom  9607  fpwwe2lem1  9655  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  fpwwe  9670  canthnumlem  9672  canthwelem  9674  canthwe  9675  canthp1lem2  9677  pwfseqlem1  9682  pwfseqlem3  9684  pwfseqlem4a  9685  pwfseqlem4  9686  pwfseqlem5  9687  hargch  9697  alephgch  9698  gch2  9699  gch3  9700  gchac  9705  wunfi  9745  intwun  9759  wunex2  9762  wuncval  9766  wunccl  9768  wuncval2  9771  tsksuc  9786  tskwe2  9797  inttsk  9798  inar1  9799  tskuni  9807  ingru  9839  gruina  9842  grur1a  9843  axgroth3  9855  inaprc  9860  tskmcl  9865  nqerf  9954  recmulnq  9988  dmrecnq  9992  genpn0  10027  genpnnp  10029  genpcl  10032  nqpr  10038  psslinpr  10055  prlem934  10057  ltexprlem1  10060  ltexprlem4  10063  ltexprlem5  10064  ltexprlem7  10066  reclem2pr  10072  reclem3pr  10073  suplem1pr  10076  supexpr  10078  addsrmo  10096  mulsrmo  10097  supsrlem  10134  supsr  10135  axaddrcl  10175  axmulrcl  10177  axrnegex  10185  axcnre  10187  axpre-lttrn  10189  wuncn  10193  dedekind  10402  cnegex  10419  relin01  10754  recextlem2  10860  mulnzcnopr  10875  divmulasscom  10911  rereccl  10945  lbreu  11175  supaddc  11192  supadd  11193  supmul1  11194  supmullem2  11196  supmul  11197  infrenegsup  11208  nnm1nn0  11536  elnnnn0c  11540  nn0n0n1ge2  11560  elnnz1  11605  zaddcl  11619  nzadd  11627  uzind  11671  eluzge3nn  11932  eluz2b2  11964  zsupss  11980  nn01to3  11984  uzwo3  11986  zmin  11987  znq  11995  qaddcl  12007  qmulcl  12009  qreccl  12011  irradd  12015  irrmul  12016  rpnnen1lem2  12017  rpnnen1lem1  12018  rpnnen1lem3  12019  rpnnen1lem5  12021  rpnnen1lem1OLD  12024  rpnnen1lem3OLD  12025  rpnnen1lem5OLD  12027  cnref1o  12030  rpcndif0  12054  qbtwnxr  12236  xrinfmss2  12346  elioo4g  12439  difreicc  12511  fzpreddisj  12597  fz0to4untppr  12650  elfz0ubfz0  12651  elfz0fzfz0  12652  fz0fzelfz0  12653  fz0fzdiffz0  12656  elfzmlbp  12658  difelfzle  12660  4fvwrd4  12667  fzosplit  12709  prinfzo0  12715  elfzo0  12717  nn0p1elfzo  12719  elfzonn0  12721  fzofzim  12723  elfzo1  12726  fzo1fzo0n0  12727  elfzom1elp1fzo  12743  fzossfzop1  12754  ssfzo12bi  12771  elfzonelfzo  12778  elfznelfzob  12782  1mod  12910  modfzo0difsn  12950  fzennn  12975  fseqsupcl  12984  fsuppmapnn0fiublem  12997  fsuppmapnn0fiub  12998  mptnn0fsupp  13004  seqf2  13027  seqf1olem1  13047  seqid3  13052  seqz  13056  ser0f  13061  seqof  13065  expcl2lem  13079  1exp  13096  hashkf  13323  hashv01gt1  13337  hashsng  13361  hashdifpr  13405  hashmap  13424  hashbclem  13438  hashbc  13439  hashf1lem1  13441  hashf1lem2  13442  ishashinf  13449  prprrab  13457  pr2pwpr  13463  hashge2el2dif  13464  brfi1uzind  13482  opfi1uzind  13485  iswrdi  13505  snopiswrd  13510  iswrdsymb  13518  wrdsymb1  13539  ccatfv0  13565  ccatval21sw  13567  lswccatn0lsw  13573  eqs1  13592  ccat1st1st  13611  ccat2s1p1  13612  lswccats1fst  13620  ccat2s1fvw  13623  swrdfv0  13633  swrdnd  13641  swrd0fv0  13649  swrdtrcfv0  13651  swrdlen2  13654  swrdfv2  13655  swrdsbslen  13657  swrdspsleq  13658  swrdswrdlem  13668  cats1un  13684  swrdccatin12lem2a  13694  swrdccatin12lem2  13698  swrdccatin12lem3  13699  swrdccat  13702  repswswrd  13740  cshwidx0mod  13760  cshf1  13765  scshwfzeqfzo  13781  s3fn  13865  f1oun2prg  13871  s4f1o  13872  ccat2s1fvwALT  13908  wwlktovfo  13911  s3sndisj  13916  s3iunsndisj  13917  coemptyd  13928  trclfvcotr  13958  reltrclfv  13966  rtrclreclem3  14008  rtrclreclem4  14009  dfrtrcl2  14010  relexpindlem  14011  shftfval  14018  rennim  14187  cnpart  14188  sqrmo  14200  sqrtneglem  14215  rexanuz  14293  sqreulem  14307  eqsqrtd  14315  limsupgord  14411  limsupval2  14419  limsupgre  14420  rlimi  14452  climeu  14494  lo1res  14498  rlimmptrcl  14546  o1of2  14551  o1rlimmul  14557  lo1mptrcl  14560  o1mptrcl  14561  isercolllem3  14605  isercoll2  14607  caucvgrlem  14611  summolem3  14653  summo  14656  fsumss  14664  fsumsplit  14679  sumsnf  14681  fsumsplitsn  14682  sumsn  14683  sumtp  14686  sumsplit  14707  fsum2dlem  14709  fsum0diag2  14722  fsum00  14737  fsumabs  14740  fsumrlim  14750  fsumo1  14751  o1fsum  14752  fsumiun  14760  incexclem  14775  isumsup2  14785  isumltss  14787  infcvgaux2i  14797  mertenslem1  14823  mertenslem2  14824  prodf1f  14831  prodmolem3  14870  prodmo  14873  fprodss  14885  fprodser  14886  prodsn  14899  prodsnf  14901  fprodm1  14904  fprod2dlem  14917  fprodsplitsn  14926  iprodmul  14940  bpolylem  14985  ef0lem  15015  efcvgfsum  15022  tanval  15064  rpnnen2lem11  15159  rpnnen2lem12  15160  ruclem6  15170  modmulconst  15222  dvdslelem  15240  dvdsdivcl  15247  dvdsssfz1  15249  dvdsfac  15257  fprodfvdvdsd  15266  nn0ehalf  15303  nn0oddm1d2  15309  nnoddm1d2  15310  sumodd  15319  divalglem8  15331  bitsfzolem  15364  bitsinv1  15372  bitsinvp1  15379  sadfval  15382  sadcf  15383  smufval  15407  smupf  15408  smuval2  15412  smupvallem  15413  smu01lem  15415  smumullem  15422  gcdcllem3  15431  gcdaddmlem  15453  bezoutlem2  15465  dfgcd2  15471  algrf  15494  algcvgblem  15498  lcmcllem  15517  lcmgcdlem  15527  absproddvds  15538  fissn0dvdsn0  15541  lcmfnncl  15550  lcmfledvds  15553  lcmftp  15557  lcmfunsnlem1  15558  lcmfunsnlem2lem1  15559  lcmfunsnlem2lem2  15560  lcmfunsnlem2  15561  coprmgcdb  15570  ncoprmgcdne1b  15571  qredeu  15579  cncongr1  15588  cncongr2  15589  isprm2lem  15601  dvdsnprmd  15610  oddprmge3  15619  ncoprmlnprm  15643  phicl2  15680  phibndlem  15682  phibnd  15683  dfphi2  15686  hashdvds  15687  phiprmpw  15688  phimullem  15691  hashgcdeq  15701  phisum  15702  odzcllem  15704  odzdvds  15707  reumodprminv  15716  nnnn0modprm0  15718  pcdvdsb  15780  difsqpwdvds  15798  oddprmdvds  15814  infpn2  15824  prmreclem1  15827  prmreclem2  15828  prmreclem3  15829  prmreclem4  15830  prmreclem5  15831  prmreclem6  15832  1arith  15838  4sqlem3  15861  4sqlem11  15866  4sqlem19  15874  vdwapf  15883  vdwlem6  15897  vdwlem8  15899  vdwlem9  15900  vdwlem13  15904  vdwnn  15909  ramtlecl  15911  0ram  15931  ram0  15933  ramub1lem1  15937  ramub1lem2  15938  ramub1  15939  prmdvdsprmo  15953  prmgaplem4  15965  cshwshashlem1  16009  cshwsdisj  16012  cshws0  16015  cshwrepswhash1  16016  setsfun0  16101  setscom  16110  setsid  16121  basprssdmsets  16132  restsspw  16300  prdshom  16335  imasaddfnlem  16396  imasaddvallem  16397  imasaddflem  16398  imasvscafn  16405  imasvscaf  16407  xpscfn  16427  xpsc0  16428  xpsc1  16429  mremre  16472  mrcuni  16489  submrc  16496  mreexexlem2d  16513  mreexexlem3d  16514  isacs2  16521  isacs1i  16525  mreacs  16526  acsfn  16527  catideu  16543  isssc  16687  isfuncd  16732  funcoppc  16742  idfucl  16748  cofucl  16755  funcres2b  16764  wunfunc  16766  fthoppc  16790  idffth  16800  ressffth  16805  natixp  16819  nati  16822  fuccocl  16831  fucidcl  16832  invfuc  16841  homaf  16887  coapm  16928  setcepi  16945  catciso  16964  funcestrcsetclem9  16996  evlfcl  17070  curf2cl  17079  uncfcurf  17087  yonedalem4c  17125  yonedalem3b  17127  yonedalem3  17128  yonedainv  17129  drsdirfi  17146  isposd  17163  lubval  17192  glbval  17205  clatl  17324  odupos  17343  poslubmo  17354  posglbmo  17355  ipoval  17362  ipolerval  17364  isacs4lem  17376  isacs5lem  17377  isacs4  17381  isacs3  17382  acsfiindd  17385  acsmapd  17386  mrelatglb  17392  mrelatlub  17394  mgmidsssn0  17477  isnsgrp  17496  isnmnd  17506  mndpfo  17522  mhmeql  17572  gsumws1  17584  gsumwspan  17591  grpinveu  17664  prdsinvlem  17732  mhmfmhm  17746  subgint  17826  0subg  17827  cycsubg  17830  subgacs  17837  nsgacs  17838  0nsg  17847  eqgfval  17850  ghmeql  17891  gimco  17918  brgici  17920  gass  17941  oppgsubm  17999  oppgsubg  18000  symgval  18006  symg2bas  18025  cayley  18041  symgextf  18044  f1omvdco3  18076  pmtrrn2  18087  symggen2  18098  pmtr3ncomlem1  18100  psgnunilem5  18121  psgnfvalfi  18140  odcl  18162  dfod2  18188  odf1o2  18195  gexcl  18202  gex1  18213  pgpfi1  18217  sylow1lem2  18221  sylow1lem3  18222  odcau  18226  pgpssslw  18236  sylow2alem2  18240  sylow2a  18241  sylow2blem1  18242  sylow2blem3  18244  sylow3lem3  18251  sylow3lem6  18254  pj1fval  18314  efgrcl  18335  efgval  18337  efgi  18339  efgi2  18345  efgsval2  18353  efgs1  18355  efgs1b  18356  efgsp1  18357  efgsres  18358  efgsfo  18359  efgredlemd  18364  efgredlem  18367  efgrelexlemb  18370  0frgp  18399  iscmnd  18412  gexex  18463  frgpnabllem1  18483  iscygodd  18497  prmcyg  18502  lt6abl  18503  gsumval3eu  18512  gsumval3  18515  gsumzaddlem  18528  gsumzsplit  18534  gsummhm2  18546  gsumzunsnd  18562  gsumunsnfd  18563  gsumpt  18568  gsum2dlem2  18577  gsumcom2  18581  eldprd  18611  dprdfadd  18627  dprdspan  18634  dprdres  18635  dprdcntz2  18645  dprd2dlem2  18647  dprd2dlem1  18648  dprd2da  18649  dprd2d2  18651  dmdprdsplit2lem  18652  dpjfval  18662  ablfacrplem  18672  ablfacrp  18673  ablfacrp2  18674  ablfac1b  18677  ablfac1eulem  18679  ablfac1eu  18680  pgpfac1lem5  18686  pgpfaclem1  18688  ablfaclem2  18693  ablfaclem3  18694  ablfac2  18696  srgfcl  18723  srgbinomlem4  18751  ring1  18810  pws1  18824  opprringb  18840  irredn0  18911  rim0to0  18952  kerf1hrm  18953  isdrngd  18982  isdrngrd  18983  opprsubrg  19011  subrgint  19012  subrgmre  19014  issubdrg  19015  issrngd  19071  lsssn0  19158  lss1d  19176  lssintcl  19177  lssmre  19179  lspf  19187  lspval  19188  lspextmo  19269  brlmici  19282  lsppratlem1  19362  lsppratlem6  19367  lbsextlem1  19373  lbsextlem2  19374  lbsextlem3  19375  lbsextlem4  19376  sraval  19391  rsp1  19439  drngnidl  19444  rng1nnzr  19489  rng1nfld  19493  abvn0b  19517  fidomndrng  19522  aspval  19543  asplss  19544  aspid  19545  aspsubrg  19546  psrbagconcl  19588  psrbagconf1o  19589  psrass1lem  19592  psraddcl  19598  psrmulcllem  19602  psrvscacl  19608  psr0cl  19609  psrnegcl  19611  psr1cl  19617  subrgpsr  19634  mvrf  19639  mplmon  19678  mplcoe1  19680  mplcoe5  19683  opsrtoslem2  19700  subrgasclcl  19714  evlseu  19731  mpfrcl  19733  mpfind  19751  coe1fval3  19793  coe1z  19848  coe1mul2  19854  coe1tm  19858  cply1mul  19879  ply1coe  19881  evl1sca  19913  pf1rcl  19928  pf1ind  19934  prmirredlem  20056  mulgrhm2  20062  zlmlmod  20086  zlmassa  20087  znf1o  20115  znfi  20123  znidomb  20125  psgnghm  20141  psgnghm2  20142  psgndiflemB  20162  redvr  20180  ipcl  20195  cssmre  20254  obselocv  20289  dsmmfi  20299  dsmm0cl  20301  frlmfibas  20322  frlmgsum  20328  uvcresum  20349  frlmlbs  20353  uvcendim  20403  mat0dimcrng  20494  mat1dimscm  20499  mat1ric  20511  scmatscm  20537  scmatf1  20555  scmatghm  20557  scmatmhm  20558  scmatric  20561  1mavmul  20572  mavmul0  20576  ma1repvcl  20594  mdetunilem9  20644  maducoeval2  20664  gsummatr01lem4  20683  cpmatacl  20741  cpmatmcl  20744  mat2pmatf1  20754  mat2pmatghm  20755  mat2pmatmul  20756  mat2pmatlin  20760  mat2pmatscmxcl  20765  m2pmfzgsumcl  20773  m2cpminvid2lem  20779  matcpmric  20784  decpmatmulsumfsupp  20798  pmatcollpw2lem  20802  monmatcollpw  20804  pmatcollpw3fi1lem1  20811  pmatcollpwscmatlem1  20814  pmatcollpwscmatlem2  20815  mp2pm2mplem4  20834  pm2mpghm  20841  pm2mpmhmlem1  20843  pm2mpmhmlem2  20844  pmmpric  20848  monmat2matmon  20849  chfacfisf  20879  chfacfisfcpmat  20880  chcoeffeqlem  20910  istopon  20937  toponcom  20953  topgele  20955  topontopn  20965  tsettps  20966  tgval  20980  eltg2b  20984  unitg  20992  en2top  21010  tgss2  21012  bastop2  21019  distop  21020  fctop  21029  cctop  21031  ppttop  21032  pptbas  21033  epttop  21034  cldss2  21055  clscld  21072  elcls  21098  mretopd  21117  toponmre  21118  neisspw  21132  neips  21138  neiuni  21147  neiptopnei  21157  clslp  21173  restbas  21183  resstps  21212  ordtbaslem  21213  ordtbas2  21216  ordtbas  21217  ordttopon  21218  ordtopn1  21219  ordtopn2  21220  ordtrest2  21229  iocpnfordt  21240  icomnfordt  21241  lecldbas  21244  tgcn  21277  tgcnp  21278  subbascn  21279  iscnp4  21288  cnntr  21300  lmff  21326  t0dist  21350  pnrmopn  21368  lpcls  21389  t1sep  21395  dishaus  21407  ordthauslem  21408  cmpcovf  21415  discmp  21422  cmpsublem  21423  cmpsub  21424  fiuncmp  21428  hauscmplem  21430  cmpfi  21432  cnconn  21446  connsubclo  21448  iunconn  21452  clsconn  21454  conncompid  21455  1stcfb  21469  2ndci  21472  2ndcsb  21473  2ndc1stc  21475  1stcrest  21477  2ndcctbss  21479  2ndcdisj  21480  2ndcomap  21482  2ndcsep  21483  dis2ndc  21484  nlly2i  21500  llynlly  21501  restnlly  21506  llyrest  21509  llyidm  21512  nllyidm  21513  hausllycmp  21518  cldllycmp  21519  lly1stc  21520  dislly  21521  isref  21533  islocfin  21541  lfinun  21549  comppfsc  21556  llycmpkgen2  21574  1stckgenlem  21577  kgencn2  21581  txuni2  21589  txbasex  21590  txbas  21591  elptr  21597  elptr2  21598  ptbasin2  21602  ptbasfi  21605  xkoopn  21613  xkouni  21623  ptpjopn  21636  ptclsg  21639  dfac14  21642  xkoccn  21643  txcnp  21644  ptcnplem  21645  ptcnp  21646  txcnmpt  21648  txcn  21650  ptcn  21651  prdstopn  21652  txdis  21656  txindis  21658  txdis1cn  21659  txlly  21660  txnlly  21661  pthaus  21662  ptrescn  21663  txtube  21664  txcmplem1  21665  txcmplem2  21666  tx1stc  21674  xkohaus  21677  xkococnlem  21683  xkococn  21684  cnmpt11  21687  cnmpt1t  21689  cnmpt12  21691  cnmpt21  21695  cnmpt2t  21697  cnmpt22  21698  cnmptkp  21704  cnmptk1  21705  cnmpt1k  21706  cnmptkk  21707  cnmptk1p  21709  cnmptk2  21710  cnmpt2k  21712  txconn  21713  qtoptop2  21723  qtopuni  21726  basqtop  21735  tgqtop  21736  qtopeu  21740  imastps  21745  kqdisj  21756  kqcldsat  21757  kqt0  21770  kqreg  21775  kqnrm  21776  hmeofval  21782  hmphi  21801  hmphdis  21820  ordthmeolem  21825  xpstopnlem1  21833  ptcmpfi  21837  reghaus  21849  fbssfi  21861  fbssint  21862  opnfbas  21866  trfbas2  21867  isfil2  21880  snfil  21888  fsubbas  21891  fgcl  21902  neifil  21904  fbasrn  21908  filuni  21909  supfil  21919  uzrest  21921  uzfbas  21922  isufil2  21932  filssufilg  21935  numufl  21939  fixufil  21946  uffixsn  21949  rnelfmlem  21976  hausflimi  22004  flimsncls  22010  hauspwpwf1  22011  flftg  22020  txflf  22030  fclscmp  22054  alexsublem  22068  alexsub  22069  alexsubb  22070  alexsubALTlem2  22072  alexsubALTlem3  22073  alexsubALTlem4  22074  ptcmplem3  22078  ptcmplem4  22079  cnextfun  22088  cnextf  22090  cnextcn  22091  cnextfres  22093  cnmpt1plusg  22111  cnmpt2plusg  22112  tmdgsum  22119  oppgtmd  22121  distgp  22123  indistgp  22124  symgtgp  22125  clssubg  22132  clsnsg  22133  cldsubg  22134  tgpconncompeqg  22135  tgpconncomp  22136  ghmcnp  22138  qustgplem  22144  tsmsfbas  22151  tsmsid  22163  tsmsf1o  22168  tgptsmscls  22173  tsmssplit  22175  tsmsxp  22178  cnmpt1vsca  22217  cnmpt2vsca  22218  ustrel  22235  ustfilxp  22236  ust0  22243  elrnust  22248  ustuni  22250  trust  22253  ustuqtop0  22264  ustuqtop3  22267  utop2nei  22274  utop3cls  22275  utopreg  22276  ussid  22284  tustps  22297  neipcfilu  22320  prdsxmetlem  22393  imasdsf1olem  22398  blbas  22455  setsmstopn  22503  prdsbl  22516  blsscls2  22529  met1stc  22546  met2ndci  22547  prdsxmslem2  22554  metuval  22574  metustrel  22577  metustexhalf  22581  metustfbas  22582  restmetu  22595  tngtopn  22674  nrgtrg  22714  tgqioo  22823  zdis  22839  iccntr  22844  icccmplem1  22845  icccmplem2  22846  reconnlem1  22849  cnmpt1ds  22865  cnmpt2ds  22866  metdsf  22871  metnrmlem3  22884  fsumcn  22893  cncfmpt1f  22936  cncfmpt2ss  22938  cnmpt2pc  22947  icoopnst  22958  iocopnst  22959  cnllycmp  22975  evth  22978  lebnumlem1  22980  copco  23037  pcoass  23043  pi1xfrcnv  23076  zlmclm  23131  cnmpt1ip  23265  cnmpt2ip  23266  cfilres  23313  cfilucfil4  23337  bcthlem5  23344  bcth  23345  minveclem1  23414  minveclem2  23416  minveclem3b  23418  minveclem4a  23420  pmltpc  23438  evthicc2  23448  ovolficcss  23457  ovolfsf  23459  ovolsf  23460  elovolmr  23464  ovolgelb  23468  ovolunlem1  23485  ovolfiniun  23489  ovoliunlem1  23490  ovoliunlem2  23491  ovoliun  23493  ovoliun2  23494  ovoliunnul  23495  ovolshftlem2  23498  ovolicc2lem4  23508  ovolicc2  23510  volfiniun  23535  iundisj  23536  voliunlem1  23538  voliunlem2  23539  voliunlem3  23540  volsup  23544  ovolioo  23556  uniioombllem3a  23572  uniioombllem3  23573  uniioombllem6  23576  dyadmax  23586  dyadmbllem  23587  dyadmbl  23588  opnmbllem  23589  volsup2  23593  vitalilem3  23598  vitalilem4  23599  vitalilem5  23600  vitali  23601  mbfconstlem  23615  mbfmptcl  23624  mbfposr  23639  ismbf3d  23641  mbfinf  23652  mbflimsup  23653  mbflim  23655  i1fima2  23666  i1fd  23668  itg1val2  23671  i1fadd  23682  i1fmul  23683  itg1addlem4  23686  i1fmulc  23690  i1fposd  23694  itg1climres  23701  itg2lr  23717  itg2seq  23729  itg2mulc  23734  itg2splitlem  23735  itg2split  23736  itg2monolem1  23737  itg2i1fseq  23742  itg2gt0  23747  itg2cn  23750  iblcnlem  23775  itgss3  23801  itgfsum  23813  itgsplitioo  23824  itggt0  23828  limcvallem  23855  cnmptlimc  23874  limcco  23877  limciun  23878  dvfval  23881  perfdvf  23887  dvnfval  23905  dvcmul  23927  dvcobr  23929  dvmptcl  23942  dvmptco  23955  dvmptfsum  23958  dvcnvlem  23959  dveflem  23962  dvef  23963  dvferm1  23968  rolle  23973  c1liplem1  23979  dvlt0  23988  dvle  23990  dvne0  23994  lhop1lem  23996  dvfsumle  24004  dvfsumge  24005  dvfsumabs  24006  dvmptrecl  24007  dvfsumlem2  24010  itgparts  24030  itgsubstlem  24031  itgsubst  24032  deg1n0ima  24069  ply1divmo  24115  fta1blem  24148  ig1pcl  24155  elply2  24172  plyeq0lem  24186  plypf1  24188  coeeulem  24200  coeeq  24203  plycj  24253  plycpn  24264  vieta1lem1  24285  vieta1lem2  24286  plyexmo  24288  elqaalem1  24294  elqaalem3  24296  aannenlem1  24303  aaliou2  24315  taylfval  24333  taylf  24335  dvntaylp  24345  taylthlem1  24347  taylthlem2  24348  ulmcau  24369  ulmss  24371  ulmdvlem2  24375  mtest  24378  mtestbdd  24379  radcnvlt1  24392  dvradcnv  24395  pserdvlem2  24402  abelthlem2  24406  abelthlem3  24407  sincn  24418  coscn  24419  reeff1o  24421  recosf1o  24502  dvlog  24618  efopn  24625  logtayl  24627  cxple2a  24666  cxpaddlelem  24713  cxpaddle  24714  logreclem  24721  relogbval  24731  relogbcl  24732  relogbexp  24739  nnlogbexp  24740  ang180lem3  24762  birthdaylem3  24901  xrlimcnp  24916  rlimcxp  24921  jensenlem1  24934  jensenlem2  24935  jensen  24936  fsumharmonic  24959  lgamgulmlem6  24981  gamcvg2lem  25006  wilthlem2  25016  basellem9  25036  sgmnncl  25094  ppinprm  25099  chtprm  25100  chtnprm  25101  ppiltx  25124  mumul  25128  sqff1o  25129  musum  25138  dvdsmulf1o  25141  fsumdvdsmul  25142  fsumvma  25159  perfectlem2  25176  dchrelbas3  25184  dchrfi  25201  dchrptlem1  25210  dchrptlem2  25211  dchrptlem3  25212  dchrsum2  25214  bcmono  25223  lgslem1  25243  lgsdir2lem5  25275  lgsne0  25281  gausslemma2dlem1a  25311  gausslemma2dlem4  25315  lgseisenlem2  25322  lgseisenlem3  25323  lgsquadlem2  25327  2lgslem3  25350  2sqlem2  25364  mul2sq  25365  2sqlem3  25366  2sqlem7  25370  2sqlem8  25372  2sqlem11  25375  2sqblem  25377  dchrisumlem3  25401  dchrisum0flblem1  25418  dchrisum0flb  25420  pntlem3  25519  qrngdiv  25534  istrkg2ld  25580  axtgupdim2  25591  tglowdim1i  25617  tgdim01  25623  isismt  25650  tglnunirn  25664  legov  25701  hlcgreu  25734  tghilberti2  25754  tglineintmo  25758  tglowdim2ln  25767  mirreu3  25770  foot  25835  midex  25850  mideu  25851  opptgdim2  25858  hlpasch  25869  cgracol  25940  cgrg3col4  25955  f1otrg  25972  axlowdimlem13  26055  eengtrkg  26086  incistruhgr  26195  upgrex  26208  umgrnloop0  26225  upgr1e  26229  lfgrnloop  26241  edgupgr  26250  umgredg  26255  numedglnl  26261  umgrnloop2  26263  usgrausgri  26283  usgruspgrb  26298  usgrislfuspgr  26301  usgrnloop0ALT  26319  usgredg3  26330  uspgredg2vlem  26337  uspgredg2v  26338  ushgredgedg  26343  ushgredgedgloop  26345  ushgredgedgloopOLD  26346  uspgr1e  26359  usgr1e  26360  subusgr  26404  usgrres  26423  umgrres1lem  26425  upgrres1  26428  nbuhgr  26462  nbumgr  26466  uhgrnbgr0nb  26473  nbgr0vtxlem  26474  nbgrnself  26478  nbgrnself2  26479  nbupgrres  26488  edgnbusgreu  26491  edgnbusgreuOLD  26492  nbusgredgeu0  26493  nb3grprlem2  26506  nb3grpr  26507  nb3grpr2  26508  uvtxnbgrss  26519  nbupgruvtxres  26537  cplgruvtxbOLD  26546  cusgredg  26555  cplgrop  26568  cusgrsizeindslem  26582  cusgrsizeinds  26583  cusgrfilem2  26587  cusgrfilem3  26588  usgredgsscusgredg  26590  1loopgrnb0  26633  1loopgrvd2  26634  1egrvtxdg0  26642  p1evtxdeqlem  26643  umgr2v2enb1  26657  umgr2v2evd2  26658  vtxdginducedm1lem4  26673  finsumvtxdg2size  26681  finrusgrfusgr  26696  rusgrprop0  26698  rgrusgrprc  26720  wlkeq  26764  uspgr2wlkeq  26777  wlkonprop  26789  wlkon2n0  26797  wlkres  26802  wlkp1lem8  26812  wlkp1  26813  wksonproplem  26836  spthdep  26865  pthdepisspth  26866  usgr2pthlem  26894  pthdlem1  26897  pthdlem2lem  26898  pthdlem2  26899  pthd  26900  lfgrn1cycl  26933  crctcshwlkn0lem4  26941  crctcshwlkn0lem5  26942  crctcshwlkn0lem6  26943  crctcshwlkn0lem7  26944  crctcshwlkn0  26949  crctcsh  26952  wwlks  26963  wwlknllvtx  26975  iswwlksnon  26982  iswspthsnon  26986  0enwwlksnge1  26998  wlkiswwlks2lem4  27006  wlkswwlksf1o  27013  wwlksm1edg  27015  wlknwwlksnsurOLD  27024  wlkwwlkfunOLD  27030  wlkwwlksurOLD  27032  wwlksnred  27036  wwlksnextfun  27042  wwlksnextsur  27044  wwlksnndef  27049  wwlksnwwlksnon  27060  wwlksnwwlksnonOLD  27062  wspn0  27071  2wlkdlem4  27075  2wlkdlem5  27076  2pthdlem1  27077  2wlkdlem8  27080  2wlkdlem10  27082  2trld  27085  umgr2adedgwlk  27092  elwwlks2  27115  elwspths2spth  27116  rusgr0edg  27122  rusgrnumwwlks  27123  rusgrnumwwlk  27124  rusgrnumwlkg  27126  clwwlk  27133  clwwlkccatlem  27139  clwlkclwwlklem2a1  27142  clwlkclwwlklem2a4  27147  clwlkclwwlklem2a  27148  clwlkclwwlklem2  27150  clwlkclwwlkf1lem3  27156  erclwwlksym  27171  clwwlknp  27192  clwwlkinwwlk  27196  clwwlkel  27202  wwlksubclwwlk  27216  umgr2cwwk2dif  27222  erclwwlknsym  27228  clwlksfclwwlkOLD  27243  clwlksf1clwwlklem0OLD  27245  clwwlknon  27262  clwwlknon1nloop  27274  clwwlknonwwlknonbOLD  27282  clwwlknondisj  27287  clwwlknondisjOLD  27292  1wlkdlem1  27317  1wlkdlem4  27320  3wlkdlem4  27342  3wlkdlem5  27343  3pthdlem1  27344  3wlkdlem8  27347  3wlkdlem10  27349  3trld  27352  upgr3v3e3cycl  27360  upgr4cycl4dv4e  27365  eupth0  27394  eupthp1  27396  eupth2eucrct  27397  trlsegvdeg  27407  eupth2lem3lem3  27410  eupth2lem3lem6  27413  eupth2lemb  27417  eupth2lems  27418  eucrctshift  27423  eucrct2eupth1  27424  konigsbergssiedgw  27430  frcond1  27448  frcond3  27451  frcond4  27452  nfrgr2v  27454  3vfriswmgrlem  27459  3vfriswmgr  27460  1to3vfriswmgr  27462  3cyclfrgr  27470  4cycl2vnunb  27472  4cyclusnfrgr  27474  frgrncvvdeqlem1  27481  frgrncvvdeqlem9  27489  frgrwopreglem4a  27492  2wspmdisj  27519  frrusgrord0lem  27521  frrusgrord0  27522  2clwwlk2clwwlk  27534  clwwlknonclwlknonf1o  27549  dlwwlknondlwlknonf1o  27554  wlkl0  27558  clwlknon2num  27559  numclwlk1lem1  27560  numclwlk1lem2  27561  numclwlk2lem2f1o  27570  numclwlk2lem2f1oOLD  27577  numclwwlk3lemOLD  27580  numclwwlk6  27589  friendshipgt3  27597  ex-natded9.26  27618  ex-br  27630  pliguhgr  27680  isgrpo  27691  grpofo  27693  grpoideu  27703  grpoinveu  27713  nmosetn0  27960  nmoolb  27966  nmlno0lem  27988  blocnilem  27999  blocni  28000  lnocni  28001  ubthlem1  28066  minvecolem1  28070  minvecolem2  28071  minvecolem5  28077  htthlem  28114  bcsiALT  28376  hlimadd  28390  shex  28409  hsn0elch  28445  hhsst  28463  hhsscms  28476  occon  28486  pjhthmo  28501  shscli  28516  choc0  28525  choc1  28526  shintcli  28528  spancl  28535  spanss  28547  ococin  28607  chsupsn  28612  pjoc1i  28630  chlejb1i  28675  chabs2  28716  spanuni  28743  spanunsni  28778  h1datomi  28780  cmbr3i  28799  cmbr4i  28800  lecmi  28801  chscllem2  28837  osumcor2i  28843  nonbooli  28850  pjss2i  28879  pjjsi  28899  pjmf1  28915  hmopex  29074  nmoplb  29106  nmfnlb  29123  nmlnop0iALT  29194  nmopun  29213  lnconi  29232  imaelshi  29257  cnlnadjlem3  29268  cnlnadjlem5  29270  cnlnadjeui  29276  cnlnssadj  29279  adjbdln  29282  adjbdlnb  29283  adjeq0  29290  branmfn  29304  hmopidmpji  29351  pjss2coi  29363  pjnormssi  29367  pjssdif2i  29373  pjinvari  29390  pjci  29399  pjcmul2i  29401  mdsl1i  29520  mdslmd3i  29531  csmdsymi  29533  mdexchi  29534  chpssati  29562  atomli  29581  chirredi  29593  mdsymlem6  29607  sumdmdii  29614  cmmdi  29615  sumdmdlem2  29618  dmdbr5ati  29621  dmdbr6ati  29622  dmdbr7ati  29623  cdjreui  29631  cdj3i  29640  spc2ed  29652  rexunirn  29670  rabeqsnd  29680  foresf1o  29681  elpwiuncl  29697  disjrnmpt  29736  disjxpin  29739  iundisjf  29740  disjexc  29744  imadifxp  29752  funresdm1  29754  fresf1o  29773  sspreima  29787  fmptdF  29796  aciunf1lem  29802  ofpreima2  29806  funcnvmptOLD  29807  funcnvmpt  29808  fgreu  29811  fcnvgreu  29812  1stpreimas  29823  resf1o  29845  fpwrelmap  29848  xlt2addrd  29863  xrge0subcld  29868  xrofsup  29873  iocinif  29883  fzdif2  29891  iundisjfi  29895  f1ocnt  29899  divnumden2  29904  nn0min  29907  fprodex01  29911  xdivpnfrp  29981  2sqcoprm  29987  2sqmo  29989  ressprs  29995  oduprs  29996  odutos  30003  tlt3  30005  trleile  30006  ogrpaddltrbid  30061  archiabl  30092  gsummpt2co  30120  gsumvsca1  30122  gsumvsca2  30123  ofldchr  30154  rhmopp  30159  rearchi  30182  psgndmfi  30186  pmtrto1cl  30189  psgnfzto1stlem  30190  fzto1st  30193  psgnfzto1st  30195  smatlem  30203  submat1n  30211  lmatcl  30222  madjusmdetlem1  30233  qtopt1  30242  qtophaus  30243  reff  30246  locfinreflem  30247  cmpcref  30257  dispcmp  30266  metidval  30273  metideq  30276  metider  30277  pstmval  30278  pstmfval  30279  pstmxmet  30280  tpr2rico  30298  ordtrest2NEW  30309  ordtconnlem1  30310  xrge0mulc1cn  30327  fsumcvg4  30336  lmxrge0  30338  lmdvg  30339  nmmulg  30352  qqhval2lem  30365  qqhre  30404  gsumesum  30461  esumcst  30465  esumsnf  30466  esumrnmpt2  30470  esumfsup  30472  esumpinfval  30475  esumpcvgval  30480  esumcvg  30488  esumcvgre  30493  esum2dlem  30494  esum2d  30495  sigaclcu2  30523  prsiga  30534  difelsiga  30536  insiga  30540  sigagenval  30543  sigagensiga  30544  inelpisys  30557  sigapisys  30558  pwldsys  30560  sigaldsys  30562  ldsysgenld  30563  sigapildsys  30565  ldgenpisyslem1  30566  ldgenpisyslem2  30567  ldgenpisyslem3  30568  ldgenpisys  30569  rossros  30583  measvuni  30617  measssd  30618  voliune  30632  ddemeas  30639  truae  30646  isanmbfm  30658  mbfmvolf  30668  mbfmcnt  30670  br2base  30671  sxbrsigalem0  30673  dya2iocnrect  30683  dya2iocuni  30685  sxbrsigalem2  30688  oms0  30699  omssubaddlem  30701  omssubadd  30702  carsguni  30710  carsgclctunlem1  30719  carsgsiga  30724  sibfinima  30741  sitgfval  30743  sitgclg  30744  sitgaddlemb  30750  oddpwdc  30756  eulerpartlemsv2  30760  eulerpartlems  30762  eulerpartlemsv3  30763  eulerpartlemv  30766  eulerpartlemb  30770  eulerpartlemt  30773  eulerpartlemmf  30777  eulerpartlemgvv  30778  eulerpartlemgh  30780  eulerpartlemgs2  30782  sseqf  30794  prob01  30815  probun  30821  probmeasd  30825  probfinmeasbOLD  30830  probfinmeasb  30831  probmeasb  30832  dstrvprob  30873  ballotlemfc0  30894  ballotlemfcc  30895  ballotlemiex  30903  ballotlemsup  30906  ballotlemfrcn0  30931  signsply0  30968  signsvtn0  30987  signstfveq0a  30993  signshf  31005  actfunsnf1o  31022  actfunsnrndisj  31023  repr0  31029  reprsuc  31033  reprlt  31037  reprgt  31039  reprinfz1  31040  reprpmtf1o  31044  breprexp  31051  breprexpnat  31052  vtsval  31055  circlemethhgt  31061  logdivsqrle  31068  hgt750lemb  31074  tgoldbachgt  31081  bnj168  31136  bnj219  31139  bnj534  31146  bnj927  31177  bnj1142  31198  bnj1143  31199  bnj1185  31202  bnj1198  31204  bnj1209  31205  bnj1361  31237  bnj1366  31238  bnj1379  31239  bnj1542  31265  bnj110  31266  bnj97  31274  bnj149  31283  bnj150  31284  bnj535  31298  bnj545  31303  bnj546  31304  bnj548  31305  bnj553  31306  bnj571  31314  bnj605  31315  bnj594  31320  bnj580  31321  bnj607  31324  bnj600  31327  bnj917  31342  bnj934  31343  bnj944  31346  bnj964  31351  bnj966  31352  bnj967  31353  bnj969  31354  bnj910  31356  bnj978  31357  bnj986  31362  bnj996  31363  bnj1006  31367  bnj1090  31385  bnj1097  31387  bnj1110  31388  bnj1118  31390  bnj1121  31391  bnj1128  31396  bnj1137  31401  bnj1176  31411  bnj1177  31412  bnj1186  31413  bnj1189  31415  bnj1228  31417  bnj1204  31418  bnj1253  31423  bnj1296  31427  bnj1384  31438  bnj1388  31439  bnj1398  31440  bnj1408  31442  bnj1417  31447  bnj1421  31448  bnj1463  31461  bnj1312  31464  bnj1498  31467  bnj60  31468  subfacp1lem3  31502  subfacp1lem5  31504  subfacp1lem6  31505  erdszelem5  31515  erdszelem7  31517  erdszelem11  31521  kur14lem9  31534  txpconn  31552  connpconn  31555  cnllysconn  31565  iccllysconn  31570  rellysconn  31571  cvmcov  31583  cvmsss2  31594  cvmliftmo  31604  cvmlift2lem1  31622  cvmlift2lem12  31634  cvmlift2lem13  31635  cvmlift3lem2  31640  mrsubff  31747  mrsubrn  31748  mrsubff1o  31750  mrsubvrs  31757  msubff  31765  mtyf  31787  msubff1o  31792  mclsval  31798  ssmclslem  31800  mclsax  31804  mthmi  31812  climuzcnv  31903  circum  31906  lediv2aALT  31909  faclimlem1  31967  fundmpss  32002  elima4  32015  dfon2lem4  32027  dfon2lem5  32028  dfon2lem7  32030  dfon2lem9  32032  dfon2  32033  rdgprc  32036  trpredss  32065  trpredmintr  32067  dftrpred3g  32069  frpomin2  32076  poseq  32090  frrlem5  32121  frrlem5b  32122  frrlem5d  32124  frrlem11  32129  elno2  32144  nofv  32147  noreson  32150  sltres  32152  noextend  32156  noextenddif  32158  noextendlt  32159  noextendgt  32160  nolesgn2o  32161  sltsolem1  32163  nosepne  32168  nosep1o  32169  nosepdmlem  32170  nosepeq  32172  nosepssdm  32173  nodenselem8  32178  nodense  32179  noprefixmo  32185  nosupno  32186  nosupfv  32189  nosupres  32190  nosupbnd1lem4  32194  nosupbnd2lem1  32198  nosupbnd2  32199  nocvxminlem  32230  conway  32247  scutbday  32250  scutun12  32254  dmscut  32255  slerec  32260  brbigcup  32342  imagesset  32397  altopeq12  32406  colinearex  32504  btwnconn1lem14  32544  hilbert1.1  32598  hilbert1.2  32599  lineintmo  32601  rankeq1o  32615  elhf2  32619  hfsn  32623  finminlem  32649  gtinfOLD  32651  opnrebl2  32653  ntruni  32659  clsint2  32661  isfne  32671  isfne4  32672  isfne4b  32673  fneint  32680  topfneec  32687  fnessref  32689  neibastop1  32691  neibastop2lem  32692  neibastop3  32694  topmeet  32696  topjoin  32697  fnemeet1  32698  fnemeet2  32699  fnejoin1  32700  fnejoin2  32701  tailfb  32709  filnetlem3  32712  filnetlem4  32713  waj-ax  32750  nandsym1  32758  onsucconni  32773  onsucsuccmpi  32779  limsucncmpi  32781  knoppcnlem5  32824  knoppcnlem8  32827  knoppcnlem11  32830  unblimceq0  32835  unbdqndv2lem2  32838  knoppndvlem2  32841  knoppndv  32862  bj-babygodel  32925  bj-exalims  32950  bj-alsb  32963  bj-ssb1a  32970  bj-ssbid1ALT  32985  bj-sb  33014  bj-nfext  33040  bj-nfs1t  33051  bj-abbi2dv  33116  ax11-pm2  33158  bj-mo3OLD  33167  bj-vexwt  33183  bj-vexwvt  33185  bj-abv  33230  bj-ab0  33231  bj-sels  33281  bj-snglss  33289  bj-projval  33315  bj-restn0  33375  bj-rest0  33378  bj-restb  33379  bj-ismooredr  33396  bj-finsumval0  33484  mpnanrd  33515  topdifinffinlem  33532  isbasisrelowllem1  33540  isbasisrelowllem2  33541  relowlssretop  33548  cnfinltrel  33578  wl-exeq  33656  wl-euequ1f  33690  wl-ax11-lem2  33697  wl-ax11-lem8  33703  phpreu  33726  finixpnum  33727  fin2so  33729  lindsenlbs  33737  matunitlindflem1  33738  matunitlindflem2  33739  matunitlindf  33740  poimirlem3  33745  poimirlem4  33746  poimirlem9  33751  poimirlem11  33753  poimirlem12  33754  poimirlem13  33755  poimirlem14  33756  poimirlem15  33757  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem24  33766  poimirlem25  33767  poimirlem26  33768  poimirlem27  33769  poimirlem28  33770  poimirlem29  33771  poimirlem30  33772  poimirlem31  33773  poimirlem32  33774  opnmbllem0  33778  mblfinlem1  33779  mblfinlem2  33780  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  voliunnfl  33786  volsupnfl  33787  cnambfre  33790  itg2addnclem2  33794  itg2addnc  33796  itggt0cn  33814  ftc1anclem3  33819  ftc1anclem5  33821  dvasin  33828  dvacos  33829  areacirclem1  33832  areacirclem4  33835  areacirclem5  33836  cover2  33840  indexa  33860  sdclem2  33870  sdclem1  33871  fdc  33873  seqpo  33875  incsequz2  33877  nnubfi  33878  nninfnub  33879  sstotbnd2  33905  sstotbnd3  33907  equivtotbnd  33909  isbnd3  33915  ssbnd  33919  totbndbnd  33920  prdsbnd  33924  prdstotbnd  33925  cntotbnd  33927  ismtyhmeolem  33935  heibor1lem  33940  heibor1  33941  heiborlem1  33942  heiborlem3  33944  heiborlem7  33948  heiborlem8  33949  heibor  33952  rrnequiv  33966  rngoideu  34034  rngmgmbs4  34062  rngomndo  34066  rngo1cl  34070  isgrpda  34086  isdrngo2  34089  0idl  34156  divrngidl  34159  intidl  34160  unichnidl  34162  keridl  34163  igenval  34192  igenidl  34194  prnc  34198  isfldidl  34199  ispridlc  34201  alrimii  34256  spesbcdi  34257  sbceq1ddi  34260  tsna1  34283  tsna2  34284  tsna3  34285  ts3an1  34289  ts3an2  34290  ts3an3  34291  ts3or1  34292  ts3or2  34293  ts3or3  34294  mpt2bi123f  34303  mptbi12f  34307  nexmo  34355  erprt  34681  ax12eq  34749  ax12el  34750  lsatlspsn2  34801  lpssat  34822  lssat  34825  lkreqN  34979  glbconN  35185  atex  35214  2llnmat  35332  4atlem3a  35405  dalem18  35489  pmap1N  35575  2lnat  35592  dalawlem10  35688  pclunN  35706  pclfinN  35708  pol1N  35718  osumcllem10N  35773  osumcllem11N  35774  pexmidlem7N  35784  pexmidlem8N  35785  lhpocnel2  35827  4atex2-0bOLDN  35887  cdleme0nex  36099  cdlemg31b0N  36503  cdlemg31b0a  36504  cdlemh  36626  cdlemk36  36722  cdlemk19w  36781  diaval  36842  dia1N  36863  docaclN  36934  dibglbN  36976  diblss  36980  dicval  36986  dihvalrel  37089  dihwN  37099  dihglblem2aN  37103  dihglblem4  37107  dihglbcpreN  37110  dih1dimatlem  37139  dihatlat  37144  dihglblem6  37150  dihjat1  37239  dvh2dim  37255  lpolconN  37297  lcfl8b  37314  lcfrlem4  37355  lcfrlem5  37356  lcfrlem6  37357  lcfrlem16  37368  lcfrlem27  37379  lcfrlem37  37389  lcfr  37395  mapdordlem2  37447  mapdpglem3  37485  mapdhcl  37537  mapdh6dN  37549  mapdh8  37598  hdmap1l6d  37623  hdmap10  37650  hdmaprnlem17N  37673  hdmap14lem14  37691  hdmaplkr  37723  hdmapip0  37725  hgmapvv  37736  elrfi  37783  ismrcd1  37787  ismrcd2  37788  istopclsd  37789  isnacs3  37799  constmap  37802  mzpclall  37816  mzpincl  37823  mzpexpmpt  37834  mzpindd  37835  mzpcompact2lem  37840  coeq0i  37842  eldiophb  37846  diophrw  37848  eldioph2lem1  37849  eldioph2lem2  37850  eldioph2b  37852  rabdiophlem1  37891  rabdiophlem2  37892  rexzrexnn0  37894  eldioph4i  37902  fphpd  37906  fiphp3d  37909  rencldnfilem  37910  rencldnfi  37911  pellexlem4  37922  pellqrex  37969  pellfundre  37971  pellfundge  37972  pellfundglb  37975  rmxyelqirr  38001  jm2.23  38089  setindtr  38117  dford3lem2  38120  dford3  38121  wopprc  38123  wdom2d2  38128  ttac  38129  fnwe2lem1  38146  fnwe2lem2  38147  fnwe2lem3  38148  fnwe2  38149  aomclem5  38154  dfac11  38158  kelac1  38159  kelac2  38161  dfac21  38162  filnm  38186  unxpwdom3  38191  dfacbasgrp  38204  hbtlem2  38220  hbtlem5  38224  hbtlem6  38225  hbt  38226  aaitgo  38258  itgoss  38259  rgspnval  38264  rgspncl  38265  rngunsnply  38269  mendring  38288  sdrgacs  38297  idomsubgmo  38302  rp-isfinite5  38389  fiinfi  38404  relintabex  38413  refimssco  38439  mptrcllem  38446  intimag  38474  ss2iundf  38477  dfrcl2  38492  iunrelexp0  38520  iunrelexpmin1  38526  iunrelexpmin2  38530  dftrcl3  38538  trclimalb2  38544  brtrclfv2  38545  dfrtrcl3  38551  cotrclrcl  38560  unhe1  38605  frege83  38766  rfovcnvf1od  38824  brcofffn  38855  clsk1indlem2  38866  clsk1indlem4  38868  clsk1indlem1  38869  clsk1independent  38870  isotone1  38872  isotone2  38873  clsneif1o  38928  neicvgf1o  38938  clsf2  38950  gneispace  38958  imadisjld  38984  wnefimgd  38986  amgm2d  39027  amgm3d  39028  prmunb2  39036  dvgrat  39037  nzin  39043  binomcxplemnotnn0  39081  pm13.194  39139  trelpss  39184  vk15.4j  39259  tratrb  39271  truniALT  39276  hbexg  39297  2uasbanh  39302  uunT1  39532  sspwtrALT2  39580  snssiALT  39585  suctrALT2  39594  en3lpVD  39602  trintALT  39639  rspcegf  39704  sumsnd  39707  cnfex  39709  fnchoice  39710  refsumcn  39711  cncmpmax  39713  rfcnnnub  39717  pwssfi  39732  uzwo4  39742  disjiun2  39747  disjxp1  39759  ixpssmapc  39764  ssdf  39768  ssinc  39785  ssdec  39786  elixpconstg  39787  ballss3  39791  iunssd  39792  iunincfi  39793  rexanuz3  39796  eliuniin  39800  eliin2f  39808  nssd  39809  eliuniincex  39813  eliincex  39814  restuni3  39822  eliuniin2  39824  iinssiin  39833  rabssd  39853  eliunid  39862  suprnmpt  39875  rnmptpr  39878  disjf1  39889  wessf1ornlem  39891  disjrnmpt2  39895  founiiun0  39897  disjf1o  39898  fompt  39899  disjinfi  39900  projf1o  39906  mpct  39911  elmapsnd  39914  mapss2  39915  difmap  39917  unirnmap  39918  inmap  39919  difmapsn  39922  unirnmapsn  39924  iunmapss  39925  ssmapsn  39926  iunmapsn  39927  axccdom  39934  dmmptdf  39935  fvmptelrn  39946  axccd2  39948  dmmptdf2  39957  mptssid  39968  fvelimad  39976  infnsuprnmpt  39983  fvelima2  39993  xrlttri5d  40013  monoords  40028  upbdrech  40036  ssfiunibd  40040  fzdifsuc2  40041  uzfissfz  40058  iuneqfzuzlem  40066  nepnfltpnf  40074  nemnftgtmnft  40076  xrssre  40080  ssuzfz  40081  infrpge  40083  allbutfi  40132  elfzd  40152  supminfrnmpt  40188  supminfxr2  40215  qinioo  40280  iccdificc  40284  iooiinicc  40287  ressiocsup  40299  ressioosup  40300  iooiinioc  40301  ressiooinf  40302  uzinico  40305  uzubioo2  40314  fsumnncl  40321  fsumiunss  40325  fsumlessf  40327  fsumsupp0  40328  mccllem  40347  fprodcnlem  40349  limciccioolb  40371  sumnnodd  40380  limcicciooub  40387  islpcn  40389  lptre2pt  40390  limsupre  40391  limcresiooub  40392  limclr  40405  climfveq  40419  fnlimabslt  40429  climfveqf  40430  limsupub  40454  limsupequzmpt2  40468  supcnvlimsup  40490  0cnv  40492  climrescn  40498  liminfgord  40504  limsupresxr  40516  liminfresxr  40517  liminfval2  40518  liminfvalxr  40533  liminfequzmpt2  40541  liminflimsupclim  40557  xlimconst  40569  icccncfext  40618  ioodvbdlimc1lem1  40664  ioodvbdlimc1lem2  40665  ioodvbdlimc2lem  40667  dvnxpaek  40675  dvnmul  40676  dvmptfprodlem  40677  dvnprodlem1  40679  dvnprodlem2  40680  dvnprodlem3  40681  itgsinexplem1  40687  itgsubsticclem  40708  itgspltprt  40712  itgperiod  40714  voliooicof  40730  stoweidlem3  40737  stoweidlem7  40741  stoweidlem14  40748  stoweidlem17  40751  stoweidlem26  40760  stoweidlem31  40765  stoweidlem34  40768  stoweidlem35  40769  stoweidlem36  40770  stoweidlem39  40773  stoweidlem44  40778  stoweidlem46  40780  stoweidlem52  40786  stoweidlem54  40788  stoweidlem57  40791  stoweidlem59  40793  stoweidlem60  40794  wallispilem4  40802  stirlinglem5  40812  fourierdlem8  40849  fourierdlem12  40853  fourierdlem14  40855  fourierdlem27  40868  fourierdlem31  40872  fourierdlem38  40879  fourierdlem39  40880  fourierdlem40  40881  fourierdlem41  40882  fourierdlem42  40883  fourierdlem46  40886  fourierdlem48  40888  fourierdlem49  40889  fourierdlem50  40890  fourierdlem51  40891  fourierdlem53  40893  fourierdlem64  40904  fourierdlem70  40910  fourierdlem71  40911  fourierdlem73  40913  fourierdlem76  40916  fourierdlem78  40918  fourierdlem79  40919  fourierdlem80  40920  fourierdlem81  40921  fourierdlem92  40932  fourierdlem93  40933  fourierdlem94  40934  fourierdlem97  40937  fourierdlem101  40941  fourierdlem102  40942  fourierdlem103  40943  fourierdlem104  40944  fourierdlem112  40952  fourierdlem113  40953  fourierdlem114  40954  fourier2  40961  fourierswlem  40964  fouriersw  40965  elaa2lem  40967  elaa2  40968  etransclem3  40971  etransclem7  40975  etransclem10  40978  etransclem24  40992  etransclem27  40995  etransclem28  40996  etransclem35  41003  etransclem38  41006  etransclem44  41012  etransclem48  41016  rrxbasefi  41020  qndenserrnbllem  41031  qndenserrn  41036  rrxsnicc  41037  ioorrnopnlem  41041  ioorrnopnxrlem  41043  prsal  41055  salgenval  41058  intsaluni  41064  intsal  41065  salgenn0  41066  salexct  41069  salgenss  41071  issalgend  41073  salexct3  41077  salgencntex  41078  salgensscntex  41079  subsaliuncllem  41092  subsaliuncl  41093  fge0iccico  41104  sge0resplit  41140  sge0iunmptlemfi  41147  sge0fodjrnlem  41150  sge0rpcpnf  41155  sge0xaddlem2  41168  sge0xadd  41169  sge0splitsn  41175  sge0gtfsumgt  41177  sge0seq  41180  sge0reuz  41181  nnfoctbdjlem  41189  iundjiunlem  41193  iundjiun  41194  meadjiunlem  41199  ismeannd  41201  psmeasure  41205  meaiininclem  41220  omeiunle  41251  omeiunltfirp  41253  carageniuncl  41257  caratheodorylem1  41260  caratheodorylem2  41261  isomenndlem  41264  elhoi  41276  hoicvr  41282  hoissrrn  41283  hoicvrrex  41290  ovnsupge0  41291  ovnlecvr  41292  ovnpnfelsup  41293  ovnsslelem  41294  ovncvrrp  41298  ovn0lem  41299  ovnsubaddlem1  41304  ovnsubaddlem2  41305  ovnsubadd  41306  hoissrrn2  41312  hoidmvval0b  41324  hoidmv1lelem1  41325  hoidmv1lelem2  41326  hoidmv1le  41328  hoidmvlelem1  41329  hoidmvlelem2  41330  hoidmvlelem3  41331  ovnhoilem1  41335  ovnlecvr2  41344  hspdifhsp  41350  hoiqssbllem1  41356  hoiqssbllem2  41357  hoiqssbllem3  41358  hspmbllem2  41361  opnvonmbllem1  41366  opnvonmbllem2  41367  ovolval2lem  41377  ovolval4lem1  41383  ovolval5lem2  41387  vonvolmbllem  41394  vonvolmbl2  41397  vonvol2  41398  iinhoiicclem  41407  iinhoiicc  41408  iunhoiioolem  41409  iunhoiioo  41410  pimltmnf2  41431  preimagelt  41432  preimalegt  41433  pimconstlt0  41434  pimconstlt1  41435  pimltpnf  41436  pimgtpnf2  41437  pimrecltpos  41439  pimiooltgt  41441  pimgtmnf2  41444  pimdecfgtioc  41445  pimincfltioc  41446  pimdecfgtioo  41447  pimincfltioo  41448  preimageiingt  41450  preimaleiinlt  41451  pimrecltneg  41453  issmflem  41456  sssmf  41467  mbfresmf  41468  smfaddlem1  41491  decsmf  41495  smflimlem2  41500  smflimlem3  41501  smflimlem6  41504  smfresal  41515  smfmullem2  41519  smfmullem4  41521  smfpimbor1lem1  41525  smfpimcc  41534  smfsuplem1  41537  smflimsuplem2  41547  smflimsuplem7  41552  smflimsuplem8  41553  confun  41626  2rexreu  41705  2reu4a  41709  funresfunco  41725  funcoressn  41727  afvpcfv0  41746  afvfvn0fveq  41750  afvelrn  41768  nelbrnelim  41817  otiunsndisjX  41821  fun2dmnopgexmpl  41826  nltle2tri  41851  elfz2z  41853  elfzelfzlble  41859  el1fzopredsuc  41863  subsubelfzo0  41864  fzoopth  41865  fsumsplitsndif  41871  iccpartipre  41885  iccpartigtl  41887  iccpartlt  41888  iccpartgt  41891  iccpartdisj  41901  pfxfv0  41928  pfxtrcfv0  41930  pfx1  41939  pfx2  41940  pfxccatin12lem2  41952  fmtnoprmfac1  42005  fmtnoprmfac2  42007  prmdvdsfmtnof1lem1  42024  prmdvdsfmtnof  42026  lighneallem3  42052  evennodd  42084  oddneven  42085  zeoALTV  42109  divgcdoddALTV  42121  nn0e  42136  evenprm2  42151  even3prm2  42156  perfectALTVlem2  42159  sbgoldbalt  42197  mogoldbb  42201  sbgoldbmb  42202  nnsum3primesprm  42206  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  bgoldbtbndlem4  42224  bgoldbtbnd  42225  upwlkbprop  42247  elsprel  42253  spr0nelg  42254  sprssspr  42259  prelspr  42264  sprsymrelfvlem  42268  sprsymrelfo  42275  sprsymrelen  42278  uspgropssxp  42280  uspgrsprf  42282  uspgrsprfo  42284  uspgrspren  42288  plusfreseq  42300  mgmhmeql  42331  isringrng  42409  rnglz  42412  c0mhm  42438  zlidlring  42456  2zrngagrp  42471  2zrngnmrid  42478  cznabel  42482  cznrng  42483  cznnring  42484  funcrngcsetc  42526  funcrngcsetcALT  42527  rhmsubcrngclem1  42555  funcringcsetc  42563  irinitoringc  42597  fldhmsubc  42612  rngcrescrhm  42613  fldhmsubcALTV  42630  rngcrescrhmALTV  42631  eliunxp2  42640  mapprop  42652  pgrpgt2nabl  42675  rmsupp0  42677  mndpsuppss  42680  suppmptcfin  42688  lcoc0  42739  linc1  42742  lcosslsp  42755  lincext1  42771  lindslinindsimp1  42774  lindslinindimp2lem2  42776  ldepspr  42790  islindeps2  42800  lmod1  42809  lmod1zrnlvec  42811  zlmodzxzldeplem1  42817  suppdm  42828  modn0mul  42843  difmodm1lt  42845  elbigolo1  42879  fllogbd  42882  relogbdivb  42884  nnolog2flm1  42912  blennngt2o2  42914  dignnld  42925  digexp  42929  dig1  42930  nn0sumshdiglem2  42944  setrec1lem2  42963  setrec1lem3  42964  setrec2fun  42967  setrec2  42970  setis  42972  elsetrecslem  42973  onsetreclem3  42981  elpglem2  42986  alscn0d  43072  aacllem  43078
  Copyright terms: Public domain W3C validator