Theorem syl2anc 411

Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)

Hypotheses

Ref	Expression
syl2anc.1	⊢ (𝜑 → 𝜓)
syl2anc.2	⊢ (𝜑 → 𝜒)
syl2anc.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anc	⊢ (𝜑 → 𝜃)

Proof of Theorem syl2anc

Step	Hyp	Ref	Expression
1		syl2anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl2anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl2anc.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	3	ex 115	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 2, 4	sylc 62	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  syl2anc2  412  sylancl  413  sylancr  414  sylancom  420  mpdan  421  mpancom  422  orim12d  787  3imp3i2an  1185  syl13anc  1251  syl31anc  1252  mp3an2i  1353  nford  1581  eqeq12d  2211  rsp2e  2548  r19.29d2r  2641  elrab3t  2919  eueq2dc  2937  csbiedf  3125  sstrd  3194  uneq12d  3319  unssd  3340  ineq12d  3366  ssind  3388  nelprd  3649  preq12d  3708  prssd  3782  opeq12d  3817  nfopd  3826  disjiun  4029  breq12d  4047  mpteq12dva  4115  ssexd  4174  exss  4261  opexg  4262  opth  4271  ifelpwund  4518  onintexmid  4610  wetriext  4614  nnsucpred  4654  omsinds  4659  xpeq12d  4689  opelxpd  4697  poinxp  4733  eqbrrdv  4761  nfimad  5019  cossxp2  5194  cnvexg  5208  iotam  5251  funprg  5309  funtpg  5310  funimaexglem  5342  funfni  5361  fnunsn  5368  fnresdm  5370  fn0  5380  fssd  5423  fssxp  5428  fssresd  5437  fconstg  5457  fconst6g  5459  resdif  5529  f1sng  5549  nffvd  5573  sefvex  5582  feqresmpt  5618  fvelimab  5620  fvmptd  5645  fvmpt2d  5651  fvmptdf  5652  fvmptt  5656  fvmptd3  5658  elfvmptrab1  5659  eqfnfvd  5665  fnmptfvd  5669  fnreseql  5675  fimacnv  5694  dff3im  5710  ffvresb  5728  f1oresrab  5730  fmptco  5731  fmptapd  5756  fsnunf  5765  fconst3m  5784  fnex  5787  fexd  5795  foco2  5803  fcof1  5833  fcofo  5834  cocan1  5837  cocan2  5838  foeqcnvco  5840  f1eqcocnv  5841  fliftrel  5842  fliftel  5843  fliftel1  5844  fliftval  5850  isocnv2  5862  isores2  5863  isotr  5866  f1oiso2  5877  riotass2  5907  riotass  5908  oveq12d  5943  ovexg  5959  ovprc  5961  ovresd  6068  offval  6147  ofrfval  6148  ofrval  6150  ofmresval  6151  offval2  6155  ofrfval2  6156  ofco  6158  caofinvl  6165  cofunexg  6175  fnexALT  6177  opabex3d  6187  oprabexd  6193  ofmresex  6203  uchoice  6204  oprssdmm  6238  xpopth  6243  eqop  6244  2nd1st  6247  2ndrn  6250  elopabi  6262  mpofvex  6272  fnmpoovd  6282  oprab2co  6285  1stconst  6288  2ndconst  6289  cnvf1olem  6291  tposexg  6325  tposf2  6335  tposf12  6336  smoiso  6369  tfrlem1  6375  tfrlem5  6381  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemibacc  6393  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlembex  6412  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllembex  6425  tfrcllemubacc  6426  tfrcllemres  6429  tfrcl  6431  rdgivallem  6448  rdgon  6453  frecabcl  6466  frecsuclem  6473  frecrdg  6475  sucinc2  6513  oav2  6530  omv2  6532  omsuc  6539  nnsucsssuc  6559  nntr2  6570  dcdifsnid  6571  nnaordi  6575  nnaword  6578  nnmord  6584  nnmword  6585  nnaordex  6595  ercl  6612  ersym  6613  ertr  6616  swoer  6629  swoord1  6630  swoord2  6631  erth  6647  eroprf  6696  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  ecovicom  6711  ecoviass  6713  ecovidi  6715  elmapd  6730  fvdiagfn  6761  resixp  6801  f1oen2g  6823  cnvct  6877  fndmeng  6878  xpsnen2g  6897  xpdom1g  6901  xpdom3m  6902  pw2f1odclem  6904  fopwdom  6906  xpf1o  6914  xpen  6915  mapen  6916  mapdom1g  6917  mapxpen  6918  xpmapenlem  6919  phplem4dom  6932  phpm  6935  phplem4on  6937  fict  6938  fidceq  6939  fidifsnen  6940  dif1en  6949  dif1enen  6950  fisbth  6953  diffisn  6963  diffifi  6964  infnfi  6965  ac6sfi  6968  tridc  6969  fimax2gtrilemstep  6970  en2eqpr  6977  fientri3  6985  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  unfidisj  6992  undifdc  6994  prfidceq  6998  fisseneq  7004  opabfi  7008  fnfi  7011  resfnfinfinss  7014  relcnvfi  7016  funrnfi  7017  f1dmvrnfibi  7019  f1finf1o  7022  preimaf1ofi  7026  fidcenumlemrks  7028  fidcenumlemr  7030  sbthlemi9  7040  fiuni  7053  eqsupti  7071  supsnti  7080  supisolem  7083  supisoex  7084  infglbti  7100  ordiso2  7110  djuex  7118  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djulclb  7130  casefun  7160  casef  7163  djudom  7168  omp1eomlem  7169  endjusym  7171  difinfsnlem  7174  difinfsn  7175  djufun  7179  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  enumctlemm  7189  nninfninc  7198  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfisollemne  7206  enomnilem  7213  finomni  7215  fodju0  7222  mkvprop  7233  enmkvlem  7236  enwomnilem  7244  nninfwlporlemd  7247  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  cardval3ex  7265  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  djuen  7296  djuenun  7297  djuassen  7302  xpdjuen  7303  exmidontriimlem1  7306  exmidontriimlem2  7307  2omotaplemap  7342  exmidapne  7345  cc2lem  7351  cc3  7353  dfplpq2  7440  addcmpblnq  7453  addpipqqslem  7455  mulpipq2  7457  addcomnqg  7467  addassnqg  7468  distrnqg  7473  nqtri3or  7482  ltsonq  7484  ltanqg  7486  ltexnqq  7494  halfnqq  7496  subhalfnqq  7500  archnqq  7503  prarloclemarch  7504  prarloclemarch2  7505  ltrnqg  7506  enq0tr  7520  nqnq0pi  7524  addcmpblnq0  7529  nnnq0lem1  7532  nqpnq0nq  7539  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  mulcomnq0  7546  addassnq0lemcl  7547  addassnq0  7548  preqlu  7558  prltlu  7573  prarloclemlt  7579  prarloclemlo  7580  prarloclem5  7586  prarloclemcalc  7588  prarloc  7589  genplt2i  7596  genpassg  7612  addnqprllem  7613  addnqprulem  7614  addnqprl  7615  addnqpru  7616  addlocprlemeqgt  7618  addlocprlemgt  7620  addlocprlem  7621  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  addnqpr  7647  appdivnq  7649  prmuloclemcalc  7651  prmuloc  7652  prmuloc2  7653  mulnqprl  7654  mulnqpru  7655  mullocprlem  7656  mullocpr  7657  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqpr  7663  distrlem4prl  7670  distrlem4pru  7671  distrlem5prl  7672  distrlem5pru  7673  distrprg  7674  ltprordil  7675  1idprl  7676  1idpru  7677  ltnqpri  7680  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltexpri  7699  addcanprleml  7700  addcanprlemu  7701  ltaprlem  7704  ltaprg  7705  prplnqu  7706  addextpr  7707  recexprlemm  7710  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  recexpr  7724  aptiprleml  7725  aptiprlemu  7726  ltmprr  7728  archpr  7729  caucvgprlemcanl  7730  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemopu  7734  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlemladd  7744  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgpr  7748  archrecpr  7750  caucvgprlemk  7751  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemopu  7757  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemk  7769  caucvgprprlemloccalc  7770  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  caucvgprprlemnkj  7778  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemexb  7793  caucvgprprlemaddq  7794  caucvgprprlem1  7795  caucvgprprlem2  7796  caucvgprpr  7798  suplocexprlemml  7802  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  suplocexprlemlub  7810  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  prsrlem1  7828  ltsrprg  7833  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  pn0sr  7857  negexsr  7858  recexgt0sr  7859  mulgt0sr  7864  aptisr  7865  mulextsr1lem  7866  mulextsr1  7867  archsr  7868  srpospr  7869  prsradd  7872  prsrlt  7873  prsrriota  7874  caucvgsrlemcl  7875  caucvgsrlemfv  7877  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffval  7882  caucvgsrlemofff  7883  caucvgsrlemoffcau  7884  caucvgsrlemoffgt1  7885  caucvgsrlemoffres  7886  map2psrprg  7891  suplocsrlemb  7892  suplocsrlem  7894  addcnsr  7920  mulcnsr  7921  addcnsrec  7928  mulcnsrec  7929  ltrennb  7940  recidpipr  7942  recidpirqlemcalc  7943  recidpirq  7944  axaddcl  7950  axmulcl  7952  axmulcom  7957  axmulass  7959  axdistr  7960  axrnegex  7965  axcnre  7967  rereceu  7975  recriota  7976  nntopi  7980  axcaucvglemval  7983  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  addcld  8065  mulcld  8066  mulcomd  8067  readdcld  8075  remulcld  8076  axsuploc  8118  lelttr  8134  ltletr  8135  gtned  8158  lttri3d  8160  letri3d  8161  eqleltd  8162  lenltd  8163  ltled  8164  readdcan  8185  addcomd  8196  cnegex  8223  negeu  8236  addsubass  8255  subsub2  8273  subsub4  8278  negcon1d  8350  neg11ad  8352  subcld  8356  pncand  8357  pncan2d  8358  pncan3d  8359  npcand  8360  nncand  8361  negsubd  8362  subnegd  8363  subeq0d  8364  subne0d  8365  subeq0ad  8366  negdid  8369  negdi2d  8370  negsubdid  8371  negsubdi2d  8372  neg2subd  8373  resubcld  8426  negf1o  8427  mulneg1d  8456  mulneg2d  8457  mul2negd  8458  ltadd2  8465  posdif  8501  add20  8520  eqord2  8530  ltnegd  8569  lenegd  8570  ltnegcon1d  8571  ltnegcon2d  8572  lenegcon1d  8573  lenegcon2d  8574  ltaddposd  8575  ltaddpos2d  8576  ltsubposd  8577  posdifd  8578  addge01d  8579  addge02d  8580  subge0d  8581  suble0d  8582  subge02d  8583  rimul  8631  rereim  8632  apreap  8633  reapmul1lem  8640  reapmul1  8641  reapadd1  8642  reapneg  8643  remulext1  8645  cru  8648  apreim  8649  apsym  8652  addext  8656  apneg  8657  mulext1  8658  mulext  8660  apti  8668  apcon4bid  8670  leltap  8671  gt0ap0d  8675  ltap  8679  ltapd  8684  ap0gt0d  8687  subap0d  8690  aprcl  8692  lt0ap0d  8695  recexaplem2  8698  recexap  8699  mulap0bd  8703  mulcanapd  8707  muleqadd  8714  receuap  8715  divmulap  8721  divdivdivap  8759  divcanap6  8765  recclapd  8827  recap0d  8828  recidapd  8829  recidap2d  8830  recrecapd  8831  dividapd  8832  div0apd  8833  apdivmuld  8859  rerecclapd  8880  div2subap  8883  rerecapb  8889  recgt0  8896  prodgt0  8898  lt2msq  8932  lediv12a  8940  lediv2a  8941  recreclt  8946  recgt0d  8980  negiso  9001  creui  9006  nnge1  9032  nnaddcld  9057  nnmulcld  9058  nndivred  9059  halfaddsub  9244  lt2halves  9246  addltmul  9247  nn0addcld  9325  nn0mulcld  9326  gtndiv  9440  suprzclex  9443  zaddcld  9471  zsubcld  9472  zmulcld  9473  btwnapz  9475  uzneg  9639  uzm1  9651  uzin  9653  uzind4  9681  supinfneg  9688  infsupneg  9689  supminfex  9690  qmulcl  9730  qapne  9732  irrmulap  9741  rpaddcld  9806  rpmulcld  9807  rpdivcld  9808  ltrecd  9809  lerecd  9810  ltrec1d  9811  lerec2d  9812  ge0p1rpd  9821  rerpdivcld  9822  ltsubrpd  9823  ltaddrpd  9824  xrltled  9893  xnn0dcle  9896  xnn0letri  9897  xrletrid  9899  xrlelttr  9900  xrltletr  9901  xaddf  9938  xaddval  9939  rexaddd  9948  xaddnemnf  9951  xaddnepnf  9952  xaddcom  9955  xnegdi  9962  xaddass  9963  xaddass2  9964  xpncan  9965  xleadd1a  9967  xleadd1  9969  xltadd1  9970  xle2add  9973  xlt2add  9974  xsubge0  9975  xposdif  9976  xlesubadd  9977  xaddcld  9978  xadd4d  9979  xleaddadd  9981  ixxdisj  9997  ixxss1  9998  ixxss2  9999  iccsupr  10060  icoshft  10084  icoshftf1o  10085  icodisj  10086  zltaddlt1le  10101  elfz1eq  10129  fzen  10137  fzsplit  10145  elfz1end  10149  fznatpl1  10170  fzdifsuc  10175  uzdisj  10187  fseq1p1m1  10188  fzm1  10194  fzneuz  10195  fznuz  10196  uznfz  10197  fznn0sub2  10222  nn0disj  10232  elfzoelz  10241  nelfzo  10246  elfzouz2  10256  fzonnsub  10264  fzospliti  10271  fzosplit  10272  fzodisj  10273  elfzo1  10285  eluzgtdifelfzo  10292  fzocatel  10294  zpnn0elfzo  10302  fzostep1  10332  exfzdc  10335  fvinim0ffz  10336  subfzo0  10337  zsupcl  10340  zssinfcl  10341  infssuzex  10342  suprzubdc  10345  qtri3or  10349  exbtwnz  10359  qbtwnre  10365  qavgle  10367  ico0  10370  elicod  10373  apbtwnz  10383  flqlelt  10385  flqge  10391  flqlt  10392  flqwordi  10397  flqbi2  10400  fldivnn0  10404  flqaddz  10406  flqmulnn0  10408  flltdivnn0lt  10413  ceilqval  10417  intfracq  10431  flqdiv  10432  modqcl  10437  mulqmod0  10441  modqmulnn  10453  zmodcld  10456  modqcyc  10470  modqcyc2  10471  modqadd1  10472  mulqaddmodid  10475  mulp1mod1  10476  m1modnnsub1  10481  modqm1p1mod0  10486  modqltm1p1mod  10487  modqmul1  10488  q2submod  10496  modifeq2int  10497  modaddmodlo  10499  modqaddmulmod  10502  modqdi  10503  modqsubdir  10504  modsumfzodifsn  10507  addmodlteq  10509  frec2uzzd  10511  frec2uzltd  10514  frec2uzlt2d  10515  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdglem  10522  frecuzrdg0  10524  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgdomlem  10528  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  frecfzen2  10538  frec2uzled  10540  fzfig  10541  fzfigd  10542  nninfinf  10554  uzsinds  10555  seqeq3  10563  seq3val  10571  seqvalcd  10572  seqovcd  10578  seq3m1  10584  seq3fveq2  10586  seq3feq2  10587  seq3feq  10591  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqcl  10610  iseqf1olemqval  10611  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemqf1o  10617  iseqf1olemqk  10618  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1olemp  10626  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  seq3id  10636  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  exp3val  10652  expcl2lemap  10662  expap0  10680  expgt1  10688  mulexp  10689  mulexpzap  10690  expadd  10692  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  ltexp2a  10702  leexp2a  10703  leexp2r  10704  mulbinom2  10767  bernneq  10771  expnbnd  10774  expnlbnd  10775  expnlbnd2  10776  modqexp  10777  expeq0d  10780  expcld  10784  expp1d  10785  sqrecapd  10788  sqmuld  10796  reexpcld  10801  nnexpcld  10806  nn0expcld  10807  rpexpcld  10808  sqgt0apd  10812  nn0ltexp2  10820  nn0opthlem1d  10831  nn0opthlem2d  10832  nn0opthd  10833  facwordi  10851  faclbnd  10852  faclbnd2  10853  faclbnd3  10854  faclbnd6  10855  facavg  10857  bcval  10860  bcval2  10861  bcrpcl  10864  bccmpl  10865  bcnp1n  10870  bcp1nk  10873  bcval5  10874  bcp1m1  10876  bcpasc  10877  bccl2  10879  hashinfuni  10888  hashinfom  10889  hashennnuni  10890  hashennn  10891  hashcl  10892  hashfz1  10894  hashen  10895  fihasheqf1od  10900  fihashneq0  10905  fseq1hash  10912  fihashdom  10914  hashunlem  10915  hashun  10916  fihashss  10927  fiprsshashgt1  10928  fihashssdif  10929  hashdifpr  10931  hashfz  10932  hashfzp1  10935  hashxp  10937  fimaxq  10938  resunimafz0  10942  fnfz0hash  10943  ffzo0hash  10945  hashfacen  10947  leisorel  10948  zfz1isolemsplit  10949  zfz1isolemiso  10950  zfz1isolem1  10951  seq3coll  10953  wrdval  10957  iswrdiz  10961  sswrd  10963  iswrdsymb  10972  wrdfin  10973  wrdsymb  10981  wrdnval  10984  fstwrdne0  10993  wrdred1  10996  wrdred1hash  10997  shftfvalg  11002  shftfval  11005  shftval2  11010  shftval5  11013  seq3shft  11022  crre  11041  remim  11044  mulreap  11048  recj  11051  reneg  11052  readd  11053  remullem  11055  imcj  11059  imneg  11060  imadd  11061  cjexp  11077  cjap  11090  cjdivap  11093  cnrecnv  11094  cjexpd  11142  readdd  11143  imaddd  11144  resubd  11145  imsubd  11146  remuld  11147  immuld  11148  cjaddd  11149  cjmuld  11150  ipcnd  11151  remul2d  11156  immul2d  11157  crred  11160  crimd  11161  caucvgrelemcau  11164  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniq  11179  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemnmsq  11201  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  resqrtcl  11213  rersqrtthlem  11214  sqrtmul  11219  rpsqrtcl  11225  sqrtdiv  11226  abscl  11235  absvalsq  11237  absge0  11244  abs00ap  11246  absreim  11252  absdivap  11254  leabs  11258  absexp  11263  absexpzap  11264  sqabs  11266  ltabs  11271  abslt  11272  absle  11273  abssubap0  11274  abssubne0  11275  absidm  11282  abssubge0  11286  abstri  11288  abs3dif  11289  abs2difabs  11292  fzomaxdiflem  11296  caubnd2  11301  amgm2  11302  absnidd  11344  resqrtcld  11347  sqrtmsqd  11348  sqrtsqd  11349  sqrtge0d  11350  absidd  11351  absltd  11358  absled  11359  absrpclapd  11372  absexpd  11376  abssubd  11377  absmuld  11378  abstrid  11380  abs2difd  11381  abs2dif2d  11382  abs2difabsd  11383  maxabslemlub  11391  maxleastb  11398  maxltsup  11402  fimaxre2  11411  negfi  11412  minmax  11414  lemininf  11418  ltmininf  11419  bdtrilem  11423  bdtri  11424  mul0inf  11425  2zinfmin  11427  xrmaxiflemcl  11429  xrmaxifle  11430  xrmaxiflemlub  11432  xrmaxiflemval  11434  xrltmaxsup  11441  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrnegiso  11446  xrnegcon1d  11448  xrminmax  11449  xrmineqinf  11453  xrltmininf  11454  xrlemininf  11455  xrminltinf  11456  xrminadd  11459  xrbdtri  11460  climconst  11474  climuni  11477  climmpt  11484  climshft  11488  climshft2  11490  climcn2  11493  mulcn2  11496  reccn2ap  11497  cn1lem  11498  cjcn2  11500  climrecl  11508  climle  11518  iserle  11526  climserle  11529  climcau  11531  climcvg1nlem  11533  serf0  11536  sumdc  11542  sumeq2  11543  sumfct  11558  nnf1o  11560  sumrbdclem  11561  fsum3cvg  11562  sumrbdc  11563  summodclem3  11564  summodclem2a  11565  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  fsumf1o  11574  isumss  11575  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  sumsnf  11593  fsumsplitsn  11594  sumpr  11597  sumtp  11598  fsumm1  11600  fsum1p  11602  fsumsplitsnun  11603  isummulc2  11610  isumadd  11615  fsum2dlemstep  11618  fsumcnv  11621  fsum0diaglem  11624  mptfzshft  11626  fsumrev  11627  fsumshft  11628  fisumrev2  11630  fisum0diag2  11631  fsummulc2  11632  modfsummodlemstep  11641  modfsummod  11642  fsumge1  11645  fsum00  11646  fsumlt  11648  fsumabs  11649  telfsumo  11650  fsumparts  11654  fsumrelem  11655  iserabs  11659  hash2iun1dif1  11664  bcxmas  11673  isumshft  11674  isumsplit  11675  isum1p  11676  isumlessdc  11680  divcnv  11681  trireciplem  11684  trirecip  11685  expcnvap0  11686  expcnvre  11687  expcnv  11688  explecnv  11689  geosergap  11690  pwm1geoserap1  11692  absltap  11693  absgtap  11694  geolim  11695  geolim2  11696  geo2lim  11700  geoisum  11701  geoisumr  11702  geoisum1  11703  geoisum1c  11704  cvgratnnlemseq  11710  cvgratnnlemrate  11714  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  ntrivcvgap0  11733  prodeq2  11741  prodrbdclem  11755  fproddccvg  11756  prodrbdc  11758  prodmodclem3  11759  prodmodclem2a  11760  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prodfct  11771  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  prodsnf  11776  fprodm1  11782  fprod1p  11783  fprodunsn  11788  fprodcl2lem  11789  fprodfac  11799  fprodabs  11800  fprodap0  11805  fprod2dlemstep  11806  fprodcnv  11809  fprodrec  11813  fprodsplitsn  11817  fprodsplit1f  11818  fprodap0f  11820  fprodeq0g  11822  fprodle  11824  fprodmodd  11825  eftvalcn  11841  efcvgfsum  11851  ege2le3  11855  efcj  11857  efaddlem  11858  efexp  11866  eftlcl  11872  reeftlcl  11873  eftlub  11874  efgt1p2  11879  efltim  11882  eflegeo  11885  tanvalap  11892  tanclapd  11896  retanclapd  11909  efival  11916  efeul  11918  sinadd  11920  cosadd  11921  tanaddaplem  11922  tanaddap  11923  addsin  11926  sinmul  11928  cos2t  11934  cos2tsin  11935  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  cos12dec  11952  absefi  11953  absef  11954  absefib  11955  efieq1re  11956  demoivreALT  11958  eirraplem  11961  dvdsval2  11974  dvdsmodexp  11979  moddvds  11983  dvds2lem  11987  zdvdsdc  11996  iddvdsexp  11999  summodnegmod  12006  dvds2ln  12008  dvdsadd2b  12024  dvdslelemd  12027  dvdsle  12028  divconjdvds  12033  fzm1ndvds  12040  fzo0dvdseq  12041  fzocongeq  12042  dvdsfac  12044  dvdsexp  12045  dvdsmod  12046  mulmoddvds  12047  odd2np1lem  12056  odd2np1  12057  opeo  12081  omeo  12082  nn0o1gt2  12089  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  divalg  12108  divalgmod  12111  modremain  12113  fldivndvdslt  12121  bitsp1  12135  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitsfi  12141  bitscmp  12142  bitsinv1lem  12145  bitsinv1  12146  dvdsbnd  12150  nndvdslegcd  12159  gcdcld  12162  zeqzmulgcd  12164  gcdcomd  12168  divgcdnn  12169  gcdn0gt0  12172  gcdaddm  12178  modgcd  12185  bezoutlemnewy  12190  bezoutlemmain  12192  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlemeu  12201  bezoutlemle  12202  dfgcd3  12204  bezout  12205  dvdsgcd  12206  dfgcd2  12208  gcdass  12209  mulgcd  12210  gcddiv  12213  gcdmultiple  12214  gcdmultiplez  12215  gcdzeq  12216  dvdsmulgcd  12219  rplpwr  12221  rppwr  12222  sqgcd  12223  bezoutr1  12227  nnwodc  12230  uzwodc  12231  nninfctlemfo  12234  nn0seqcvgd  12236  ialgr0  12239  algrp1  12241  algcvg  12243  algcvgb  12245  eucalgval2  12248  eucalgval  12249  eucalgf  12250  eucalginv  12251  eucalglt  12252  lcmval  12258  lcmcllem  12262  lcmledvds  12265  lcmneg  12269  lcmgcdlem  12272  lcmass  12280  ncoprmgcdne1b  12284  coprmdvds2  12288  mulgcddvds  12289  rpmulgcd2  12290  qredeu  12292  rpdvds  12294  congr  12295  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  1idssfct  12310  isprm4  12314  prmind2  12315  dvdsnprmd  12320  prmdc  12325  oddprmge3  12330  sqnprm  12331  exprmfct  12333  isprm5lem  12336  isprm5  12337  coprm  12339  euclemma  12341  isprm6  12342  prmexpb  12346  prmfac1  12347  rpexp  12348  rpexp12i  12350  pw2dvdslemn  12360  pw2dvds  12361  pw2dvdseulemle  12362  oddpwdclemxy  12364  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  znege1  12373  sqrt2irraplemnn  12374  sqrt2irrap  12375  qnumdenbi  12387  divnumden  12391  numdensq  12397  nn0sqrtelqelz  12401  nonsq  12402  phivalfi  12407  phicl2  12409  phibnd  12412  hashdvds  12416  phiprmpw  12417  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  eulerth  12428  fermltl  12429  prmdiv  12430  prmdiveq  12431  hashgcdlem  12433  hashgcdeq  12435  phisum  12436  odzcllem  12438  odzdvds  12441  odzphi  12442  vfermltl  12447  modprm0  12450  nnnn0modprm0  12451  coprimeprodsq  12453  oddprm  12455  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem16  12475  pythagtriplem19  12478  pclemub  12483  pclemdc  12484  pcprendvds  12486  pcpremul  12489  pceu  12491  pccld  12496  pcmul  12497  pcdiv  12498  pcqmul  12499  pcge0  12509  pcdvdsb  12516  pcidlem  12519  pcneg  12521  pcgcd1  12524  pc2dvds  12526  pcprmpw2  12529  dvdsprmpweqle  12533  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  pcmpt2  12540  pcmptdvds  12541  pcprod  12542  fldivp1  12544  pcfaclem  12545  pcfac  12546  pcbc  12547  qexpz  12548  expnprm  12549  prmpwdvds  12551  pockthlem  12552  pockthg  12553  infpnlem1  12555  infpnlem2  12556  1arithlem4  12562  1arith  12563  4sqlem5  12578  4sqlem6  12579  4sqlem8  12581  4sqlem10  12583  mul4sqlem  12589  4sqlemafi  12591  4sqleminfi  12593  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  4sqlem12  12598  4sqlem14  12600  4sqlem16  12602  4sqlem17  12603  oddennn  12636  xpct  12640  znnen  12642  ennnfonelemk  12644  ennnfonelemp1  12650  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemrnh  12660  ennnfonelemrn  12663  ennnfonelemdm  12664  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  ctiunctlemf  12682  ctiunctlemfo  12683  ssnnctlemct  12690  nninfdclemcl  12692  nninfdclemlt  12695  unbendc  12698  isstruct2r  12716  strnfvnd  12725  setsvala  12736  setsex  12737  strsetsid  12738  setsfun  12740  setsfun0  12741  setsn0fun  12742  setscom  12745  setsslid  12756  ressbasd  12772  strressid  12776  ressval3d  12777  resseqnbasd  12778  ressinbasd  12779  ressressg  12780  strleund  12808  strext  12810  2strbasg  12824  2stropg  12825  restid2  12952  topnvalg  12955  tgval  12966  ptex  12968  prdsex  12973  prdsvalstrd  12975  prdsval  12977  prdsbaslemss  12978  prdsbas  12980  prdsplusg  12981  prdsmulr  12982  prdsbas2  12983  prdsplusgval  12987  prdsplusgfval  12988  prdsmulrval  12989  prdsmulrfval  12990  pwsval  12995  pwsbas  12996  pwselbas  12998  pwsplusgval  12999  pwsmulrval  13000  imasex  13009  imasival  13010  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfnlemg  13018  imasaddvallemg  13019  qusval  13027  qusex  13029  xpsfeq  13049  xpsfval  13052  xpsff1o  13053  xpsval  13056  plusffvalg  13066  mgmb1mgm1  13072  mgm1  13074  ismgmid2  13084  gsumfzval  13095  gsumpropd2  13097  gsum0g  13100  gsumval2  13101  gsumprval  13103  sgrp1  13115  prdssgrpd  13119  ismndd  13141  ress0g  13147  prdsidlem  13151  mnd1  13159  mnd1id  13160  mhmf1o  13174  0mhm  13190  mhmco  13194  mhmima  13195  mhmeql  13196  gsumfzz  13199  gsumwmhm  13202  gsumfzcl  13203  grppropstrg  13223  isgrpd2  13225  isgrpd  13227  grplidd  13237  grpridd  13238  grprcan  13241  grpidd2  13245  grpsubfvalg  13249  grpinvcld  13253  isgrpinv  13258  grplinvd  13259  grprinvd  13260  grpinv11  13273  grpsubinv  13277  grpinvadd  13282  grpsubsub  13293  grpaddsubass  13294  grpnpcan  13296  grpsubpropd2  13309  grp1  13310  grp1inv  13311  pwssub  13317  imasgrp2  13318  mhmlem  13322  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgval  13330  mulgfng  13332  mulgnnp1  13338  mulgnn0p1  13341  mulgnnsubcl  13342  mulgneg  13348  mulgnegneg  13349  mulgnndir  13359  mulgnn0dir  13360  mulgdirlem  13361  mulgdir  13362  mulgmodid  13369  mulgsubdir  13370  submmulg  13374  subg0  13388  subgsubcl  13393  subgsub  13394  subgmulg  13396  issubg4m  13401  subgintm  13406  isnsg3  13415  nmzsubg  13418  ssnmz  13419  1nsgtrivd  13427  releqgg  13428  eqgex  13429  eqgfval  13430  eqger  13432  eqgen  13435  eqgcpbl  13436  quseccl0g  13439  qus0  13443  isghm  13451  ghmid  13457  ghmsub  13459  ghmmulg  13464  ghmrn  13465  ghmeql  13475  ghmnsgima  13476  ghmf1o  13483  conjsubg  13485  conjsubgen  13486  conjnmz  13487  ablinvadd  13518  ablsub2inv  13519  ablsub4  13521  abladdsub4  13522  ablpncan2  13524  ablsubsub4  13527  ablpnpcan  13528  ablnncan  13529  invghm  13537  eqgabl  13538  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzconst  13549  gsumfzmhm  13551  rnglz  13579  rngrz  13580  rngmneg1  13581  rngmneg2  13582  rngm2neg  13583  rngsubdi  13585  rngsubdir  13586  srgfcl  13607  srgisid  13620  srgmulgass  13623  srgpcomp  13624  ringcom  13665  ringlz  13677  ringrz  13678  ringlzd  13679  ringrzd  13680  ring1eq0  13682  ringinvnz1ne0  13683  ringinvnzdiv  13684  ringnegl  13685  ringnegr  13686  ringmneg1  13687  ringmneg2  13688  ringm2neg  13689  ringsubdi  13690  ringsubdir  13691  ring1  13693  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrex  13732  dvdsrneg  13737  1unit  13741  unitmulcl  13747  unitmulclb  13748  unitgrp  13750  invrfvald  13756  dvrfvald  13767  dvrvald  13768  rdivmuldivd  13778  invrpropdg  13783  isrim0  13795  rhmdvdsr  13809  rhmunitinv  13812  isnzr2  13818  subrngin  13847  subrngpropd  13850  subrgin  13878  rrgeq0  13899  unitrrg  13901  domneq0  13906  aprval  13916  aprirr  13917  aprap  13920  islmodd  13927  scaffvalg  13940  lmod0vs  13955  lmodvsmmulgdi  13957  lmodfopnelem1  13958  lmodvsneg  13965  lmodcom  13967  lmodsubvs  13977  lmodsubdi  13978  lmodsubdir  13979  lssvacl  13999  lssvsubcl  14000  lss0cl  14003  lssvneln0  14007  lssvscl  14009  lssvnegcl  14010  lss1d  14017  lssintclm  14018  lspprcl  14027  lsptpcl  14028  lspss  14033  lspun  14036  lssats2  14048  lspsneli  14049  lspsnvsi  14052  lspsnss2  14053  lspsnneg  14054  lspsnsub  14055  lspun0  14059  lspsneq0b  14061  lmodindp1  14062  lsslsp  14063  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  sraex  14080  lidlss  14110  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  qusmul2  14163  gsumfzfsumlem0  14220  gsumfzfsumlemm  14221  gsumfzfsum  14222  mulgrhm  14243  zlmlemg  14262  zlmsca  14266  zlmvscag  14267  znval  14270  znle  14271  znbaslemnn  14273  znf1o  14285  znleval  14287  znfi  14289  znhash  14290  znidomb  14292  znunit  14293  znrrg  14294  psrval  14298  psrbaglesuppg  14304  psrbasg  14305  psrplusgg  14308  psrnegcl  14313  psrgrp  14315  psr0  14316  toponsspwpwg  14344  topontopn  14359  tgidm  14396  2basgeng  14404  uncld  14435  cldcls  14436  iuncld  14437  clsss  14440  ntrss  14441  neival  14465  neiint  14467  neiss  14472  neipsm  14476  topssnei  14484  resttopon  14493  restco  14496  ssrest  14504  restdis  14506  lmfval  14514  iscnp3  14525  cnprcl2k  14528  tgcn  14530  lmbrf  14537  iscnp4  14540  cnpnei  14541  cnco  14543  cnptopco  14544  cnclima  14545  cnntr  14547  cnss1  14548  cnss2  14549  cncnpi  14550  cncnp  14552  cncnp2m  14553  cnconst2  14555  cnrest  14557  cnrest2  14558  cnptopresti  14560  cnptoprest  14561  cnptoprest2  14562  lmss  14568  lmtopcnp  14572  lmcn  14573  txbasval  14589  neitx  14590  tx1cn  14591  tx2cn  14592  txcnp  14593  upxp  14594  uptx  14596  txcn  14597  txrest  14598  txdis1cn  14600  txlm  14601  lmcn2  14602  cnmpt11  14605  cnmpt1t  14607  cnmpt12  14609  cnmpt1st  14610  cnmpt2nd  14611  cnmpt2c  14612  cnmpt21  14613  cnmpt2t  14615  cnmpt22  14616  cnmpt22f  14617  cnmpt1res  14618  cnmpt2res  14619  cnmptcom  14620  imasnopn  14621  hmeontr  14635  hmeoimaf1o  14636  hmeores  14637  txswaphmeo  14643  psmetsym  14651  psmetxrge0  14654  psmetres2  14655  isxmet2d  14670  mettri2  14684  xmetsym  14690  xmetrtri  14698  xblpnfps  14720  xblpnf  14721  bldisj  14723  bl2in  14725  xblss2ps  14726  xblss2  14727  blss2ps  14728  blss2  14729  unirnblps  14744  unirnbl  14745  ssblps  14747  ssbl  14748  blssps  14749  blss  14750  ssblex  14753  blbas  14755  xmeter  14758  xmetresbl  14762  setsmsbasg  14801  setsmsdsg  14802  setsmstsetg  14803  neibl  14813  metss  14816  metss2  14820  comet  14821  bdmetval  14822  bdxmet  14823  bdmet  14824  bdbl  14825  bdmopn  14826  mopnex  14827  metrest  14828  xmetxp  14829  xmetxpbl  14830  xmettxlem  14831  xmettx  14832  metcnp  14834  metcnpi3  14839  txmetcnp  14840  txmetcn  14841  bl2ioo  14872  ioo2bl  14873  ioo2blex  14874  blssioo  14875  tgioo  14876  tgqioo  14877  addcncntoplem  14883  fsumcncntop  14889  cncff  14899  cncfi  14900  elcncf1di  14901  rescncf  14903  cncfcdm  14904  climcncf  14906  mulc1cncf  14911  cncfco  14913  cncfmet  14914  mulcncflem  14929  mulcncf  14930  cnopnap  14933  maxcncf  14937  mincncf  14938  dedekindeulemuub  14939  dedekindeulemub  14940  dedekindeulemlu  14943  dedekindeu  14945  suplociccreex  14946  suplociccex  14947  dedekindicclemuub  14948  dedekindicclemub  14949  dedekindicclemlu  14952  dedekindicclemeu  14953  dedekindicclemicc  14954  dedekindicc  14955  ivthinclemlm  14956  ivthinclemum  14957  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthinc  14965  ivthreinc  14967  hovera  14969  hoverb  14970  hoverlt1  14971  hovergt0  14972  ellimc3apf  14982  limcimolemlt  14986  limcimo  14987  cnplimcim  14989  cnplimclemr  14991  cnlimci  14995  limccnpcntop  14997  limccnp2lem  14998  limccnp2cntop  14999  reldvg  15001  dvfvalap  15003  dvbss  15007  dvfgg  15010  dvidlemap  15013  dvidrelem  15014  dvidsslem  15015  dvcnp2cntop  15021  dvaddxxbr  15023  dvmulxxbr  15024  dvaddxx  15025  dvmulxx  15026  dviaddf  15027  dvimulf  15028  dvcoapbr  15029  dvcjbr  15030  dvrecap  15035  dvmptclx  15040  dvmptcjx  15046  dvmptfsum  15047  dveflem  15048  plyss  15060  ply1termlem  15064  plyaddlem1  15069  plymullem1  15070  plyaddlem  15071  plysub  15075  plycoeid3  15079  plycolemc  15080  plycjlemc  15082  plycj  15083  plyreres  15086  dvply1  15087  reeff1oleme  15094  eflt  15097  sin0pilem1  15103  sin0pilem2  15104  ptolemy  15146  tanrpcl  15159  tangtx  15160  cosordlem  15171  cos11  15175  logdivlti  15203  relogmuld  15206  relogdivd  15207  logled  15208  rplogcld  15210  logge0d  15211  rpcxpadd  15227  rpmulcxp  15231  cxpmul  15234  rpcxproot  15236  cxplt  15238  cxple  15239  rpcxple2  15240  rpcxplt2  15241  cxplt3  15242  cxple3  15243  rpcxpsqrt  15244  rpcncxpcld  15249  rpcxpsqrtth  15252  cxprecd  15253  rpcxpcld  15255  logcxpd  15256  apcxp2  15261  rpabscxpbnd  15262  ltexp2  15263  rplogbval  15267  relogbval  15273  relogbzcl  15274  nnlogbexp  15281  logbrec  15282  rpcxplogb  15286  logbgcd1irr  15289  logbgcd1irraplemexp  15290  logbgcd1irraplemap  15291  wilthlem1  15302  sgmval2  15306  dvdsppwf1o  15311  mpodvdsmulf1o  15312  fsumdvdsmul  15313  sgmppw  15314  mersenne  15319  perfect1  15320  perfectlem1  15321  perfectlem2  15322  perfect  15323  lgslem1  15327  lgslem4  15330  lgsval  15331  lgsfvalg  15332  lgsfcl2  15333  lgscllem  15334  lgsval2lem  15337  lgsneg  15351  lgsneg1  15352  lgsmod  15353  lgsdir2  15360  lgsdirprm  15361  lgsdir  15362  lgsdilem2  15363  lgsdi  15364  lgsne0  15365  lgssq  15367  lgssq2  15368  lgsmulsqcoprm  15373  lgsdirnn0  15374  lgsdinn0  15375  gausslemma2dlem0c  15378  gausslemma2dlem0d  15379  gausslemma2dlem0i  15384  gausslemma2dlem1a  15385  gausslemma2dlem1cl  15386  gausslemma2dlem1f1o  15387  gausslemma2dlem4  15391  gausslemma2dlem6  15394  gausslemma2dlem7  15395  gausslemma2d  15396  lgseisenlem1  15397  lgseisenlem2  15398  lgseisenlem3  15399  lgseisenlem4  15400  lgseisen  15401  lgsquadlemsfi  15402  lgsquadlem1  15404  lgsquadlem2  15405  lgsquadlem3  15406  lgsquad2lem1  15408  lgsquad2  15410  lgsquad3  15411  2lgslem3b1  15425  2lgslem3c1  15426  2lgsoddprm  15440  2sqlem2  15442  mul2sq  15443  2sqlem3  15444  2sqlem4  15445  2sqlem7  15448  2sqlem8a  15449  2sqlem8  15450  spimd  15497  djucllem  15532  bdssexd  15637  nnti  15725  2omapen  15729  pwf1oexmid  15732  subctctexmid  15733  domomsubct  15734  pw1nct  15736  nnsf  15738  nninfself  15746  nninfsellemeq  15747  nninfsellemeqinf  15749  nninffeq  15753  nnnninfex  15755  qdencn  15762  refeq  15763  cvgcmp2nlemabs  15767  trilpolemeq1  15775  trilpolemlt1  15776  trirec0  15779  apdifflemf  15781  apdifflemr  15782  apdiff  15783  redcwlpo  15790  reap0  15793  nconstwlpolemgt0  15799  neap0mkv  15804