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

Theorem recnd 8861
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
recnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem recnd
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 recn 8827 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 15 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   CCcc 8735   RRcr 8736
This theorem is referenced by:  00id  8987  mul02lem1  8988  addid1  8992  cnegex  8993  ltadd1  9241  leadd2  9243  ltsubadd  9244  ltsubadd2  9245  lesubadd  9246  lesubadd2  9247  lesub1  9268  lesub2  9269  ltnegcon1  9275  ltnegcon2  9276  add20  9286  subge0  9287  suble0  9288  lesub0  9290  mulge0  9291  eqord2  9304  rereccl  9478  redivcl  9479  recgt0  9600  prodgt0  9601  prodge0  9603  ltmul1a  9605  ltdiv1  9620  ltmuldiv  9626  ltrec  9637  recp1lt1  9654  recreclt  9655  ledivp1  9658  infmsup  9732  infmrcl  9733  rimul  9737  cru  9738  avglt1  9949  avglt2  9950  nn0cnd  10020  zcn  10029  zeo  10097  zcnd  10118  cnref1o  10349  rpcn  10362  rpcnd  10392  ltaddrp2d  10420  qbtwnre  10526  xralrple  10532  xpncan  10571  xmulcom  10586  xmulneg1  10589  xlemul1  10610  icoshftf1o  10759  lincmb01cmp  10777  iccf1o  10778  fladdz  10950  flzadd  10951  flhalf  10954  ceim1l  10957  intfracq  10963  fldiv  10964  mod0  10978  modlt  10981  moddiffl  10982  modfrac  10984  flmod  10985  intfrac  10986  modmulnn  10988  modid  10993  modcyc  10999  modadd1  11001  modnegd  11004  modadd12d  11005  modsub12d  11006  moddi  11007  modsubdir  11008  modirr  11009  seqf1olem1  11085  serle  11101  expcl2lem  11115  expnegz  11136  expaddzlem  11145  expaddz  11146  expmulz  11148  ltexp2a  11153  leexp2a  11157  leexp2r  11159  exple1  11161  expubnd  11162  sq11  11176  bernneq2  11228  expmulnbnd  11233  discr1  11237  discr  11238  faclbnd  11303  bcp1nk  11329  remim  11602  reim0b  11604  rereb  11605  mulre  11606  cjreb  11608  recj  11609  reneg  11610  readd  11611  resub  11612  remullem  11613  remul2  11615  rediv  11616  imcj  11617  imneg  11618  imadd  11619  imsub  11620  immul2  11622  imdiv  11623  cjcj  11625  cjadd  11626  ipcnval  11628  cjmulval  11630  cjneg  11632  imval2  11636  cjreim2  11646  sqr0lem  11726  sqrlem5  11732  sqrlem7  11734  resqrthlem  11740  remsqsqr  11742  sqrmul  11745  sqrdiv  11751  sqrneg  11753  sqrmsq  11756  absdiv  11780  absid  11781  absexp  11789  absexpz  11790  absimle  11794  abslt  11798  absle  11799  abssubne0  11800  releabs  11805  recval  11806  abstri  11814  abs2difabs  11818  abs1m  11819  abslem2  11823  absrdbnd  11825  sqreulem  11843  sqreu  11844  amgm2  11853  lo1bddrp  11999  o1lo1  12011  rlimrecl  12054  rlimge0  12055  climrecl  12057  climge0  12058  climabs0  12059  reccn2  12070  o1rlimmul  12092  lo1mul2  12102  lo1sub  12104  climle  12113  climsqz  12114  climsqz2  12115  rlimsqz  12123  rlimsqz2  12124  rlimno1  12127  climlec2  12132  isercolllem1  12138  climsup  12143  caucvgrlem  12145  caurcvgr  12146  caucvgrlem2  12147  iseraltlem1  12154  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  isumrecl  12228  isumge0  12229  fsumless  12254  fsumge1  12255  fsum00  12256  fsumle  12257  fsumlt  12258  fsumabs  12259  o1fsum  12271  seqabs  12272  cvgcmp  12274  cvgcmpce  12276  abscvgcvg  12277  isumrpcl  12302  isumle  12303  isumless  12304  isumsup  12306  climcndslem1  12308  climcndslem2  12309  climcnds  12310  flo1  12313  supcvg  12314  trireciplem  12320  trirecip  12321  explecnv  12323  geo2sum  12329  geo2lim  12331  geomulcvg  12332  cvgrat  12339  mertenslem1  12340  mertenslem2  12341  efcllem  12359  ege2le3  12371  efaddlem  12374  efgt0  12383  eftlub  12389  effsumlt  12391  eflt  12397  eflegeo  12401  resin4p  12418  recos4p  12419  retanhcl  12439  tanhlt1  12440  efeul  12442  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  absefi  12476  absef  12477  absefib  12478  efieq1re  12479  eirrlem  12482  rpnnen2lem5  12497  rpnnen2lem8  12500  rpnnen2lem9  12501  rpnnen2lem11  12503  rpnnen2  12504  moddvds  12538  odd2np1  12587  divalglem5  12596  bitsp1  12622  bitsp1o  12624  bitsfzo  12626  bitscmp  12629  sadcaddlem  12648  nn0seqcvgd  12740  sqnprm  12777  isprm5  12791  nonsq  12830  eulerthlem2  12850  prmdiveq  12854  odzdvds  12860  pythagtriplem14  12881  pcid  12925  fldivp1  12945  pcfac  12947  pockthlem  12952  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  prmrec  12969  4sqlem5  12989  4sqlem10  12994  mul4sqlem  13000  4sqlem15  13006  4sqlem16  13007  mulgneg  14585  ghmmulg  14695  odmodnn0  14855  mndodconglem  14856  pgpfaclem2  15317  isabvd  15585  abv1z  15597  abvneg  15599  abvrec  15601  abvdiv  15602  abvdom  15603  rege0subm  16428  cnsubrg  16432  gzrngunitlem  16436  prmirredlem  16446  bl2in  17957  blhalf  17960  blss  17972  methaus  18066  nrmmetd  18097  nm2dif  18146  nminvr  18180  nmdvr  18181  nlmmul0or  18194  nrginvrcnlem  18201  nmolb2d  18227  nmoi2  18239  nmoleub  18240  nmo0  18244  nmoeq0  18245  nmoco  18246  nmotri  18248  nmoid  18251  blcvx  18304  xrsxmet  18315  recld2  18320  reconnlem2  18332  opnreen  18336  metdstri  18355  metnrmlem3  18365  iihalf2cn  18432  icchmeo  18439  icopnfcnv  18440  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  icccvx  18448  cnheiborlem  18452  evth  18457  lebnumii  18464  pcoass  18522  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  nmoleub2lem  18595  nmoleub2lem3  18596  nmoleub3  18600  cphsqrcl2  18622  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  tchcph  18667  iscau3  18704  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  minveclem7  18799  pjthlem1  18801  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ovolfsval  18830  ovollb2lem  18847  ovolctb  18849  ovolunlem1a  18855  ovolunnul  18859  ovolfiniun  18860  ovoliunlem1  18861  ovoliun2  18865  shft2rab  18867  ovolshftlem1  18868  sca2rab  18871  ovolscalem1  18872  ovolsca  18874  ovolicc1  18875  ovolicc2lem4  18879  ovolicopnf  18883  cmmbl  18892  nulmbl  18893  nulmbl2  18894  unmbl  18895  volinun  18903  volfiniun  18904  voliunlem1  18907  voliunlem3  18909  ioombl1lem3  18917  ioombl1lem4  18918  ovolioo  18925  ioorcl2  18927  uniioovol  18934  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombllem6  18943  dyadovol  18948  dyaddisjlem  18950  opnmbllem  18956  vitalilem1  18963  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  ismbf  18985  mbfmulc2lem  19002  mbfmulc2re  19003  mbfpos  19006  mbfmulc2  19018  mbfinf  19020  itg1val2  19039  itg11  19046  i1fmullem  19049  i1fadd  19050  itg1addlem4  19054  itg1addlem5  19055  i1fmulclem  19057  i1fmulc  19058  itg1mulc  19059  itg1sub  19064  itg10a  19065  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfmullem2  19079  itg2const  19095  itg2const2  19096  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem3  19107  itg2addlem  19113  itgcl  19138  itgcnlem  19144  itgrevallem1  19149  itgposval  19150  iblneg  19157  itgneg  19158  i1fibl  19162  itgitg1  19163  itgconst  19173  ibladd  19175  itgaddlem2  19178  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem2  19187  itgmulc2  19188  itgabs  19189  itgsplit  19190  bddmulibl  19193  dvcjbr  19298  dvfre  19300  dvexp3  19325  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  c1liplem1  19343  c1lip1  19344  dveq0  19347  dv11cn  19348  dvlt0  19352  dvle  19354  dvivthlem1  19355  dvivth  19357  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlimge0  19377  dvfsumrlim2  19379  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  ftc1lem5  19387  plyeq0lem  19592  coemulhi  19635  plyrecj  19660  plydivlem3  19675  aalioulem2  19713  aalioulem3  19714  aalioulem4  19715  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou2  19720  aaliou2b  19721  aaliou3lem3  19724  aaliou3lem7  19729  aaliou3lem9  19730  taylthlem2  19753  ulmcn  19776  ulmdvlem1  19777  mtest  19781  itgulm  19784  radcnvlem1  19789  radcnvlem2  19790  radcnvlt1  19794  radcnvle  19796  dvradcnv  19797  pserulm  19798  abelthlem2  19808  abelthlem5  19811  abelthlem7  19814  abelth2  19818  reeff1olem  19822  efcvx  19825  pilem2  19828  pilem3  19829  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  coseq0negpitopi  19871  tanrpcl  19872  tangtx  19873  tanabsge  19874  sinq12gt0  19875  sinq34lt0t  19877  cosq14gt0  19878  cosq14ge0  19879  pige3  19885  coskpi  19888  sineq0  19889  cosordlem  19893  sinord  19896  tanord1  19899  tanord  19900  tanregt0  19901  efif1olem2  19905  efif1olem4  19907  eff1olem  19910  logrnaddcl  19931  logneg  19941  lognegb  19943  reexplog  19948  relogexp  19949  logfac  19954  efiarg  19961  cosargd  19962  cosarg0d  19963  argregt0  19964  argrege0  19965  argimgt0  19966  logneg2  19969  tanarg  19970  logdivlti  19971  divlogrlim  19982  logcnlem2  19990  logcnlem3  19991  logcnlem4  19992  logcn  19994  logf1o2  19997  advlog  20001  advlogexp  20002  efopnlem1  20003  logtayllem  20006  logtayl  20007  logccv  20010  logcxp  20016  mulcxp  20032  divcxp  20034  cxpmul  20035  cxproot  20037  cxpmul2z  20038  abscxp  20039  abscxp2  20040  cxplt  20041  cxplea  20043  cxple2  20044  cxple2a  20046  cxplt3  20047  cxpsqrlem  20049  cxpsqr  20050  logsqr  20051  dvcxp2  20083  cxpcn3lem  20087  resqrcn  20089  cxpaddlelem  20091  cxpaddle  20092  abscxpbnd  20093  root1id  20094  root1eq1  20095  root1cj  20096  cxpeq  20097  loglesqr  20098  cosangneg2d  20105  angrtmuld  20106  ang180lem2  20108  lawcoslem1  20113  lawcos  20114  pythag  20115  isosctrlem1  20118  isosctrlem2  20119  isosctrlem3  20120  ssscongptld  20122  chordthmlem  20129  chordthmlem2  20130  chordthmlem3  20131  chordthmlem4  20132  chordthmlem5  20133  asinsinlem  20187  reasinsin  20192  acosrecl  20199  atancj  20206  atanrecl  20207  atanlogaddlem  20209  atanlogsublem  20211  atanbndlem  20221  atans2  20227  ressatans  20230  atantayl  20233  leibpilem2  20237  leibpi  20238  leibpisum  20239  log2tlbnd  20241  log2ublem2  20243  birthdaylem2  20247  birthdaylem3  20248  cxp2limlem  20270  cxp2lim  20271  cxploglim  20272  cxploglim2  20273  divsqrsumo1  20278  cvxcl  20279  scvxcvx  20280  jensenlem2  20282  jensen  20283  amgmlem  20284  emcllem2  20290  emcllem3  20291  emcllem5  20293  emcllem6  20294  emcllem7  20295  harmonicbnd4  20304  fsumharmonic  20305  ftalem1  20310  ftalem2  20311  ftalem4  20313  ftalem5  20314  basellem3  20320  basellem4  20321  basellem5  20322  basellem6  20323  basellem7  20324  basellem8  20325  basellem9  20326  efnnfsumcl  20340  chtprm  20391  chpp1  20393  chtdif  20396  efchtdvds  20397  prmorcht  20416  mumullem2  20418  fsumfldivdiaglem  20429  ppiub  20443  chtleppi  20449  chtublem  20450  chtub  20451  pclogsum  20454  vmasum  20455  logfac2  20456  chpval2  20457  chpchtsum  20458  chpub  20459  logfaclbnd  20461  logfacbnd3  20462  logfacrlim  20463  logexprlim  20464  logfacrlim2  20465  mersenne  20466  dchrabs  20499  dchrptlem1  20503  dchrptlem2  20504  bcmax  20517  bcp1ctr  20518  bposlem1  20523  bposlem9  20531  lgsvalmod  20554  lgsdilem  20561  lgsne0  20572  lgsqrlem2  20581  lgseisenlem1  20588  lgseisenlem2  20589  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  mul2sq  20604  2sqlem3  20605  2sqlem8  20611  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  chtppilimlem1  20622  chtppilimlem2  20623  chtppilim  20624  chto1ub  20625  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  vmadivsum  20631  vmadivsumb  20632  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlema  20637  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasum2if  20646  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  dchrisum0flblem1  20657  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrmusumlem  20671  dchrvmasumlem  20672  rpvmasum  20675  rplogsum  20676  dirith2  20677  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  logdivsum  20682  mulog2sumlem1  20683  mulog2sumlem2  20684  mulog2sumlem3  20685  vmalogdivsum2  20687  vmalogdivsum  20688  2vmadivsumlem  20689  logsqvma  20691  logsqvma2  20692  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  selberglem3  20696  selberg  20697  selbergb  20698  selberg2lem  20699  selberg2  20700  selberg2b  20701  chpdifbndlem1  20702  logdivbnd  20705  selberg3lem1  20706  selberg3lem2  20707  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrmax  20713  pntrsumo1  20714  pntrsumbnd  20715  pntrsumbnd2  20716  selbergr  20717  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntsval2  20725  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6a  20731  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemn  20749  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlem3  20758  pntleml  20760  pnt2  20762  pnt  20763  abvcxp  20764  ostth2lem1  20767  qabvexp  20775  padicabv  20779  padicabvcxp  20781  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  nvm1  21230  nvpi  21232  nvz0  21234  nvmtri  21237  nvabs  21239  nvge0  21240  nv1  21242  smcnlem  21270  ipval2lem4  21279  ipval2  21280  4ipval2  21281  4ipval3  21285  ipidsq  21286  dipcj  21290  dip0r  21293  ipz  21295  nmoub3i  21351  nmlno0lem  21371  nmblolbii  21377  blocnilem  21382  cncph  21397  ipasslem4  21412  ipasslem5  21413  ipblnfi  21434  minvecolem2  21454  minvecolem4  21459  minvecolem6  21461  minvecolem7  21462  htthlem  21497  normpyc  21725  hhph  21757  bcs2  21761  norm1  21828  norm1exi  21829  pjhthlem1  21970  eigvalcl  22541  eighmorth  22544  nmlnop0iALT  22575  nmbdoplbi  22604  nmcexi  22606  nmcoplbi  22608  nmbdfnlbi  22629  nmcfnlbi  22632  riesz4i  22643  cnlnadjlem2  22648  cnlnadjlem7  22653  nmopcoi  22675  nmopcoadji  22681  branmfn  22685  leopnmid  22718  opsqrlem1  22720  hst1h  22807  hstle  22810  hstoh  22812  sto2i  22817  stadd3i  22828  strlem1  22830  golem1  22851  stcltrlem1  22856  cdj1i  23013  cdj3lem1  23014  cdj3lem3b  23020  cdj3i  23021  fzsplit3  23031  bcm1n  23032  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsgt1  23069  ballotlemsel1i  23071  ballotlemsi  23073  lt2addrd  23249  sqsscirc1  23292  sqsscirc2  23293  cnre2csqima  23295  rmulccn  23301  xrge0iifcnv  23315  xrge0iifhom  23319  nnlogbexp  23406  logbrec  23407  esumpcvgval  23446  dya2ub  23575  dya2iocseg  23579  indsum  23606  zetacvg  23689  subfacval2  23718  subfaclim  23719  subfacval3  23720  rescon  23777  eupap1  23900  sinccvglem  24005  circum  24007  modaddabs  24011  fveecn  24530  eqeelen  24532  brbtwn2  24533  colinearalglem4  24537  colinearalg  24538  axsegconlem9  24553  axsegconlem10  24554  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3  24559  ax5seglem5  24561  ax5seglem6  24562  ax5seglem9  24565  ax5seg  24566  axbtwnid  24567  axpaschlem  24568  axpasch  24569  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  bpolydiflem  24789  bpoly4  24794  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem3  24926  areacirclem6  24930  areacirc  24931  cntrset  25602  dmse1  25603  msr3  25605  msr4  25606  mslb1  25607  2wsms  25608  msra3  25609  iintlem1  25610  lvsovso  25626  rnegvex2  25661  nn0prpwlem  26238  csbrn  26462  trirn  26463  mettrifi  26473  lmclim2  26474  geomcau  26475  isbnd3  26508  ssbnd  26512  cntotbnd  26520  bfplem1  26546  bfplem2  26547  bfp  26548  rrnmet  26553  rrndstprj1  26554  rrndstprj2  26555  rrncmslem  26556  rrnequiv  26559  rrntotbnd  26560  ismrer1  26562  eldioph2lem1  26839  lzenom  26849  rencldnfilem  26903  icodiamlt  26905  irrapxlem1  26907  irrapxlem2  26908  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  pell1234qrreccl  26939  pell14qrgt0  26944  pell14qrdivcl  26950  pell14qrexpclnn0  26951  pell14qrexpcl  26952  pell14qrdich  26954  pell1qrgaplem  26958  pellfundex  26971  reglogmul  26978  reglogexp  26979  reglogbas  26980  reglog1  26981  pellfund14  26983  rmspecsqrnq  26991  rmspecfund  26994  rmym1  27020  rmyluc  27022  monotoddzzfi  27027  expmordi  27032  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  jm2.24  27050  acongrep  27067  fzmaxdif  27068  acongeq  27070  modabsdifz  27078  jm2.19lem4  27085  jm2.19  27086  jm2.26lem3  27094  jm3.1lem1  27110  jm3.1lem2  27111  dvconstbi  27551  climinf  27732  stoweidlem13  27762  stoweidlem17  27766  stoweidlem21  27770  stoweidlem47  27796  stoweidlem59  27808  wallispilem3  27816  wallispilem5  27818  wallispi2lem1  27820  stirlinglem1  27823  stirlinglem5  27827  stirlinglem11  27833  stirlinglem12  27834  stirlinglem14  27836  sigaras  27845  sigarms  27846  sigarls  27847  sigarexp  27849  sigarperm  27850  sigarimcd  27852  sigarcol  27854  sharhght  27855  cevathlem2  27858
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator