MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ex Structured version   Unicode version

Theorem ex 425
Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule  -> I ( -> introduction), see natded 21713. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
exp.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ex  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem ex
StepHypRef Expression
1 df-an 362 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
2 exp.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylbir 206 . 2  |-  ( -.  ( ph  ->  -.  ps )  ->  ch )
43expi 144 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360
This theorem is referenced by:  expcom  426  exp3a  427  impancom  429  pm2.01da  431  pm2.18da  432  pm3.2  436  jao  500  pm2.65da  561  expimpd  588  exp31  589  exp32  590  exp4b  592  exp41  595  exp43  597  exp53  602  impr  604  simplbi2  610  pm5.32da  624  anidms  628  mtand  642  syl2anc  644  pm5.74da  670  imdistanda  676  jaoian  761  jaodan  762  pm2.61ian  767  pm2.61dan  768  impbida  807  anim12dan  812  pm5.21nd  870  ecase  910  prlem1  930  pm3.2an3  1134  3jcad  1136  3impia  1151  3an1rs  1166  3exp1  1170  3exp2  1172  exp520  1175  syl3anl2  1234  3jaoian  1250  3jaodan  1251  mp3anl1  1274  mp3anl2  1275  mp3anl3  1276  inegd  1343  alanimi  1572  exlimddv  1649  nfimdOLD  1829  exlimdd  1913  sbequ1  1944  spimedOLD  1962  cbvaldva  1995  cbvexdva  1996  ax12o  2011  ax12OLD  2021  nfald2  2065  dvelimhOLD  2073  ax11v2OLD  2080  equveli  2086  equveliOLD  2087  sbequi  2112  sbequiOLD  2116  nfsb4tOLD  2130  sbiedv  2155  dvelimdfOLD  2159  sbcom  2166  sbcomOLD  2167  sbcom2  2192  sbal1  2205  dvelimALT  2212  ax12from12o  2235  dvelimf-o  2259  ax11indi  2275  ax11inda  2279  ax11v2-o  2280  eupickbi  2349  moexex  2352  axbnd  2418  nfabd2  2592  dvelimdc  2594  pm2.61dane  2684  rgen2a  2774  ralimiaa  2782  ralimdaa  2785  ralrimiva  2791  ralrimdva  2798  ralrimivva  2800  ralrimdvv  2802  ralrimdvva  2803  reximdva  2820  rexlimiva  2827  rexlimdva  2832  rexlimdvva  2839  r19.29_2a  2854  ralcom2  2874  2gencl  2987  vtocldf  3005  spcimdv  3035  rspct  3047  eqvinc  3065  ceqex  3068  reu6  3125  eqreu  3128  2rmorex  3140  2reu5  3144  sbciedf  3198  rmob  3251  csbiebt  3289  csbiedf  3290  sspsstr  3454  psssstr  3455  reupick  3627  reximdva0  3641  ssn0  3662  uneqdifeq  3718  r19.2zb  3720  prel12  3977  dfnfc2  4035  intssuni  4074  unissint  4076  intab  4082  uniintsn  4089  iineq2d  4115  ssiun2  4136  disjiun  4204  disjxiun  4211  mpteq2da  4296  trintss  4320  copsexg  4444  copsex2t  4445  pwssun  4491  sess1  4552  sess2  4553  frminex  4564  wefrc  4578  wereu2  4581  ordelord  4605  tron  4606  tz7.7  4609  onfr  4622  onelss  4625  ordtr2  4627  ordtr3  4628  ordunidif  4631  ordintdif  4632  onintss  4633  suctr  4667  ordsssuc2  4672  ordtri2or2  4680  unizlim  4700  reusv1  4725  reusv2lem2  4727  reusv2lem3  4728  reusv3  4733  reusv6OLD  4736  rabxfrd  4746  iunpw  4761  dfwe2  4764  ssorduni  4768  onint  4777  onint0  4778  oninton  4782  onnminsb  4786  oneqmin  4787  ordsuc  4796  ordpwsuc  4797  ordsucelsuc  4804  ordsucuniel  4806  ordsucun  4807  ordunisuc2  4826  limsuc  4831  limsssuc  4832  tfi  4835  tfisi  4840  tfindsg  4842  tfindsg2  4843  dfom2  4849  limomss  4852  nn0suc  4871  findsg  4874  posn  4948  frsn  4950  2optocl  4955  relop  5025  releldmb  5106  relelrnb  5107  elrnmptg  5122  relimasn  5229  elrelimasn  5230  relbrcnvg  5245  trin2  5259  sotri2  5265  soltmin  5275  ssxpb  5305  sofld  5320  soex  5321  relresfld  5398  relcoi1  5400  iotaval  5431  funmo  5472  imadif  5530  2elresin  5558  feu  5621  fcnvres  5622  f1oun  5696  f1oprg  5720  funbrfv  5767  funbrfv2b  5773  dffn5  5774  dfimafn  5777  funimass4  5779  ssimaex  5790  funfv  5792  dffv2  5798  fvmptss  5815  fvmptf  5823  fvimacnv  5847  funimass3  5848  elpreima  5852  iinpreima  5862  elrnrexdm  5876  eldmrexrn  5878  dff3  5884  dffo4  5887  dffo5  5888  fmpt  5892  ffvresb  5902  fsn  5908  fconst5  5951  funrnex  5969  zfrep6  5970  f1dmex  5973  funfvima  5975  funfvima2  5976  f1mpt  6009  f1imass  6012  f1ocnvfvrneq  6021  foeqcnvco  6029  f1eqcocnv  6030  fliftfun  6036  fliftf  6039  isomin  6059  isofrlem  6062  isopolem  6067  isosolem  6069  weniso  6077  wemoiso  6080  wemoiso2  6081  oprabid  6107  oprabexd  6188  ovidi  6194  ovg  6214  nssdmovg  6231  suppssfv  6303  suppssov1  6304  fo2ndres  6373  op1steq  6393  dfoprab3  6405  bropopvvv  6428  curry1val  6441  curry2val  6445  fo2ndf  6455  f1o2ndf1  6456  frxp  6458  poxp  6460  soxp  6461  mpt2xopxnop0  6468  mpt2xopynvov0  6471  mpt2xopoveqd  6474  brovex  6476  isprmpt2  6479  reldmtpos  6489  brtpos  6490  rntpos  6494  tposf2  6505  tposf12  6506  nfriotad  6560  riotaxfrd  6583  eusvobj2  6584  riotaprc  6589  riotasvdOLD  6595  riotasv2dOLD  6597  riotasv3dOLD  6601  onfununi  6605  issmo2  6613  smores  6616  smoiso  6626  smo11  6628  smorndom  6632  smoiso2  6633  tfrlem1  6638  tfrlem5  6643  tfrlem9  6648  tfrlem11  6651  tz7.44-3  6668  rdgsucmptnf  6689  rdglim2  6692  frsucmptn  6698  tz7.48-3  6703  tz7.49  6704  abianfplem  6717  abianfp  6718  oe0lem  6759  oevn0  6761  oecl  6783  oa0r  6784  om1r  6788  oe1m  6790  oaordi  6791  oawordex  6802  oaordex  6803  oaass  6806  omordi  6811  omord  6813  omcan  6814  omwordi  6816  om00  6820  odi  6824  omass  6825  oneo  6826  omopth2  6829  oen0  6831  oeordi  6832  oewordri  6837  oeworde  6838  oeordsuc  6839  oelim2  6840  oeoalem  6841  oeoa  6842  oeoe  6844  oeeui  6847  nnaordi  6863  nnawordi  6866  nnmcom  6871  nnmord  6877  nnmwordi  6880  nnawordex  6882  nnaordex  6883  oaabs  6889  oaabs2  6890  omabs  6892  nnneo  6896  ertr  6922  erex  6931  iserd  6933  erdisj  6954  iiner  6978  erinxp  6980  qsel  6985  qliftfun  6991  qliftfund  6992  2ecoptocl  6997  brecop  6999  eceqoveq  7011  mapss  7058  ixpssmap2g  7093  ixpssmapg  7094  undifixp  7100  resixpfo  7102  boxriin  7106  boxcutc  7107  brdomg  7120  dom2lem  7149  fundmen  7182  unen  7191  domdifsn  7193  undom  7198  xpdom2  7205  omxpenlem  7211  fopwdom  7218  sdomdomtr  7242  domsdomtr  7244  fodomr  7260  2pwuninel  7264  domssex  7270  xpf1o  7271  mapen  7273  mapxpen  7275  mapunen  7278  mapdom2  7280  ssenen  7283  infensuc  7287  phplem4  7291  nneneq  7292  php  7293  php3  7295  onomeneq  7298  nndomo  7302  sucdom2  7305  sucdom  7306  sucdomiOLD  7307  pssinf  7321  isinf  7324  fineqvlem  7325  pssnn  7329  ssfi  7331  domfi  7332  f1finf1o  7337  enp1i  7345  findcard2  7350  findcard2s  7351  findcard3  7352  ac6sfi  7353  frfi  7354  fimax2g  7355  fisupg  7357  unblem2  7362  unblem3  7363  isfinite2  7367  nnsdomg  7368  xpfi  7380  domunfican  7381  fiint  7385  fodomfib  7388  fofinf1o  7389  infssuni  7399  ixpfi2  7407  finsschain  7415  indexfi  7416  ssfii  7426  fieq0  7428  dffi2  7430  dffi3  7438  marypha1lem  7440  marypha2  7446  eqsup  7463  supmaxlem  7471  fisup2g  7473  fisupcl  7474  supisoex  7478  ordiso2  7486  ordtypelem7  7495  ordtypelem9  7497  ordtypelem10  7498  oieu  7510  oismo  7511  hartogslem1  7513  wofib  7516  wemappo  7520  card2inf  7525  brwdomn0  7539  brwdom2  7543  domwdom  7544  wdomtr  7545  wdomd  7551  brwdom3  7552  xpwdomg  7555  unxpwdom2  7558  suc11reg  7576  inf3lem1  7585  inf3lem5  7589  infdiffi  7614  noinfepOLD  7617  cantnflt  7629  cantnfreslem  7633  cantnfp1lem3  7638  cantnflem3  7649  cantnf  7651  wemapwe  7656  cnfcom  7659  cnfcom3lem  7662  trcl  7666  epfrs  7669  en3lplem2  7673  tc00  7689  r1tr  7704  r1ordg  7706  r1pwss  7712  r1val1  7714  rankr1ai  7726  rankr1c  7749  rankelb  7752  rankval3b  7754  rankonidlem  7756  onssr1  7759  r1pw  7773  r1pwcl  7775  rankssb  7776  rankeq0b  7788  rankxplim3  7807  tcrank  7810  hta  7823  xpnum  7840  cardne  7854  carden2a  7855  cardlim  7861  harcard  7867  carduni  7870  cardiun  7871  isinffi  7881  pm54.43  7889  pr2nelem  7890  pr2ne  7891  en2eqpr  7893  infxpenlem  7897  infxpenc2lem1  7902  infxpenc2  7905  fseqenlem2  7908  fseqdom  7909  dfac8alem  7912  dfac8clem  7915  ac10ct  7917  indcardi  7924  acni2  7929  acndom2  7937  fodomacn  7939  numwdom  7942  wdomfil  7944  infpwfien  7945  alephcard  7953  alephnbtwn  7954  alephordi  7957  alephord2i  7960  alephsucdom  7962  alephdom  7964  cardaleph  7972  cardalephex  7973  cardinfima  7980  alephval3  7993  iunfictbso  7997  dfac5lem4  8009  dfac5  8011  dfac2  8013  dfac9  8018  dfac12lem2  8026  dfac12lem3  8027  dfac12r  8028  dfac12k  8029  kmlem11  8042  cdainflem  8073  cdainf  8074  pwsdompw  8086  infdif  8091  infdif2  8092  infxp  8097  infmap2  8100  ackbij2lem1  8101  ackbij1lem5  8106  ackbij1lem14  8115  ackbij1lem16  8117  ackbij1lem18  8119  ackbij1b  8121  ackbij2lem2  8122  ackbij2lem3  8123  ackbij2  8125  fictb  8127  cfub  8131  cfflb  8141  cfss  8147  cfslb2n  8150  cofsmo  8151  cfsmolem  8152  coftr  8155  cfcof  8156  sornom  8159  infpssrlem4  8188  infpssrlem5  8189  infpssr  8190  fin4en1  8191  fin23lem7  8198  isfin2-2  8201  ssfin2  8202  enfin2i  8203  fin23lem24  8204  fincssdom  8205  fin23lem25  8206  fin23lem26  8207  fin23lem14  8215  fin23lem20  8219  fin23lem28  8222  fin23lem30  8224  fin23lem32  8226  isf32lem5  8239  isf32lem9  8243  isf32lem10  8244  isf34lem4  8259  enfin1ai  8266  isfin1-2  8267  isfin1-3  8268  fin56  8275  isfin7-2  8278  fin1a2lem6  8287  fin1a2lem9  8290  fin1a2lem11  8292  fin1a2lem13  8294  fin12  8295  fin1a2s  8296  axcc3  8320  axcc4dom  8323  domtriomlem  8324  axdc2lem  8330  axdc3lem2  8333  axdc3lem4  8335  axdc4lem  8337  axcclem  8339  ac6num  8361  ac6c4  8363  zorn2lem4  8381  zorn2lem6  8383  zorn2lem7  8384  ttukeylem1  8391  ttukeylem5  8395  ttukeylem6  8396  axdclem2  8402  fodomb  8406  brdom6disj  8412  iunfo  8416  iundom2g  8417  uniimadom  8421  carden  8428  cardmin  8441  ficard  8442  konigthlem  8445  alephval2  8449  alephadd  8454  alephreg  8459  pwcfsdom  8460  cfpwsdom  8461  smobeth  8463  axextnd  8468  axrepndlem1  8469  axrepndlem2  8470  axunnd  8473  axpowndlem2  8475  axpowndlem3  8476  axpowndlem4  8477  axpownd  8478  axregndlem2  8480  axregnd  8481  axinfndlem1  8482  axinfnd  8483  axacndlem4  8487  axacndlem5  8488  axacnd  8489  fpwwe2lem8  8514  fpwwe2lem9  8515  fpwwe2lem10  8516  fpwwe2lem11  8517  fpwwe2lem12  8518  fpwwe2lem13  8519  fpwwe2  8520  canthwe  8528  canthp1lem2  8530  canthp1  8531  gchcda1  8533  pwfseqlem1  8535  pwfseqlem4a  8538  pwfseqlem4  8539  pwfseq  8541  gchaclem  8547  gchpwdom  8551  inawinalem  8566  winalim2  8573  gchina  8576  wunom  8597  wuncval2  8624  inar1  8652  inatsk  8655  tskord  8657  tskcard  8658  r1tskina  8659  tskuni  8660  gruiun  8676  gruima  8679  intgru  8691  ingru  8692  grudomon  8694  grur1a  8696  grur1  8697  grutsk  8699  addcanpi  8778  mulcanpi  8779  nlt1pi  8785  indpi  8786  nqereu  8808  nqerf  8809  recmulnq  8843  ltexnq  8854  ltbtwnnq  8857  prcdnq  8872  npomex  8875  genpss  8883  genpnnp  8884  genpcd  8885  1idpr  8908  prlem934  8912  ltexprlem2  8916  ltexprlem3  8917  ltexprlem4  8918  ltexprlem7  8921  ltexpri  8922  prlem936  8926  reclem2pr  8927  reclem3pr  8928  suplem1pr  8931  suplem2pr  8932  map2psrpr  8987  supsrlem  8988  supsr  8989  axrrecex  9040  axpre-sup  9046  1re  9092  mul02lem2  9245  cnegex  9249  add20  9542  mulge0  9547  recex  9656  mul0or  9664  recgt0  9856  prodgt02  9858  prodge02  9860  ltmul1  9862  lemul12b  9869  lemul12a  9870  ledivmulOLD  9886  ledivp1i  9938  fimaxre3  9959  sup2  9966  supmul1  9975  supmullem1  9976  supmul  9978  infmrcl  9989  inelr  9992  rimul  9993  cru  9994  nnrecgt0  10039  addltmul  10205  nominpos  10206  nn0sub  10272  nn0n0n1ge2b  10283  elnnz  10294  zrevaddcl  10323  zextle  10345  peano5uzi  10360  uzind2  10364  uzindOLD  10366  fzind  10370  fnn0ind  10371  nn0ind-raph  10372  btwnz  10374  uz11  10510  eluzp1m1  10511  uzwo  10541  uzwoOLD  10542  lbzbi  10566  zsupss  10567  zmax  10573  zbtwnre  10574  qreccl  10596  qrevaddcl  10598  irradd  10600  irrmul  10601  rpnnen1lem5  10606  xrlttri  10734  qbtwnre  10787  qsqueeze  10789  qextltlem  10790  xleadd1  10836  xle2add  10840  xsubge0  10842  xlesubadd  10844  xmulge0  10865  xlemul1a  10869  xlemul1  10871  xrsupexmnf  10885  xrinfmexpnf  10886  xrsupsslem  10887  xrinfmsslem  10888  xrub  10892  supxrpnf  10899  supxrunb1  10900  supxrunb2  10901  supxrbnd  10909  ixxss1  10936  ixxss2  10937  ixxss12  10938  ixxub  10939  ixxlb  10940  iccid  10963  ico0  10964  ioc0  10965  elioc2  10975  elico2  10976  elicc2  10977  prunioo  11027  difreicc  11030  iccsplit  11031  fzen  11074  0fz1  11076  fzopth  11091  fzss1  11093  fzss2  11094  uzsplit  11120  1fv  11122  fzm1  11129  fznuz  11131  fzrevral  11133  fzosplit  11168  fzouzsplit  11170  fzofzp1b  11192  elfznelfzo  11194  elfznelfzob  11195  injresinjlem  11201  injresinj  11202  modid2  11273  modabs2  11277  om2uzrdg  11298  fzennn  11309  uzindi  11322  seqcl2  11343  seqf1o  11366  seqid  11370  seqz  11373  seqof  11382  expcl2lem  11395  expnegz  11416  leexp2r  11439  leexp1a  11440  sqlecan  11489  sq01  11503  zesq  11504  facdiv  11580  facndiv  11581  facwordi  11582  faclbnd  11583  faclbnd6  11592  facubnd  11593  bcval4  11600  bcpasc  11614  bccl  11615  fiinfnf1o  11636  hasheqf1oi  11637  hashf1rn  11638  hashclb  11643  hasheq0  11646  hashdom  11655  hashinfxadd  11661  hashunx  11662  hashnn0n0nn  11666  elprchashprn2  11669  hashprb  11670  hashle00  11671  hashgt0elex  11672  hash1snb  11683  hashgt12el2  11685  hash2prde  11690  hash2prb  11691  hashtpg  11693  hashfzo  11696  hashxplem  11698  hashfun  11702  hashbclem  11703  hashfacen  11705  hashf1lem1  11706  leisorel  11711  seqcoll  11714  brfi1indlem  11716  brfi1uzind  11717  ccatopth  11778  wrdind  11793  s2f1o  11865  f1oun2prg  11866  s4dom  11868  reim0b  11926  sqeqd  11973  sqr0  12049  sqrlem1  12050  sqrlem6  12055  resqrex  12058  sqrmo  12059  abs00  12096  absnid  12105  absor  12107  absexpz  12112  abslt  12120  absle  12121  abs3lem  12144  r19.29uz  12156  r19.2uz  12157  rexuzre  12158  cau3lem  12160  caubnd2  12163  caubnd  12164  sqreu  12166  clim  12290  rlim  12291  lo1bdd2  12320  lo1o1  12328  o1lo1  12333  o1lo12  12334  rlimuni  12346  rlimdm  12347  climuni  12348  rlimresb  12361  lo1eq  12364  rlimeq  12365  rlimcn2  12386  climcn1  12387  climcn2  12388  mulcn2  12391  o1dif  12425  iserex  12452  isercolllem1  12460  isercolllem2  12461  isercoll  12463  climcau  12466  caucvg  12474  caucvgb  12475  sumrblem  12507  fsumcvg  12508  summolem2a  12511  summolem2  12512  zsum  12514  sumz  12518  fsumf1o  12519  sumss  12520  fsumss  12521  fsumcvg2  12523  fsumcvg3  12525  fsum2dlem  12556  fsum00  12579  fsumabs  12582  fsumrlim  12592  fsumo1  12593  o1fsum  12594  cvgcmp  12597  fsumiun  12602  qshash  12608  bcxmas  12617  incexclem  12618  isumsplit  12622  supcvg  12637  cvgrat  12662  mertenslem2  12664  efexp  12704  efieq1re  12802  rpnnen2lem11  12826  rpnnen2  12827  ruclem3  12834  ruclem13  12843  sqr2irr  12850  dvdsval2  12857  dvds0  12867  absdvdsb  12870  dvdsabsb  12871  dvdsmul1  12873  dvdscmul  12878  dvdsmulc  12879  dvds2ln  12882  dvds2add  12883  dvds2sub  12884  dvdslelem  12896  dvdseq  12899  dvds1  12900  dvdsext  12902  fzo0dvdseq  12904  dvdsfac  12906  odd2np1  12910  divalglem8  12922  divalglem9  12923  sadcaddlem  12971  sadcadd  12972  sadadd2  12974  saddisjlem  12978  saddisj  12979  sadadd  12981  sadass  12985  bitsuz  12988  smupvallem  12997  smu01lem  12999  smueqlem  13004  smumul  13007  gcdeq0  13023  gcd0id  13025  gcdneg  13028  gcdaddmlem  13030  gcdabs  13035  bezoutlem1  13040  bezoutlem3  13042  bezout  13044  dvdsgcd  13045  rppwr  13059  dvdssqlem  13061  seq1st  13064  algfx  13073  eucalglt  13078  eucalgcvga  13079  isprm2lem  13088  prmind2  13092  coprm  13102  coprmdvds  13104  qredeq  13108  qredeu  13109  isprm6  13111  isprm5  13114  prmfac1  13120  divgcdodd  13121  rpexp  13122  rpdvds  13126  nonsq  13153  hashdvds  13166  phimullem  13170  eulerthlem2  13173  prmdiveq  13177  pythagtrip  13210  iserodd  13211  pcexp  13235  pc11  13255  pcprmpw  13258  pcadd2  13261  pcmptcl  13262  pcfac  13270  expnprm  13273  prmpwdvds  13274  unbenlem  13278  infpnlem1  13280  prmunb  13284  prmreclem1  13286  prmreclem2  13287  prmreclem3  13288  prmreclem5  13290  prmreclem6  13291  1arith  13297  4sqlem11  13325  4sqlem13  13327  4sqlem16  13330  vdwmc2  13349  vdwlem6  13356  vdwlem7  13357  vdwlem11  13361  vdwlem12  13362  vdwlem13  13363  vdwnnlem3  13367  ramtlecl  13370  ramtcl  13380  ram0  13392  ramz  13395  2expltfac  13428  prmlem0  13430  ressress  13528  wunress  13530  prdsdsval3  13709  imasvscafn  13764  mreiincl  13823  mreriincl  13825  mremre  13831  mrieqv2d  13866  mreexexlem2d  13872  mreexexd  13875  isacs2  13880  acsfiel  13881  acsfn1  13888  acsfn1c  13889  acsfn2  13890  iscatd  13900  catidd  13907  iscatd2  13908  catpropd  13937  invfun  13991  sscfn1  14019  sscfn2  14020  isssc  14022  issubc  14037  funcres2b  14096  funcres2  14097  wunfunc  14098  funcres2c  14100  ffthiso  14128  setcmon  14244  setcepi  14245  setciso  14248  funcsetcres2  14250  drsdirfi  14397  pltle  14420  pltne  14421  pleval2i  14423  pltn2lp  14428  pospo  14432  lubid  14441  joinle  14452  meetle  14459  istos  14466  mod1ile  14536  mod2ile  14537  lubun  14552  clatleglb  14555  poslubmo  14575  ipodrsima  14593  isacs3lem  14594  isacs4lem  14596  isacs5lem  14597  isacs5  14600  acsfiindd  14605  acsmapd  14606  acsmap2d  14607  mreclat  14615  latdisdlem  14617  pslem  14640  psssdm2  14649  spwex  14663  spwpr4  14665  letsr  14674  dirtr  14683  dirge  14684  mgmidmo  14695  mndpropd  14723  gsumval2a  14784  gsumwspan  14793  frmdss2  14810  isgrpinv  14857  grpinv11  14862  grpinvnz  14864  mulgneg2  14919  mulgnnass  14920  mulgnn0ass  14921  mulgass  14922  subginv  14953  issubg2  14961  issubg3  14962  ssnmz  14984  eqger  14992  eqgcpbl  14996  ghmmhmb  15019  ghmpreima  15029  conjnmz  15041  gaorber  15087  resscntz  15132  mndodcong  15182  oddvdsnn0  15184  odeq  15190  odf1o1  15208  odf1o2  15209  gexdvds  15220  gexcl3  15223  gex1  15227  pgpfi1  15231  sylow1lem3  15236  sylow1lem4  15237  pgpfi  15241  pgpssslw  15250  sylow2alem2  15254  sylow2a  15255  sylow2blem3  15258  sylow3lem2  15264  sylow3lem3  15265  lsmub1x  15282  lsmub2x  15283  lsmlub  15299  lsmdisj2  15316  subgdisjb  15327  lsmhash  15339  efgval  15351  efgsrel  15368  efgs1b  15370  efgsfo  15373  efgredlemc  15379  efgrelexlemb  15384  efgredeu  15386  efgcpbllemb  15389  frgpnabllem1  15486  frgpnabl  15488  cygabl  15502  prmcyg  15505  lt6abl  15506  cyggex2  15508  cyggexb  15510  gsumval3a  15514  gsumval3  15516  gsumzres  15519  gsumzcl  15520  gsumzf1o  15521  gsumzaddlem  15528  gsumconst  15534  gsumzmhm  15535  gsummulglem  15538  gsumzoppg  15541  gsum2d2  15550  gsumcom2  15551  dmdprd  15561  dprdfeq0  15582  dprdub  15585  subgdmdprd  15594  dprddisj2  15599  dprd2da  15602  dmdprdsplit2  15606  dmdprdpr  15609  ablfacrplem  15625  ablfacrp  15626  ablfac1eu  15633  pgpfac1lem2  15635  pgpfac1lem3a  15636  pgpfac1lem3  15637  pgpfac1lem5  15639  ablfac2  15649  rng1eq0  15704  mulgass2  15712  irredn0  15810  isdrng2  15847  drnginvrcl  15854  drnginvrn0  15855  drnginvrl  15856  drnginvrr  15857  drngmul0or  15858  isdrngd  15862  subrguss  15885  issubrg2  15890  issrngd  15951  lmodprop2d  16008  islssd  16014  lsssssubg  16036  lssacs  16045  lssats2  16078  lmodindp1  16092  lvecvs0or  16182  lssvs0or  16184  lspsneleq  16189  lspsncmp  16190  lspsneq  16196  lspsneu  16197  lspdisj  16199  lspdisj2  16201  lspfixed  16202  lspexch  16203  lspindp3  16210  lsmcv  16215  lspsncv0  16220  lsppratlem1  16221  lsppratlem6  16226  lspprat  16227  lbsextlem2  16233  lbsextlem4  16235  lidl1el  16291  drngnidl  16302  2idlcpbl  16307  lidldvgen  16328  isnzr2  16336  unitrrg  16355  fidomndrnglem  16368  fidomndrng  16369  assapropd  16388  psrbaglefi  16439  mplsubrglem  16504  mplbas2  16533  opsrtoslem2  16547  xrsdsreclblem  16746  zsssubrg  16759  cnsubrg  16761  zlpirlem1  16770  prmirredlem  16775  mulgrhm2  16790  domnchr  16815  znidomb  16844  znrrg  16848  cyggic  16855  ocvocv  16900  ocvin  16903  lsmcss  16921  cssmre  16922  pjfo  16944  pjcss  16945  obs2ss  16958  obslbs  16959  uniopn  16972  riinopn  16983  istps2OLD  16988  bastg  17033  tgcl  17036  tgdom  17045  en1top  17051  en2top  17052  bastop2  17061  indistopon  17067  ppttop  17073  pptbas  17074  epttop  17075  clsval2  17116  isopn3  17132  0ntr  17137  elcls3  17149  mretopd  17158  toponmre  17159  neiint  17170  neisspw  17173  0nnei  17178  neips  17179  opnneissb  17180  opnssneib  17181  neindisj  17183  opnnei  17186  tpnei  17187  neiuni  17188  neindisj2  17189  innei  17191  opnneiid  17192  neissex  17193  neiptoptop  17197  neiptopnei  17198  neiptopreu  17199  clslp  17214  restcld  17238  ssrest  17242  restfpw  17245  neitr  17246  restntr  17248  tgcn  17318  tgcnp  17319  iscnp4  17329  cnpnei  17330  cnntr  17341  cnss1  17342  cnss2  17343  cnrest2  17352  cnrest2r  17353  cnprest2  17356  cndis  17357  cnindis  17358  lmss  17364  hausnei  17394  hausnei2  17419  isnrm3  17425  lpcls  17430  lmmo  17446  lmfun  17447  dishaus  17448  ordthauslem  17449  cmpcovf  17456  fincmp  17458  cmpsublem  17464  cmpsub  17465  cmpcld  17467  hauscmplem  17471  bwth  17475  conndisj  17481  dfcon2  17484  cnconn  17487  iuncon  17493  uncon  17494  clscon  17495  2ndcctbss  17520  2ndcdisj  17521  2ndcomap  17523  2ndcsep  17524  dis2ndc  17525  1stcelcls  17526  1stccnp  17527  1stccn  17528  nlly2i  17541  llynlly  17542  restnlly  17547  restlly  17548  llyrest  17550  nllyrest  17551  llyidm  17553  lly1stc  17561  dislly  17562  kgentopon  17572  kgenss  17577  kgenidm  17581  llycmpkgen2  17584  1stckgen  17588  kgencn2  17591  kgencn3  17592  ptbasfi  17615  txcls  17638  ptpjopn  17646  ptclsg  17649  dfac14  17652  txcnp  17654  ptcnplem  17655  upxp  17657  txcn  17660  prdstopn  17662  txindis  17668  txdis1cn  17669  txnlly  17671  txcmplem1  17675  txcmpb  17678  txhaus  17681  txlm  17682  tx1stc  17684  txkgen  17686  xkohaus  17687  xkopt  17689  xkococnlem  17693  txcon  17723  qtoptop2  17733  idqtop  17740  qtopkgen  17744  basqtop  17745  qtopss  17749  qtopomap  17752  qtopcmap  17753  kqfvima  17764  isr0  17771  regr1lem  17773  hmeoopn  17800  hmeocld  17801  hmphdis  17830  ptcmpfi  17847  xkocnv  17848  qtophmeo  17851  nrmhaus  17860  fbssint  17872  fbfinnfr  17875  opnfbas  17876  filtop  17889  isfild  17892  fsubbas  17901  fbunfip  17903  ssfg  17906  fgss2  17908  fgcl  17912  fgabs  17913  filcon  17917  fbasrn  17918  filuni  17919  trfil2  17921  fgtr  17924  trfg  17925  csdfil  17928  uzrest  17931  ufilb  17940  ufilmax  17941  ufprim  17943  filssufilg  17945  ufileu  17953  filufint  17954  ufildom1  17960  cfinufil  17962  ufildr  17965  fin1aufil  17966  rnelfm  17987  fmfnfmlem1  17988  fmfnfmlem4  17991  fmfnfm  17992  fmco  17995  ufldom  17996  flimss2  18006  flimss1  18007  fbflim2  18011  flimclsi  18012  hausflimi  18014  hausflim  18015  flimcf  18016  flimsncls  18020  hauspwpwf1  18021  flffbas  18029  flftg  18030  cnpflf  18035  txflf  18040  isfcls  18043  fclsopn  18048  supnfcls  18054  fclsbas  18055  fclsss1  18056  fclsss2  18057  fclscf  18059  fclsfnflim  18061  flimfnfcls  18062  uffclsflim  18065  ufilcmp  18066  isfcf  18068  fcfnei  18069  fcfneii  18071  cnpfcf  18075  alexsublem  18077  alexsubb  18079  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  ptcmplem2  18086  ptcmplem3  18087  ptcmplem4  18088  cnextfun  18097  cnextf  18099  cnextcn  18100  tmdmulg  18124  tmdgsum2  18128  cldsubg  18142  ghmcnp  18146  tgphaus  18148  tgpt0  18150  divstgpopn  18151  haustsms2  18168  tgptsmscls  18181  tgptsmscld  18182  isust  18235  ustex2sym  18248  ustex3sym  18249  trust  18261  elutop  18265  utoptop  18266  restutop  18269  restutopopn  18270  ustuqtop4  18276  utop2nei  18282  utop3cls  18283  utopreg  18284  isucn2  18311  ucnima  18313  ucncn  18317  neipcfilu  18328  imasdsf1olem  18405  xblss2ps  18433  xblss2  18434  unirnblps  18451  unirnbl  18452  blin2  18461  blbas  18462  xmeter  18465  isxms2  18480  setsmstopn  18510  metss  18540  methaus  18552  metrest  18556  prdsxmslem2  18561  metustidOLD  18591  metustid  18592  metustsym  18594  metustexhalfOLD  18595  metustexhalf  18596  metustfbasOLD  18597  metustfbas  18598  metustOLD  18599  metust  18600  cfilucfilOLD  18601  cfilucfil  18602  blval2  18607  dscopn  18623  isngp2  18646  tngtopn  18693  nrgdomn  18709  nmoeq0  18772  qdensere  18806  xrsxmet  18842  xrsblre  18844  xrsmopn  18845  recld2  18847  zdis  18849  reperflem  18851  icccmplem2  18856  icccmplem3  18857  reconnlem1  18859  reconnlem2  18860  reconn  18861  opnreen  18864  rectbntr0  18865  xmetdcn2  18870  metds0  18882  metdsre  18885  metdseq0  18886  expcn  18904  rescncf  18929  cncfss  18931  cncfco  18939  icoopnst  18966  iocopnst  18967  iccpnfcnv  18971  xrhmeo  18973  icccvx  18977  cnheiborlem  18981  cnheibor  18982  phtpcer  19022  phtpc01  19023  pcohtpy  19047  pcopt  19049  pcopt2  19050  pi1cpbl  19071  clmmulg  19120  nmoleub2lem3  19125  nmhmcn  19130  cphsqrcl3  19152  tchcph  19196  clsocv  19206  cfil3i  19224  fgcfil  19226  cfilfcls  19229  iscau2  19232  caun0  19236  cmetcaulem  19243  iscmet3lem2  19247  iscmet3  19248  iscmet2  19249  cfilres  19251  caussi  19252  causs  19253  caubl  19262  iscmet3i  19266  lmcau  19267  cfilucfil4OLD  19275  cfilucfil4  19276  cncmet  19277  bcthlem2  19280  bcthlem5  19283  bcth  19284  cmetcusp1OLD  19307  cmetcusp1  19308  cmetcuspOLD  19309  cmetcusp  19310  minveclem4  19335  minveclem7  19338  pjth  19342  pmltpc  19349  ivthlem2  19351  ivthlem3  19352  ivthicc  19357  evthicc2  19359  ovolctb  19388  ovolunnul  19398  ovoliun  19403  ovoliunnul  19405  ovolscalem1  19411  ovolicc2lem4  19418  ovolicc2lem5  19419  ovolicopnf  19422  volun  19441  volfiniun  19443  iundisj  19444  voliunlem1  19446  voliunlem3  19448  volsup  19452  iunmbl2  19453  ioorcl2  19466  ioorf  19467  uniioombllem3  19479  dyadss  19488  dyaddisjlem  19489  dyadmax  19492  dyadmbl  19494  opnmbllem  19495  volsup2  19499  vitalilem2  19503  vitalilem3  19504  vitalilem4  19505  vitalilem5  19506  vitali  19507  ismbf  19524  ismbfcn  19525  mbfeqalem  19536  ismbf3d  19548  i1fd  19575  i1f0rn  19576  itg11  19585  i1faddlem  19587  i1fmullem  19588  itg1addlem2  19591  itg1addlem4  19593  itg10a  19604  itg1ge0a  19605  mbfi1fseqlem4  19612  mbfi1flimlem  19616  mbfmullem  19619  itg2const2  19635  itg2seq  19636  itg2split  19643  itg2addlem  19652  itg2add  19653  itg2gt0  19654  iblcnlem  19682  iblpos  19686  itgposval  19689  iblss  19698  itgle  19703  ibladdlem  19713  itgfsum  19720  iblabslem  19721  iblabs  19722  iblabsr  19723  iblmulc2  19724  itgabs  19728  itgsplitioo  19731  bddmulibl  19732  limcvallem  19760  limcdif  19765  limcnlp  19767  limcres  19775  limciun  19783  limcun  19784  perfdvf  19792  dvres  19800  dvidlem  19804  dvcnp2  19808  cpnord  19823  dvaddf  19830  dvmulf  19831  dvcof  19836  dvcj  19838  dvexp  19841  dvrec  19843  dvcnv  19863  dveflem  19865  rolle  19876  dvlip  19879  dvlip2  19881  c1liplem1  19882  dvgt0lem2  19889  dvge0  19892  dvne0  19897  lhop1lem  19899  dvcnvre  19905  dvfsumabs  19909  ftc1a  19923  ftc1cn  19929  itgsubst  19935  evlseu  19939  deg1ldgn  20018  coe1mul3  20024  deg1add  20028  ply1nzb  20047  ply1domn  20048  ply1divmo  20060  ply1divex  20061  q1peqb  20079  fta1g  20092  fta1b  20094  ig1peu  20096  ig1pdvds  20101  ply1lpir  20103  plyco0  20113  dgrlem  20150  coeid  20159  dgrle  20164  0dgrb  20167  coe1termlem  20178  dgreq0  20185  dgrcolem1  20193  dvnply2  20206  plydivlem4  20215  plydiveu  20217  plydivalg  20218  fta1  20227  vieta1  20231  plyexmo  20232  elqaa  20241  aannenlem1  20247  aalioulem2  20252  aalioulem4  20254  aalioulem5  20255  aalioulem6  20256  aaliou  20257  aaliou3lem2  20262  aaliou3lem7  20268  taylf  20279  dvtaylp  20288  ulmval  20298  ulmres  20306  ulmshftlem  20307  ulmuni  20310  ulmcaulem  20312  ulmcau  20313  ulmdv  20321  pserulm  20340  pserdv  20347  reeff1o  20365  pilem2  20370  pilem3  20371  cosord  20436  efif1olem4  20449  argimgt0  20509  logdivlt  20518  divlogrlim  20528  logno1  20529  dvloglem  20541  logf1o2  20543  efopnlem2  20550  cxpge0  20576  cxpsqr  20596  cxpeq  20643  loglesqr  20644  ang180lem2  20654  logreclem  20662  angpined  20673  angpieqvd  20674  dcubic  20688  atansssdm  20775  xrlimcnp  20809  efrlim  20810  scvxcvx  20826  jensen  20829  amgm  20831  fsumharmonic  20852  wilthlem2  20854  basellem2  20866  basellem3  20867  basellem4  20868  ppisval  20888  ppisval2  20889  isppw  20899  isppw2  20900  ppieq0  20961  mumullem2  20965  sqff1o  20967  fsumdvdsdiaglem  20970  fsumdvdscom  20972  dvdsflsumcom  20975  fsumfldivdiaglem  20976  chpeq0  20994  chteq0  20995  chtublem  20997  chtub  20998  fsumvma  20999  chpchtsum  21005  perfectlem1  21015  perfectlem2  21016  perfect  21017  dchrfi  21041  dchrptlem1  21050  dchrpt  21053  bposlem3  21072  lgsdir2lem4  21112  lgsdir2lem5  21113  lgsne0  21119  lgsdchrval  21133  lgsquadlem2  21141  lgsquadlem3  21142  m1lgs  21148  2sqlem6  21155  2sqlem8a  21157  2sqlem9  21159  2sqlem10  21160  2sqb  21164  chtppilimlem2  21170  chebbnd2  21173  vmadivsumb  21179  rplogsumlem2  21181  dchrisumlema  21184  dchrisumlem2  21186  dchrisumlem3  21187  dchrisum0fno1  21207  dchrisum0re  21209  dchrisum0lem1  21212  dirith2  21224  vmalogdivsum2  21234  vmalogdivsum  21235  2vmadivsumlem  21236  selbergb  21245  selberg2b  21248  selberg3lem1  21253  selberg3lem2  21254  selberg3  21255  selberg4lem1  21256  selberg4  21257  pntrmax  21260  pntrlog2bndlem2  21274  pntrlog2bndlem4  21276  pntpbnd1  21282  pntibnd  21289  ostth3  21334  ostth  21335  umgraex  21360  isusgra0  21378  ausisusgra  21382  usgra1  21395  usgraedgprv  21398  usgraedgrnv  21399  usgranloopv  21400  usgranloop  21401  usgranloop0  21402  usgra2edg  21404  usgrarnedg  21406  usgraedg4  21408  usgra1v  21411  usgrafisindb0  21424  usgrafisindb1  21425  usgrares1  21426  usgrafilem2  21428  usgrafisinds  21429  nbgraop  21438  nbgraop1  21439  nbusgra  21442  nbgra0nb  21443  nbgraeledg  21444  nbgraisvtx  21445  nbgranself  21448  nbgrassovt  21449  nbgraf1olem1  21453  nbgraf1olem5  21457  nb3graprlem1  21462  nbcusgra  21474  cusgrares  21483  cusgrasizeinds  21487  cusgrasize2inds  21488  cusgrafilem2  21491  cusgrafilem3  21492  cusgrafi  21493  sizeusglecusglem1  21495  sizeusglecusglem2  21496  sizeusglecusg  21497  uvtxnbgra  21504  uvtxnm1nbgra  21505  uvtxnbgravtx  21506  0wlkon  21549  0trlon  21550  2trllemE  21555  usgrnloop  21565  is2wlk  21567  spthispth  21575  0pthon  21581  0pthonv  21583  spthonepeq  21589  constr1trl  21590  constr2wlk  21600  constr2trl  21601  constr2spth  21602  constr2pth  21603  2pthon  21604  redwlklem  21607  redwlk  21608  wlkdvspthlem  21609  wlkdvspth  21610  cyclnspth  21620  cyclispthon  21622  fargshiftfv  21624  fargshiftf1  21626  fargshiftfva  21628  usgrcyclnl1  21629  usgrcyclnl2  21630  3cycl3dv  21631  nvnencycllem  21632  constr3trllem1  21639  constr3trllem2  21640  constr3trllem5  21643  constr3trl  21648  constr3pth  21649  constr3cyclp  21651  4cycl4dv  21656  1conngra  21664  cusconngra  21665  vdgrf  21671  vdusgraval  21680  hashnbgravdg  21684  iseupa  21689  eupatrl  21692  eupath2lem3  21703  ex-natded5.3  21717  lpni  21769  isgrpo  21786  grpoidinvlem3  21796  grpoideu  21799  grpoinvf  21830  grponnncan2  21844  gxnn0neg  21853  gxnn0suc  21854  gxcl  21855  gxcom  21859  gxinv  21860  gxid  21863  gxnn0add  21864  gxadd  21865  gxnn0mul  21867  gxmul  21868  isabloda  21889  opidon  21912  ghomid  21955  ghgrp  21958  ghsubgolem  21960  rngmgmbs4  22007  rngoidmlem  22013  rngosn4  22017  rngoueqz  22020  zerdivemp1  22024  rngoridfz  22025  isnvi  22094  nvmul0or  22135  nvz  22160  nmcvcn  22193  sspmval  22234  nmoub3i  22276  nmlno0lem  22296  nmlnoubi  22299  lnon0  22301  blocnilem  22307  dipsubdir  22351  ubthlem1  22374  ubthlem3  22376  minvecolem4  22384  minvecolem7  22387  htthlem  22422  hvmul0or  22529  hiidge0  22602  his6  22603  hial0  22606  hial02  22607  normgt0  22631  normpyc  22650  isch3  22746  ocsh  22787  occon  22791  ocorth  22795  chocunii  22805  occl  22808  shsel3  22819  shsel1  22825  shlessi  22881  shlej1i  22882  shmodsi  22893  shlub  22918  chssoc  23000  h1de2bi  23058  h1de2ctlem  23059  spansneleq  23074  spansnss2  23079  spanpr  23084  h1datomi  23085  cm2j  23124  chscl  23145  sumspansn  23153  spansnm0i  23154  spansncvi  23156  pjjsi  23204  pjsumi  23214  hon0  23298  hoaddsub  23321  nmopub2tALT  23414  nmfnleub2  23431  hmopadj2  23446  nmlnop0iALT  23500  nmopun  23519  nmophmi  23536  lnopcnbd  23541  lnfncnbd  23562  riesz3i  23567  riesz1  23570  nmopadjlem  23594  nmoptrii  23599  nmopcoi  23600  nmopcoadji  23606  branmfn  23610  rnbra  23612  kbass6  23626  leopadd  23637  pjnmopi  23653  pjnormssi  23673  sticl  23720  hst1h  23732  hstles  23736  stge1i  23743  stlei  23745  staddi  23751  stadd3i  23753  strlem1  23755  stcltrlem1  23781  cvcon3  23789  cvnbtwn  23791  mdbr3  23802  mdbr4  23803  dmdmd  23805  dmdbr3  23810  dmdbr4  23811  dmdbr5  23813  mdsl0  23815  mdsl2bi  23828  mdslmd1i  23834  mdslmd3i  23837  csmdsymi  23839  mdexchi  23840  atsseq  23852  superpos  23859  hatomistici  23867  cvbr4i  23872  atcv0eq  23884  atcv1  23885  atexch  23886  atomli  23887  atoml2i  23888  atordi  23889  atcvatlem  23890  atcvati  23891  atcvat2i  23892  chirredlem1  23895  chirredlem4  23898  chirredi  23899  atcvat3i  23901  atcvat4i  23902  atabsi  23906  mdsymlem4  23911  mdsymlem5  23912  mdsymlem6  23913  sumdmdlem  23923  dmdbr5ati  23927  cdj1i  23938  cdj3lem1  23939  cdj3i  23946  addltmulALT  23951  adantl3r  23958  adantl4r  23959  adantl5r  23960  adantl6r  23961  eqvincg  23963  abrexss  23995  rabss3d  23997  ifeqeqx  24003  ifbieq12d2  24004  elim2ifim  24008  iundifdifd  24014  disjpreima  24028  dfimafnf  24045  abfmpeld  24068  abfmpel  24069  feqmptdf  24077  fcomptf  24079  offval2f  24082  funcnvmptOLD  24084  funcnvmpt  24085  rnmpt2ss  24088  isoun  24091  disjdsct  24092  xaddeq0  24121  xrofsup  24128  snunioc  24139  eliccelico  24142  elicoelioo  24143  iocinif  24146  ssnnssfz  24150  iundisjfi  24154  ishashinf  24161  xrecex  24168  xrge0npcan  24218  ofldaddlt  24243  subofld  24247  kerf1hrm  24264  reofld  24282  pstmfval  24293  unitdivcld  24301  sqsscirc1  24308  cnre2csqlem  24310  cnre2csqima  24311  tpr2rico  24312  fmcncfil  24319  xrge0iifcnv  24321  xrge0iifiso  24323  lmxrge0  24339  lmdvg  24340  qqhval2lem  24367  qqhval2  24368  rrhre  24389  indf1ofs  24425  esumeq12dvaf  24430  esumel  24444  esumf1o  24447  esumc  24448  esummono  24452  esumlef  24456  esumcst  24457  esumfsup  24462  esumpinfval  24465  esumpinfsum  24469  esumpcvgval  24470  esumcvg  24478  sigaclcuni  24503  dmvlsiga  24514  sigaclci  24517  sigainb  24521  insiga  24522  cldssbrsiga  24543  ismeas  24555  measxun2  24566  measssd  24571  measiun  24574  measinb  24577  measdivcstOLD  24580  measdivcst  24581  cntmeas  24582  voliune  24587  volfiniune  24588  volmeas  24589  imambfm  24614  dya2icobrsiga  24628  dya2iocnrect  24633  dya2iocuni  24635  dya2iocucvr  24636  sxbrsigalem2  24638  sibfof  24656  probun  24679  rrvsum  24714  dstrvprob  24731  dstfrvunirn  24734  ballotlemfp1  24751  ballotlemfc0  24752  ballotlemfcc  24753  ballotlem4  24758  ballotlemirc  24791  ballotlem7  24795  eldmgm  24808  lgamgulmlem2  24816  lgamgulmlem6  24820  lgambdd  24823  lgamucov  24824  lgamcvg2  24841  derangsn  24858  derangenlem  24859  subfacp1lem3  24870  subfacp1lem5  24872  subfacp1lem6  24873  erdszelem8  24886  erdszelem9  24887  erdsze2lem1  24891  erdsze2lem2  24892  txscon  24930  rescon  24935  rellyscon  24940  cvmscld  24962  cvmsss2  24963  cvmfolem  24968  cvmliftmolem1  24970  cvmliftmo  24973  cvmliftlem7  24980  cvmliftlem10  24983  cvmliftlem15  24987  cvmlift2lem10  25001  cvmlift2lem11  25002  cvmlift2lem12  25003  cvmlift3lem7  25014  ghomcl  25105  ghomf1olem  25107  lediv2aALT  25119  relexpindlem  25141  pm2.61iine  25188  dedekind  25189  dedekindle  25190  mulge0b  25193  ntrivcvg  25227  ntrivcvgfvn0  25229  prodrblem  25257  fprodcvg  25258  prodmolem2a  25262  prodmo  25264  zprod  25265  prod1  25272  fprodf1o  25274  prodss  25275  fprodss  25276  fprodsplit  25291  fprod2dlem  25306  faclim  25367  faclim2  25369  br8  25381  br6  25382  br4  25383  funpsstri  25391  fundmpss  25392  funsseq  25395  fprb  25399  dfon2lem3  25414  dfon2lem6  25417  dfon2lem8  25419  predpo  25461  setlikess  25472  preddowncl  25473  wfi  25484  trpredtr  25510  trpredelss  25512  trpredrec  25518  frmin  25519  frind  25520  soseq  25531  wfr3g  25539  wfrlem10  25549  wfrlem12  25551  wfrlem14  25553  wzel  25577  frr3g  25583  frrlem5e  25592  frrlem11  25596  sltval2  25613  noreson  25617  sltres  25621  sltsolem1  25625  sltasym  25629  nodenselem3  25640  nodenselem5  25642  nodenselem7  25644  nodenselem8  25645  nocvxminlem  25647  nobndup  25657  nobnddown  25658  nofulllem5  25663  elfuns  25762  brbtwn2  25846  axsegcon  25868  ax5seglem5  25874  axpaschlem  25881  axpasch  25882  axlowdimlem14  25896  axlowdimlem16  25898  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  axcontlem8  25912  axcontlem9  25913  axcontlem10  25914  axcontlem12  25916  cgrcomim  25925  cgrtr  25928  cgrtr3  25930  cgrdegen  25940  cgrextend  25944  segconeq  25946  segconeu  25947  btwnouttr2  25958  btwnouttr  25960  trisegint  25964  funtransport  25967  ifscgr  25980  cgrsub  25981  cgrxfr  25991  btwnxfr  25992  colinearxfr  26011  lineext  26012  brofs2  26013  brifs2  26014  linecgr  26017  idinside  26020  btwnconn1lem7  26029  btwnconn1lem11  26033  btwnconn1lem12  26034  btwnconn1lem14  26036  btwnconn1  26037  btwnconn2  26038  btwnconn3  26039  midofsegid  26040  brsegle  26044  brsegle2  26045  btwnsegle  26053  colinbtwnle  26054  btwnoutside  26061  outsideofeq  26066  outsideofeu  26067  outsidele  26068  funray  26076  lineunray  26083  lineelsb2  26084  linethru  26089  hilbert1.2  26091  lineintmo  26093  ontopbas  26180  onpsstopbas  26182  ordtop  26188  onsuct0  26193  onsucsuccmpi  26195  ordcmp  26199  onint1  26201  ee7.2aOLD  26213  supadd  26240  ltflcei  26241  lxflflp1  26243  opnmbllem0  26244  mblfinlem1  26245  mblfinlem3  26247  ismblfin  26249  ovoliunnfl  26250  voliunnfl  26252  volsupnfl  26253  mbfresfi  26255  cnambfre  26257  itg2addnclem  26258  itg2addnclem2  26259  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  ibladdnclem  26263  iblabsnclem  26270  iblabsnc  26271  iblmulc2nc  26272  itgabsnc  26276  bddiblnc  26277  ftc1cnnc  26281  ftc1anclem5  26286  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  dvreasin  26292  dvreacos  26293  areacirclem1  26294  areacirclem4  26297  areacirclem5  26298  areacirc  26299  exp5g  26306  exp56  26310  exp58  26311  exp510  26312  exp511  26313  exp512  26314  elicc3  26322  finminlem  26323  opnrebl2  26326  nn0prpwlem  26327  nn0prpw  26328  opnbnd  26330  cldbnd  26331  opnregcld  26335  cldregopn  26336  ivthALT  26340  fneint  26359  reftr  26371  topfneec  26373  fnessref  26375  refssfne  26376  locfincmp  26386  locfincf  26388  comppfsc  26389  neibastop1  26390  neibastop2  26392  fnemeet2  26398  fnejoin2  26400  fgmin  26401  tailfb  26408  syldanl  26415  unirep  26416  brabg2  26419  upixp  26433  indexdom  26438  frinfm  26439  filbcmb  26444  fzmul  26446  fzadd2  26447  sdclem2  26448  sdclem1  26449  fdc  26451  fdc1  26452  seqpo  26453  incsequz  26454  incsequz2  26455  nnubfi  26456  nninfnub  26457  metf1o  26463  mettrifi  26465  istotbnd3  26482  sstotbnd2  26485  sstotbnd3  26487  isbndx  26493  isbnd2  26494  isbnd3  26495  bndss  26497  ssbnd  26499  equivbnd2  26503  prdstotbnd  26505  cntotbnd  26507  cnpwstotbnd  26508  ismtycnv  26513  ismtyima  26514  ismtyhmeo  26516  heibor1lem  26520  heiborlem1  26522  heiborlem3  26524  heiborlem8  26529  heibor  26532  bfp  26535  rrncms  26544  ghomco  26560  grpokerinj  26562  rngosubdi  26571  rngosubdir  26572  zerdivemp1x  26573  rngohomco  26592  rngoisocnv  26599  riscer  26606  iscringd  26611  crngohomfo  26618  1idl  26638  divrngidl  26640  intidl  26641  unichnidl  26643  keridl  26644  ispridl2  26650  igenval2  26678  prnc  26679  ispridlc  26682  isdmn3  26686  jca3  26695  prtlem90  26708  prtlem10  26716  prtlem17  26727  prtlem19  26729  prter2  26732  prter3  26733  ralxpmap  26744  elrfi  26750  elrfirn2  26752  ismrc  26757  isnacs3  26766  mzpindd  26805  mzpcompact2lem  26810  fzsplit1nn0  26814  diophrw  26819  eldioph2  26822  eldioph2b  26823  lzunuz  26828  diophin  26833  eldiophss  26835  diophrex  26836  eq0rabdioph  26837  eqrabdioph  26838  rexrabdioph  26856  rexzrexnn0  26866  eluzrabdioph  26868  eldioph4b  26874  fphpd  26879  fphpdo  26880  fiphp3d  26882  rencldnfilem  26883  icodiamlt  26885  irrapxlem2  26888  irrapxlem3  26889  irrapxlem4  26890  irrapxlem5  26891  irrapxlem6  26892  pellexlem3  26896  pellexlem5  26898  pellexlem6  26899  pellex  26900  pell1234qrne0  26918  pell1234qrreccl  26919  pell1234qrmulcl  26920  pell14qrgt0  26924  pell1234qrdich  26926  elpell14qr2  26927  pell14qrmulcl  26928  pell14qrreccl  26929  pell14qrdich  26934  pell1qrge1  26935  elpell1qr2  26937  pell1qrgap  26939  pellqrex  26944  pellfundre  26946  pellfundge  26947  pellfundlb  26949  pellfundglb  26950  pellfundex  26951  pellfund14b  26964  qirropth  26973  rmxycomplete  26982  monotuz  27006  monotoddzzfi  27007  2nn0ind  27010  rpexpmord  27013  congabseq  27041  acongtr  27045  dvdsacongtr  27051  bezoutr1  27053  dvdsleabs2  27057  jm2.18  27061  jm2.19lem4  27065  jm2.19  27066  jm2.25  27072  jm2.26a  27073  jm2.26lem3  27074  jm2.27  27081  rmydioph  27087  setindtr  27097  dford3lem2  27100  rpnnen3  27105  harinf  27107  ttac  27109  limsuc2  27117  wepwsolem  27118  dnnumch1  27121  dnnumch3  27124  fnwe2lem2  27128  fnwe2  27130  aomclem6  27136  kelac1  27140  dfac21  27143  kercvrlsm  27160  pwssplit4  27170  uvcf1  27220  frlmsslsp  27227  frlmup4  27232  unxpwdom3  27235  isnumbasgrplem1  27245  lindfmm  27276  lsslindf  27279  islinds3  27283  islinds4  27284  lmiclbs  27286  lmisfree  27291  lnr2i  27299  hbtlem5  27311  dgrnznn  27319  dgraalem  27329  dgraa0p  27333  mpaaeu  27334  rngunsnply  27357  f1otrspeq  27369  pmtrmvd  27377  symggen  27390  psgnunilem2  27397  psgnunilem4  27399  psgneu  27408  acsfn1p  27486  proot1hash  27498  dvconstbi  27530  expgrowth  27531  pm14.24  27611  ralbidar  27626  rexbidar  27627  ipo0  27630  ifr0  27631  ordpss  27632  fnchoice  27678  refsumcn  27679  rfcnnnub  27685  fmptdf  27696  infrglb  27700  m1expeven  27703  climsuse  27712  climreeq  27717  itgsinexplem1  27726  stoweidlem5  27732  stoweidlem7  27734  stoweidlem14  27741  stoweidlem16  27743  stoweidlem18  27745  stoweidlem21  27748  stoweidlem26  27753  stoweidlem27  27754  stoweidlem28  27755  stoweidlem29  27756  stoweidlem31  27758  stoweidlem34  27761  stoweidlem35  27762  stoweidlem36  27763  stoweidlem39  27766  stoweidlem41  27768  stoweidlem42  27769  stoweidlem43  27770  stoweidlem44  27771  stoweidlem45  27772  stoweidlem46  27773  stoweidlem48  27775  stoweidlem49  27776  stoweidlem50  27777  stoweidlem51  27778  stoweidlem52  27779  stoweidlem53  27780  stoweidlem55  27782  stoweidlem56  27783  stoweidlem57  27784  stoweidlem59  27786  stoweidlem60  27787  stoweidlem61  27788  stoweidlem62  27789  wallispilem3  27794  wallispilem4  27795  wallispi2lem1  27798  wallispi2lem2  27799  stirlinglem5  27805  sigarcol  27832  rexrsb  27925  2reurex  27937  2reu1  27942  eu2ndop1stv  27958  funressnfv  27970  afv0nbfvbi  27993  afveu  27995  funbrafv  28000  funbrafv2b  28001  dfafn5a  28002  dfaimafn  28007  afvres  28014  tz6.12-afv  28015  afvco2  28018  rlimdmafv  28019  ndmaovdistr  28049  otsndisj  28067  otiunsndisj  28068  otiunsndisjX  28069  2f1fvneq  28079  rnfdmpr  28085  imarnf1pr  28086  resfnfinfin  28088  2leaddle2  28094  lesubnn0  28098  uzletr  28105  ssfz12  28106  elfz2z  28107  elfzelfzelfz  28111  elfz0fzfz0  28116  2elfz2melfz  28119  fz0fzelfz0  28120  ubmelfzo  28128  ubmelm1fzo  28129  fzo1fzo0n0  28130  ssfzo12  28132  elfzonelfzo  28134  fzonmapblen  28136  subsubelfzo0  28137  fzofzim  28138  el2fzo  28140  fzoopth  28141  2ffzoeq  28142  flltdivnn0lt  28149  ltdifltdiv  28150  modifeq2int  28163  hashimarn  28165  hashimarni  28166  wrdlenge2n0  28178  ccatsymb  28181  swrdltnd  28183  swrdnd  28184  swrd0  28185  swrdvalodmlem1  28189  swrdvalodm2  28190  swrdvalodm  28191  swrd0swrd  28199  swrdswrdlem  28200  swrdswrd  28201  swrdswrd0  28203  swrdccatin1  28207  swrdccatin12lem2  28209  swrdccatin12lem3a  28210  swrdccatin12lem3b  28211  swrdccatin2  28212  swrdccatin12lem3  28214  swrdccatin12lem4  28215  swrdccatin12  28216  swrdccat3  28217  swrdccat  28218  swrdccat3a  28219  swrdccat3blem  28220  swrdccat3b  28221  swrdccatin12d  28224  modprm0  28230  cshwoor  28239  cshwidx  28244  cshwidxmod  28245  2cshw1lem1  28250  2cshw1lem2  28251  2cshw1  28253  2cshw2lem1  28254  2cshw2lem2  28255  2cshw2lem3  28256  2cshw2  28257  2cshw  28258  2cshwmod  28259  lswrdn0  28262  cshweqdif2  28272  cshweqdif2s  28273  cshweqrep  28276  cshw1  28277  cshw1v  28278  cshwsame  28279  cshwsame0  28280  cshwssizelem1a  28281  cshwssizelem1  28282  cshwssizelem2  28283  cshwssizelem4a  28285  cshwsdisj  28287  cshwsiun  28288  cshwssizesame  28290  cshwssizensame  28291  cshwsexa  28293  uhgraedgrnv  28294  iswlkg  28302  usg2wlkeq  28306  usgra2pthspth  28307  usgra2wlkspthlem1  28308  usgra2wlkspthlem2  28309  usgra2wlkspth  28310  usgra2pth  28313  usgra2adedgspthlem1  28315  usgra2adedgspthlem2  28316  usgra2adedgspth  28317  usgra2adedgwlk  28318  usgra2adedgwlkon  28319  usgra2adedglem1  28320  usg2wlkon  28322  el2wlkonot  28338  el2spthonot  28339  el2spthonot0  28340  el2wlkonotot0  28341  2wlkonot3v  28344  2spthonot3v  28345  el2wlksoton  28347  el2spthsoton  28348  el2wlksotot  28351  usg2wotspth  28353  2pthwlkonot  28354  usg2spthonot  28357  usg2spthonot0  28358  usgfiregdegfi  28363  usgrauvtxvd  28365  0egra0rgra  28377  cusgraisrusgra  28379  frgraunss  28387  frisusgranb  28389  frgra1v  28390  frgra3vlem2  28393  frgra3v  28394  3vfriswmgralem  28396  3vfriswmgra  28397  1to2vfriswmgra  28398  1to3vfriswmgra  28399  2pthfrgrarn2  28402  2pthfrgra  28403  3cyclfrgrarn1  28404  3cyclfrgrarn  28405  3cyclfrgra  28407  4cycl2vnunb  28409  n4cyclfrgra  28410  4cyclusnfrgra  28411  frgranbnb  28412  vdn0frgrav2  28416  vdgn0frgrav2  28417  vdn1frgrav2  28418  vdgn1frgrav2  28419  vdgfrgragt2  28420  frgrancvvdeqlem3  28423  frgrancvvdeqlem4  28424  frgrancvvdeqlemB  28429  frgrancvvdeqlemC  28430  frgrancvvdeqlem9  28432  frgrawopreglem4  28438  frgrawopreglem5  28439  frgrawopreg  28440  frgraeu  28445  frg2wot1  28448  frg2woteqm  28450  frg2woteq  28451  2spotdisj  28452  2spotiundisj  28453  usg2spot2nb  28456  usgreghash2spotv  28457  usgreg2spot  28458  2spotmdisj  28459  usgreghash2spot  28460  frgregordn0  28461  ad4ant13  28540  ad4ant14  28541  ad4ant23  28545  ad4ant24  28546  ad5ant13  28549  ad5ant14  28550  ad5ant15  28551  ad5ant23  28552  ad5ant24  28553  ad5ant25  28554  ee222  28586  tratrb  28622  ordelordALT  28624  truniALT  28628  ggen31  28633  onfrALTlem2  28634  ex3  28660  int2  28709  e222  28739  e22an  28775  ee22an  28776  e11an  28792  ee11an  28793  e01an  28795  e10an  28798  e02an  28801  ee02an  28802  eel12131  28823  eel32131  28826  eel2122old  28830  eel11111  28837  e12an  28839  e20an  28842  ee20an  28843  e21an  28845  ee21an  28846  e33an  28849  ee33an  28850  e03an  28856  ee03an  28857  e30an  28860  ee30an  28861  e13an  28863  ee13an  28864  e31an  28867  e23an  28870  e32an  28874  uun0.1  28892  bitr3VD  28963  3orbi123VD  28964  tratrbVD  28975  ordelordALTVD  28981  trsbcVD  28991  truniALTVD  28992  sbcssVD  28997  csbingVD  28998  onfrALTlem2VD  29003  csbxpgVD  29008  csbunigVD  29012  csbfv12gALTVD  29013  sspwimp  29032  sspwimpcf  29034  suctrALTcf  29036  suctrALT3  29038  sspwimpALT  29039  sspwimpALT2  29042  a9e2ndeqALT  29045  chordthmALT  29047  iunconlem2  29049  sineq0ALT  29051  bnj1109  29159  bnj149  29248  bnj517  29258  bnj518  29259  bnj605  29280  bnj594  29285  bnj580  29286  bnj852  29294  bnj849  29298  bnj964  29316  bnj1018  29335  bnj1174  29374  bnj1175  29375  bnj1388  29404  bnj1398  29405  bnj1417  29412  bnj1489  29427  dvelimhvAUX7  29494  spimedNEW7  29512  equveliNEW7  29530  ax11v2NEW7  29532  nfsb4twAUX7  29578  sbequiNEW7  29581  sbcomwAUX7  29590  sbal1NEW7  29617  sbiedvNEW7  29634  dvelimALTNEW7  29638  sbcom2NEW7  29646  ax7w15AUX7  29670  dvelimhOLD7  29715  nfald2OLD7  29719  cbvaldvaOLD7  29738  cbvexdvaOLD7  29739  nfsb4tOLD7  29747  nfsb4tw2AUXOLD7  29748  dvelimdfOLD7  29753  sbcomOLD7  29757  lubunNEW  29773  lshpnel  29783  lshpdisj  29787  lshpinN  29789  lsatspn0  29800  lsatcmp  29803  lsatcmp2  29804  lssats  29812  lpssat  29813  lssatle  29815  lssat  29816  islshpat  29817  lcvntr  29826  lsatcv0  29831  lsatcveq0  29832  lsat0cv  29833  lsatcv0eq  29847  lsatcv1  29848  islshpcv  29853  lkr0f  29894  eqlkr3  29901  lkrlsp  29902  lkrshp  29905  lkrshp4  29908  lshpkrlem1  29910  lshpkr  29917  lshpset2N  29919  lfl1dim  29921  lfl1dim2N  29922  lkrpssN  29963  lkrin  29964  lkrss2N  29969  lub0N  29989  omllaw3  30045  cmtcomlemN  30048  cmtbr3N  30054  cmtbr4N  30055  ncvr1  30072  cvrnbtwn2  30075  cvrcon3b  30077  cvrnbtwn4  30079  cvrnrefN  30082  cvrcmp  30083  isatliN  30102  atcvreq0  30114  atnle  30117  atlatmstc  30119  atlatle  30120  atlrelat1  30121  cvlexchb1  30130  cvlatexch3  30138  cvlcvr1  30139  cvlsupr2  30143  hlsupr2  30186  hlrelat2  30202  exatleN  30203  intnatN  30206  cvrval3  30212  cvrval4N  30213  cvrval5  30214  cvrexchlem  30218  cvrat  30221  ltltncvr  30222  ltcvrntr  30223  cvrntr  30224  lnnat  30226  atcvrj0  30227  cvrat2  30228  atcvrj2b  30231  atltcvr  30234  atexchcvrN  30239  cvrat3  30241  cvrat4  30242  atbtwn  30245  athgt  30255  ps-2  30277  islln2a  30316  2atnelpln  30343  islpln2a  30347  lplnllnneN  30355  2llnjaN  30365  2llnjN  30366  lvoli2  30380  3atnelvolN  30385  islvol2aN  30391  lplncvrlvol  30415  2lplnja  30418  dalem1  30458  dalem20  30492  dalem25  30497  psubspi  30546  snatpsubN  30549  pointpsubN  30550  linepsubN  30551  pmaple  30560  pmapglbx  30568  pmapglb2N  30570  pmapglb2xN  30571  lncvrelatN  30580  lncmp  30582  elpaddn0  30599  paddss1  30616  paddss2  30617  paddss12  30618  paddasslem3  30621  paddasslem5  30623  paddasslem14  30632  paddssw2  30643  pmod1i  30647  pmapjat1  30652  llnexchb2lem  30667  llnexchb2  30668  pclclN  30690  pclfinN  30699  2polssN  30714  2polcon4bN  30717  ispsubcl2N  30746  pclfinclN  30749  poml4N  30752  lhpexle1lem  30806  lhpm0atN  30828  lhp2atne  30833  lhp2at0ne  30835  lhpat3  30845  4atexlemunv  30865  4atexlemntlpq  30867  4atexlemex2  30870  4atexlemcnd  30871  lautcvr  30891  lauteq  30894  ltrncnvnid  30926  ltrnid  30934  idltrn  30949  trlator0  30970  trlatn0  30971  ltrnnidn  30973  ltrnideq  30974  trlnidatb  30976  trlnid  30978  ltrnatlw  30982  trlval4  30987  cdleme0moN  31024  cdleme3b  31028  cdleme11c  31060  cdleme11l  31068  cdleme16b  31078  cdleme18b  31091  cdlemednpq  31098  cdleme20j  31117  cdleme21ct  31128  cdleme21i  31134  cdleme22b  31140  cdleme22cN  31141  cdleme25dN  31155  cdleme27a  31166  cdlemefr29exN  31201  cdlemefs32sn1aw  31213  cdleme43fsv1snlem  31219  cdleme41sn3a  31232  cdleme35h2  31256  cdleme38n  31263  cdleme40m  31266  cdleme40n  31267  cdleme50rnlem  31343  cdleme50ldil  31347  cdlemftr3  31364  cdlemg1a  31369  cdlemg1cex  31387  cdlemg4c  31411  cdlemg6c  31419  cdlemg8c  31428  cdlemg11a  31436  cdlemg11b  31441  cdlemg12e  31446  cdlemg18a  31477  cdlemg33  31510  trlcoat  31522  cdlemg42  31528  cdlemh  31616  tendoid0  31624  tendo1ne0  31627  cdlemk33N  31708  cdlemk34  31709  cdleml9  31783  dva1dim  31784  erng1lem  31786  erngdvlem4-rN  31798  diaelrnN  31845  diaintclN  31858  diasslssN  31859  dia2dimlem1  31864  cdlemm10N  31918  diarnN  31929  dibintclN  31967  dicvalrelN  31985  dicssdvh  31986  dihvalcqpre  32035  dihopelvalcpre  32048  dihsslss  32076  dihvalrel  32079  dih1  32086  dihglblem5apreN  32091  dihglbcpreN  32100  dihmeetlem13N  32119  dihlspsnssN  32132  dihlspsnat  32133  dihatexv  32138  dihglblem6  32140  dihglb2  32142  dihintcl  32144  dochss  32165  dochsat  32183  dochlkr  32185  dochkrshp  32186  dochkrshp4  32189  djhlsmcl  32214  dihjatcclem4  32221  dihjat1lem  32228  dihjat2  32231  dochsatshp  32251  dochexmidlem5  32264  dochexmidlem8  32267  dochkr1  32278  dochkr1OLDN  32279  islpoldN  32284  lcfl6  32300  lcfl7N  32301  lcfl8  32302  lcfl8b  32304  lclkrlem2e  32311  lcfrvalsnN  32341  lcfrlem5  32346  lcfrlem6  32347  lcfrlem9  32350  lcfrlem32  32374  mapdval2N  32430  mapdordlem1a  32434  mapdordlem2  32437  mapdrvallem2  32445  mapd1o  32448  mapd0  32465  mapdn0  32469  mapdpglem2  32473  mapdpglem11  32482  mapdpglem16  32487  mapdheq2  32529  mapdh8b  32580  mapdh9a  32590  mapdh9aOLDN  32591  hdmaprnlem3eN  32661  hdmaprnlem10N  32662  hdmaprnlem16N  32665  hdmaprnN  32667  hgmaprnN  32704  hgmap11  32705  hdmapip0  32718  hlhillcs  32761  hlhilhillem  32763
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator