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

Theorem breq2d 4656
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
breq2d (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Proof of Theorem breq2d
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq2 4648 . 2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481   class class class wbr 4644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645
This theorem is referenced by:  breqtrd  4670  sbcbr1g  4700  pofun  5041  csbfv12  6218  isorel  6561  soisores  6562  soisoi  6563  isocnv  6565  isotr  6571  f1owe  6588  caovordig  6824  caovordg  6826  caovord  6830  f1oweALT  7137  frxp  7272  xporderlem  7273  fnwelem  7277  difsnen  8027  domdifsn  8028  unfilem3  8211  domunfican  8218  marypha1lem  8324  marypha1  8325  inflb  8380  wemapwe  8579  oef1o  8580  r1sdom  8622  sdomsdomcardi  8782  alephordi  8882  pwcdadom  9023  sornom  9084  axdclem  9326  pwcfsdom  9390  elgch  9429  winalim2  9503  rankcf  9584  inatsk  9585  pinq  9734  nqereu  9736  ltaddnq  9781  ltrnq  9786  archnq  9787  addclprlem1  9823  mulclprlem  9826  1idpr  9836  ltaprlem  9851  ltapr  9852  prlem936  9854  ltasr  9906  mulgt0sr  9911  sqgt0sr  9912  map2psrpr  9916  axpre-ltadd  9973  axpre-mulgt0  9974  axpre-sup  9975  ltaddneg  10236  ltsubadd2  10484  lesubadd2  10486  ltaddpos2  10504  posdif  10506  lesub1  10507  ltnegcon1  10514  lenegcon1  10517  addge02  10524  leaddle0  10528  mulge0  10531  msqge0  10534  ltordlem  10538  possumd  10637  sublt0d  10638  prodgt0  10853  prodgt02  10854  prodge02  10856  ltmulgt12  10869  lemulge12  10871  mulge0b  10878  mulle0b  10879  ltdivmul  10883  ledivmul  10884  ltdivmul2  10885  lt2mul2div  10886  ledivmul2  10887  ltrec  10890  ltrec1  10895  ltdiv23  10899  lediv23  10900  nnge1  11031  halfpos  11247  lt2halves  11252  addltmul  11253  avglt2  11256  avgle2  11258  nnrecl  11275  difgtsumgt  11331  zltlem1  11415  nn0le2is012  11426  gtndiv  11439  nn01to3  11766  rebtwnz  11772  nnledivrp  11925  xrmax1  11991  max1ALT  12002  qbtwnre  12015  xralrple  12021  xltnegi  12032  xmulval  12041  xsubge0  12076  xposdif  12077  xlesubadd  12078  divelunit  12299  eluzgtdifelfzo  12513  fllelt  12581  flflp1  12591  flbi  12600  btwnzge0  12612  2tnp1ge0ge0  12613  dfceil2  12623  ceilval2  12624  2submod  12714  addmodlteq  12728  om2uzlti  12732  monoord  12814  sermono  12816  expval  12845  expnbnd  12976  discr1  12983  discr  12984  facwordi  13059  seqcoll  13231  seqcoll2  13232  hashtpg  13250  swrdccat3blem  13476  cnpart  13961  sqrlem6  13969  sqrmo  13973  resqreu  13974  resqrtcl  13975  resqrtthlem  13976  sqrtneg  13989  sqreulem  14080  sqreu  14081  sqrtthlem  14083  eqsqrtd  14088  limsuple  14190  rlimcld2  14290  rlimrege0  14291  o1compt  14299  climserle  14374  caurcvgr  14385  fsum00  14511  fsumabs  14514  climcndslem2  14563  climcnds  14564  supcvg  14569  georeclim  14584  geoisumr  14590  cvgrat  14596  sin01bnd  14896  cos01bnd  14897  ruclem1  14941  ruclem9  14948  ruclem12  14951  summodnegmod  14993  modmulconst  14994  dvdsaddr  15006  dvdssub  15007  dvdssubr  15008  dvdsfac  15029  dvdsmod  15031  fprodfvdvdsd  15039  oddp1even  15049  ltoddhalfle  15066  opoe  15068  omoe  15069  sumeven  15091  sumodd  15092  divalglem0  15097  divalglem2  15099  divalglem4  15100  divalglem5  15101  divalglem9  15105  divalg  15107  divalg2  15109  divalgmod  15110  divalgmodOLD  15111  ndvdssub  15114  ndvdsadd  15115  bitsfval  15126  bitsval  15127  bits0  15131  bitsp1  15134  bitsfzolem  15137  bitsfzo  15138  bitscmp  15141  bitsinv1lem  15144  bitsshft  15178  gcdcllem1  15202  dvdslegcd  15207  bezoutlem4  15240  dvdssqim  15254  dvdsmulgcd  15255  dvdssq  15261  nn0seqcvgd  15264  lcmfunsnlem2lem2  15333  coprmdvds  15347  coprmdvdsOLD  15348  coprmdvds2  15349  rpmul  15354  cncongr1  15362  divgcdodd  15403  isprm6  15407  prmdvdsexp  15408  prmdvdsexpr  15410  prmfac1  15412  hashdvds  15461  phiprmpw  15462  eulerthlem2  15468  prmdiv  15471  prmdiveq  15472  odzval  15477  odzcllem  15478  odzdvds  15481  pythagtriplem11  15511  pythagtriplem13  15513  pythagtrip  15520  pceulem  15531  pczndvds2  15552  pcdvdsb  15554  pc2dvds  15564  pcz  15566  pcprmpw2  15567  dvdsprmpweq  15569  dvdsprmpweqle  15571  difsqpwdvds  15572  pcaddlem  15573  pcmpt  15577  prmpwdvds  15589  pockthlem  15590  prmreclem2  15602  prmreclem4  15604  4sqlem11  15640  vdwlem9  15674  rami  15700  ramlb  15704  0ram  15705  ramz2  15709  ramub1lem1  15711  prmdvdsprmo  15727  prmgaplem7  15742  prmgaplem8  15743  setsstruct  15879  imasleval  16182  subsubc  16494  pospo  16954  mulgval  17524  oddvdsnn0  17944  odmulg  17954  pgpfi1  17991  pgpfi  18001  slwispgp  18007  pgpssslw  18010  subgslw  18012  sylow2alem2  18014  sylow2blem3  18018  fislw  18021  efgi  18113  efgval2  18118  efgsrel  18128  efgredlemb  18140  lt6abl  18277  telgsums  18371  dprdval  18383  dprd2dlem2  18420  dprd2da  18422  dprd2d2  18424  ablfacrplem  18445  ablfac1a  18449  ablfac1b  18450  ablfac1eulem  18452  ablfac1eu  18453  pgpfac1lem3a  18456  ablfaclem3  18467  dvdsrtr  18633  dvdsrmul1  18634  unitpropd  18678  isabvd  18801  mplval  19409  ressmplbas2  19436  mplbaspropd  19588  zndvds0  19880  znunit  19893  cygth  19901  frlmup1  20118  lmisfree  20162  pmatcoe1fsupp  20487  fvmptnn04if  20635  hmphindis  21581  ordthmeolem  21585  psmettri2  22095  ismet2  22119  xmettri2  22126  imasdsf1olem  22159  imasf1oxmet  22161  comet  22299  stdbdxmet  22301  nmogelb  22501  nmolb  22502  metdsge  22633  metdseq0  22638  iihalf2  22713  bndth  22738  evth  22739  ipcau2  23014  tchcphlem1  23015  tchcphlem2  23016  iscau3  23057  iscmet3  23072  bcthlem1  23102  bcth  23107  minveclem3b  23180  minveclem3  23181  minveclem4  23184  minveclem5  23185  pjthlem1  23189  pjthlem2  23190  pmltpclem1  23198  pmltpc  23200  ivthlem2  23202  ivthlem3  23203  ovolgelb  23229  ovolunlem1  23246  ovoliunlem2  23252  ovolshftlem1  23258  ovolscalem1  23262  ovolicc1  23265  ovolicc2lem3  23268  ioombl1lem4  23310  mbfmulc2lem  23395  mbfposb  23401  mbfaddlem  23408  mbfsup  23412  mbfinf  23413  mbflimsup  23414  i1fposd  23455  itg1ge0a  23459  mbfi1fseqlem4  23466  mbfi1fseqlem6  23468  mbfi1flimlem  23470  mbfi1flim  23471  itg2const2  23489  itg2seq  23490  itg2monolem1  23498  itg2i1fseq  23503  itg2addlem  23506  ibllem  23512  isibl  23513  isibl2  23514  iblitg  23516  dfitg  23517  cbvitg  23523  itgeq2  23525  itgvallem  23532  iblneg  23550  itgneg  23551  itggt0  23589  dvlip  23737  c1lip1  23741  dvfsumle  23765  dvfsumlem2  23771  dvfsumlem4  23773  dvfsum2  23778  mdeglt  23806  degltp1le  23814  deg1suble  23848  ply1divex  23877  plypf1  23949  dgrlb  23973  coemulc  23992  dgrsub  24009  quotval  24028  plydivlem4  24032  quotcan  24045  vieta1lem2  24047  aalioulem2  24069  aaliou3lem9  24086  ulmcn  24134  dvradcnv  24156  sincosq1sgn  24231  sincosq2sgn  24232  sincosq4sgn  24234  logltb  24327  logle1b  24360  loglt1b  24361  cxpge0  24410  cxple2  24424  logreclem  24481  jensen  24696  emcllem7  24709  lgamgulmlem1  24736  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem5  24740  lgambdd  24744  lgamcvglem  24747  wilthlem1  24775  ftalem2  24781  ftalem3  24782  ftalem7  24786  fta  24787  sgmval  24849  mumul  24888  dvdsppwf1o  24893  musum  24898  chtublem  24917  chtub  24918  perfect1  24934  bcmono  24983  bclbnd  24986  bposlem1  24990  bposlem5  24994  lgslem1  25003  lgsval  25007  lgsdilem  25030  lgsne0  25041  lgsqrlem2  25053  lgsqrlem4  25055  gausslemma2dlem1a  25071  lgseisenlem1  25081  lgseisenlem2  25082  lgsquadlem1  25086  lgsquadlem2  25087  lgsquadlem3  25088  lgsquad2lem2  25091  m1lgs  25094  2lgslem1a1  25095  2lgslem1a  25097  2lgsoddprmlem2  25115  2lgsoddprmlem3  25120  2sqlem4  25127  2sqlem8a  25131  2sqblem  25137  dchrisumlema  25158  dchrisumlem2  25160  dchrisumlem3  25161  chpdifbndlem2  25224  pntrsumbnd2  25237  pntpbnd1  25256  pntibndlem3  25262  pntlemi  25274  pntleme  25278  pntlem3  25279  pnt3  25282  ostth2lem2  25304  ostth3  25308  ostth  25309  tgcgrxfr  25394  hlpasch  25629  islmib  25660  lmicom  25661  trgcopyeu  25679  iscgra  25682  iscgra1  25683  iscgrad  25684  isleag  25714  iseqlg  25728  brbtwn2  25766  axlowdim2  25821  axlowdim  25822  axcontlem2  25826  axcontlem3  25827  axcontlem4  25828  axcontlem9  25833  axcontlem10  25834  axcontlem11  25835  axcontlem12  25836  ebtwntg  25843  umgrislfupgrlem  25998  lfgredgge2  26000  lfgrnloop  26001  lfuhgr1v0e  26127  1hevtxdg1  26383  vtxdgoddnumeven  26430  ewlksfval  26478  isewlk  26479  ewlkinedg  26481  lfgrwlkprop  26565  crctcshlem4  26693  umgrwwlks2on  26831  elwwlks2  26842  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  eupth2lem3lem3  27070  eupth2lem3lem4  27071  eupth2lem3lem6  27073  eupth2lem3lem7  27074  eupth2lems  27078  eupth2  27079  eucrct2eupth  27085  konigsberglem4  27097  frgrreggt1  27221  ex-ind-dvds  27288  nmounbseqi  27602  nmounbseqiALT  27603  isblo3i  27626  blo3i  27627  blocnilem  27629  siilem2  27677  normlem6  27942  normgt0  27954  norm3dif  27977  norm3lemt  27979  pjhthlem1  28220  pjige0  28520  nmcexi  28855  lnconi  28862  lnopcnbd  28865  lnfncnbd  28886  riesz1  28894  cnlnadjlem2  28897  cnlnadjlem8  28903  leopg  28951  leop2  28953  leoppos  28955  leopadd  28961  leopmuli  28962  leopmul2i  28964  pjssge0i  28995  pjdifnormi  28996  pjssposi  29001  pjssdif1i  29004  chcv1  29184  cvexch  29203  atcvatlem  29214  atcvat3i  29225  atdmd  29227  cdj3i  29270  addltmulALT  29275  xrofsup  29507  fsumiunle  29549  xrge0addgt0  29665  omndadd  29680  omndmul2  29686  ogrpinvlt  29698  isinftm  29709  isarchi3  29715  archirng  29716  archirngz  29717  archiexdiv  29718  isorng  29773  orngmul  29777  ofldchr  29788  isarchiofld  29791  elrhmunit  29794  rearchi  29816  fzto1st  29827  unitdivcld  29921  esumlub  30096  esumfsup  30106  esumcvg  30122  esum2d  30129  dya2ub  30306  omssubadd  30336  carsgmon  30350  itgeq12dv  30362  oddpwdc  30390  eulerpartlems  30396  prob01  30449  orvcval  30493  ballotlemfc0  30528  ballotlemfcc  30529  ballotleme  30532  ballotlem4  30534  ballotlemimin  30541  ballotlem1c  30543  ballotlemsval  30544  ballotlemieq  30552  ballotlemfrcn0  30565  sgnmulsgp  30586  signsply0  30602  signslema  30613  signsvfpn  30636  erdszelem8  31154  erdsze2lem2  31160  abs2sqle  31548  abs2sqlt  31549  pdivsq  31610  dvdspw  31611  poseq  31724  soseq  31725  sltval  31774  nolt02o  31819  nosupbnd1lem1  31828  nosupbnd1lem2  31829  nosupbnd2  31836  conway  31884  scutcut  31886  scutbday  31887  scutun12  31891  scutbdaybnd  31895  scutbdaylt  31896  cgrdegen  32086  brofs  32087  segconeu  32093  btwntriv2  32094  transportprops  32116  brifs  32125  ifscgr  32126  brcgr3  32128  cgrxfr  32137  brcolinear2  32140  colineardim1  32143  brfs  32161  idinside  32166  btwnconn1lem11  32179  btwnconn1lem12  32180  btwnconn1lem14  32182  brsegle  32190  seglerflx  32194  seglemin  32195  segleantisym  32197  btwnsegle  32199  outsideofeu  32213  outsidele  32214  fvray  32223  nn0prpwlem  32292  nn0prpw  32293  unblimceq0lem  32472  unbdqndv2  32477  knoppndvlem13  32490  knoppndvlem19  32496  knoppndvlem21  32498  ltflcei  33368  cos2h  33371  tan2h  33372  matunitlindflem2  33377  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem18  33398  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem25  33405  poimirlem27  33407  poimirlem28  33408  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  poimir  33413  heicant  33415  mblfinlem2  33418  mblfinlem3  33419  mblfinlem4  33420  itg2addnclem  33432  itg2addnclem2  33433  itg2gt0cn  33436  itggt0cn  33453  ftc1anclem5  33460  dvasin  33467  areacirclem1  33471  areacirclem4  33474  areacirclem5  33475  areacirc  33476  seqpo  33514  incsequz2  33516  mettrifi  33524  heibor1lem  33579  rrncmslem  33602  lsatcv0eq  34153  oposlem  34288  oplecon1b  34307  opltcon1b  34311  atlatmstc  34425  cvlexch1  34434  cvlexch2  34435  cvlexchb2  34437  cvlatexchb2  34441  cvlatexch2  34443  cvlatcvr2  34448  cvlsupr2  34449  ishlat1  34458  hlsuprexch  34486  cvrexch  34525  cvrat  34527  atcvr0eq  34531  atcvrj0  34533  atltcvr  34540  cvrat3  34547  cvrat4  34548  cvrat42  34549  3noncolr2  34554  hlatcon2  34557  4noncolr3  34558  3dimlem1  34563  3dimlem2  34564  3dimlem3a  34565  3dimlem3  34566  3dimlem3OLDN  34567  3dimlem4a  34568  3dimlem4  34569  3dimlem4OLDN  34570  3dim1lem5  34571  3dim2  34573  3dim3  34574  ps-1  34582  ps-2  34583  3atlem5  34592  3atlem6  34593  lplni2  34642  lplnnle2at  34646  lplnnleat  34647  lplnnlelln  34648  lplnribN  34656  lplnexllnN  34669  lvoli2  34686  lvolnle3at  34687  lvolnleat  34688  lvolnlelln  34689  lvolnlelpln  34690  4atlem9  34708  4atlem10a  34709  4atlem11a  34712  4atlem11  34714  4atlem12a  34715  dalempnes  34756  dalemqnet  34757  dalem1  34764  dalemswapyzps  34795  dalemrotps  34796  dalem30  34807  dalem35  34812  lineset  34843  islinei  34845  psubspset  34849  psubspi2N  34853  snatpsubN  34855  2llnma1  34892  elpaddn0  34905  elpaddri  34907  elpaddat  34909  elpadd2at  34911  paddcom  34918  paddasslem12  34936  pmapjat1  34958  llnexchb2  34974  lhp2at0nle  35140  lhprelat3N  35145  4atexlemswapqr  35168  4atexlemcnd  35177  lautle  35189  lautcvr  35197  ltrnel  35244  ltrneq2  35253  trlnle  35292  cdlemc3  35299  cdlemd6  35309  cdleme3  35343  cdleme7aa  35348  cdleme7  35355  cdleme11c  35367  cdleme15c  35382  cdleme20yOLD  35409  cdleme20m  35430  cdleme21b  35433  cdleme21c  35434  cdleme21at  35435  cdleme36a  35567  cdleme43bN  35597  cdleme43dN  35599  cdleme46f2g2  35600  cdleme46f2g1  35601  cdlemeg46c  35620  cdlemeg46nlpq  35624  cdlemb3  35713  cdlemg4d  35720  cdlemg6d  35728  cdlemg10c  35746  cdlemg12  35757  cdlemg27b  35803  djhcvat42  36523  elpell1qr2  37255  monotuz  37325  monotoddzzfi  37326  monotoddzz  37327  oddcomabszz  37328  rmxypos  37333  mzpcong  37358  congrep  37359  acongsym  37362  acongneg2  37363  acongtr  37364  acongeq12d  37365  jm2.18  37374  jm2.19lem2  37376  jm2.19lem3  37377  jm2.19lem4  37378  jm2.19  37379  jm2.25  37385  jm2.15nn0  37389  jm2.16nn0  37390  jm2.27  37394  rmydioph  37400  expdiophlem1  37407  expdiophlem2  37408  fnwe2lem2  37440  relexpmulg  37821  relexpxpmin  37828  frege124d  37872  frege72  38049  frege91  38068  inductionexd  38273  imo72b2lem0  38285  imo72b2lem2  38287  imo72b2lem1  38291  imo72b2  38295  dvgrat  38331  hashnzfz  38339  evth2f  38994  evthf  39006  rfcnpre3  39012  brneqtrd  39068  dmrelrnrel  39235  upbdrech2  39335  supxrgelem  39366  supxrge  39367  xrlexaddrp  39381  xralrple2  39383  ltdivgt1  39385  infleinf  39401  xralrple4  39402  xralrple3  39403  ltdiv23neg  39430  leneg3d  39500  fsumlessf  39609  fmul01  39612  fmul01lt1lem1  39616  climinf  39638  climinff  39643  limcrecl  39661  limsupre  39673  limclner  39683  limsuppnfd  39734  climinf2  39739  limsuppnf  39743  climinfmpt  39747  limsupre2  39757  limsupre2mpt  39762  limsupre3  39765  limsupre3mpt  39766  limsupre3uz  39768  limsupreuz  39769  limsupvaluz2  39770  limsupreuzmpt  39771  limsupge  39787  liminfreuz  39829  liminflt  39831  liminflimsupclim  39833  cncficcgt0  39864  stoweidlem3  39983  stoweidlem7  39987  stoweidlem15  39995  stoweidlem16  39996  stoweidlem18  39998  stoweidlem26  40006  stoweidlem27  40007  stoweidlem28  40008  stoweidlem31  40011  stoweidlem34  40014  stoweidlem36  40016  stoweidlem37  40017  stoweidlem41  40021  stoweidlem44  40024  stoweidlem45  40025  stoweidlem46  40026  stoweidlem48  40028  stoweidlem51  40031  stoweidlem55  40035  stoweidlem59  40039  stoweidlem60  40040  stoweidlem62  40042  fourierdlem42  40129  fourierdlem50  40136  fourierdlem54  40140  fourierdlem68  40154  fourierdlem79  40165  fourierdlem96  40182  fourierdlem97  40183  fourierdlem98  40184  fourierdlem99  40185  fourierdlem105  40191  fourierdlem108  40194  fourierdlem110  40196  fourierdlem111  40197  etransclem24  40238  etransclem25  40239  etransclem35  40249  etransclem37  40251  etransclem41  40255  etransclem44  40258  sge0gerp  40375  sge0pnffigt  40376  sge0gerpmpt  40382  omessle  40475  ovncvrrp  40541  ovnsubaddlem1  40547  ovnsubadd  40549  hoidmv1lelem2  40569  hoidmvlelem3  40574  hoidmvle  40577  ovncvr2  40588  hoidifhspval2  40592  hoidifhspval3  40596  hspmbllem2  40604  hspmbl  40606  pimgtpnf2  40680  pimgtmnf2  40687  pimdecfgtioc  40688  pimdecfgtioo  40690  pimincfltioo  40691  pimgtmnf  40695  incsmf  40714  issmfgt  40728  decsmf  40738  smfpreimagtf  40739  issmfge  40741  smflimlem4  40745  smflim  40748  smfpimgtxr  40751  smfpimgtmpt  40752  smfpimgtxrmpt  40755  smfinflem  40786  smfinf  40787  smfinfmpt  40788  ltsubsubaddltsub  41078  subsubelfzo0  41099  smonoord  41105  iccpartiltu  41122  iccpartlt  41124  iccpartgtl  41126  iccpartgt  41127  iccpartgel  41129  iccpartrn  41130  iccpartiun  41134  icceuelpartlem  41135  iccpartdisj  41137  iccpartnel  41138  goldbachthlem2  41223  fmtnoprmfac1lem  41241  fmtnoprmfac1  41242  fmtnofac1  41247  2pwp1prm  41268  flsqrt  41273  lighneallem1  41287  lighneallem3  41289  lighneallem4  41292  bits0ALTV  41355  sbgoldbaltlem1  41432  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  bgoldbtbnd  41462  1hegrlfgr  41478  lcoop  41965  islininds  42000  ldepsnlinc  42062  ltsubaddb  42069  ltsubsubb  42070  ltsubadd2b  42071  bigoval  42108  elbigo2r  42112  logbge0b  42122  logblt1b  42123  fldivexpfllog2  42124  nnlog2ge0lt1  42125  fllog2  42127  nnpw2pmod  42142  dignn0ldlem  42161  dig2nn1st  42164
  Copyright terms: Public domain W3C validator