Theorem recnd 9625

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

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		recn 9585	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 16	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1804   CCcc 9493   RRcr 9494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  00id  9758  mul02lem1  9759  addid1  9763  cnegex  9764  ltadd1  10026  leadd2  10028  ltsubadd  10029  ltsubadd2  10030  lesubadd  10031  lesubadd2  10032  lesub1  10053  lesub2  10054  ltnegcon1  10060  ltnegcon2  10061  add20  10071  subge0  10072  suble0  10073  lesub0  10076  mulge0  10077  eqord2  10091  rereccl  10269  redivcl  10270  recgt0  10393  prodgt0  10394  prodge0  10396  ltmul1a  10398  ltdiv1  10413  ltmuldiv  10422  ltrec  10433  recp1lt1  10450  recreclt  10451  ledivp1  10454  infmsup  10528  infmrcl  10529  rimul  10534  cru  10535  avglt1  10783  avglt2  10784  nn0cnd  10861  zcn  10876  zeo  10955  zcnd  10976  eluzelcn  11102  cnref1o  11225  rpcn  11238  rpcnd  11268  ltaddrp2d  11296  qbtwnre  11408  xralrple  11414  xpncan  11453  xmulcom  11468  xmulneg1  11471  xlemul1  11492  icoshftf1o  11653  lincmb01cmp  11673  iccf1o  11674  fladdz  11939  flzadd  11940  flhalf  11943  ceim1l  11955  intfracq  11967  fldiv  11968  modvalr  11980  flpmodeq  11982  mod0  11984  modlt  11987  moddiffl  11988  modfrac  11990  flmod  11991  intfrac  11992  modmulnn  11994  modvalp1  11995  modid  12001  modcyc  12012  modadd1  12014  modaddabs  12015  modadd2mod  12018  modnegd  12023  modadd12d  12024  modsub12d  12025  modaddmulmod  12034  moddi  12035  modsubdir  12036  modeqmodmin  12037  modirr  12038  seqf1olem1  12127  serle  12143  expcl2lem  12159  expnegz  12181  expaddzlem  12190  expaddz  12191  expmulz  12193  ltexp2a  12198  leexp2a  12202  leexp2r  12204  exple1  12206  expubnd  12207  sq11  12221  bernneq2  12274  expmulnbnd  12279  discr1  12283  discr  12284  faclbnd  12349  bcp1nk  12376  cshweqrep  12770  remim  12931  reim0b  12933  rereb  12934  mulre  12935  cjreb  12937  recj  12938  reneg  12939  readd  12940  resub  12941  remullem  12942  remul2  12944  rediv  12945  imcj  12946  imneg  12947  imadd  12948  imsub  12949  immul2  12951  imdiv  12952  cjcj  12954  cjadd  12955  ipcnval  12957  cjmulval  12959  cjneg  12961  imval2  12965  cjreim2  12975  sqr0lem  13055  sqrlem5  13061  sqrlem7  13063  resqrtthlem  13069  remsqsqrt  13071  sqrtmul  13074  sqrtdiv  13080  sqrtneg  13082  sqrtmsq  13085  absdiv  13109  absid  13110  absexp  13118  absexpz  13119  absimle  13123  abslt  13128  absle  13129  abssubne0  13130  releabs  13135  recval  13136  abstri  13144  abs2difabs  13148  abs1m  13149  abslem2  13153  absrdbnd  13155  sqreulem  13173  sqreu  13174  amgm2  13183  lo1bddrp  13329  o1lo1  13341  rlimrecl  13384  rlimge0  13385  climrecl  13387  climge0  13388  climabs0  13389  reccn2  13400  o1rlimmul  13422  lo1mul2  13432  lo1sub  13434  climle  13443  climsqz  13444  climsqz2  13445  rlimsqz  13453  rlimsqz2  13454  climlec2  13462  isercolllem1  13468  climsup  13473  caucvgrlem  13476  caurcvgr  13477  caucvgrlem2  13478  iseraltlem1  13485  iseraltlem2  13486  iseraltlem3  13487  iseralt  13488  isumrecl  13561  isumge0  13562  fsumless  13591  fsumge1  13592  fsum00  13593  fsumle  13594  fsumlt  13595  fsumabs  13596  o1fsum  13608  seqabs  13609  cvgcmp  13611  cvgcmpce  13613  abscvgcvg  13614  isumrpcl  13636  isumle  13637  isumless  13638  isumsup  13640  climcndslem1  13642  climcndslem2  13643  climcnds  13644  flo1  13647  supcvg  13648  trireciplem  13654  trirecip  13655  explecnv  13657  geo2sum  13663  geo2lim  13665  geomulcvg  13666  cvgrat  13673  mertenslem1  13674  mertenslem2  13675  fprodabs  13759  iprodrecl  13776  efcllem  13794  ege2le3  13806  efaddlem  13809  efgt0  13819  eftlub  13825  effsumlt  13827  eflt  13833  eflegeo  13837  resin4p  13854  recos4p  13855  retanhcl  13875  tanhlt1  13876  efeul  13878  ef01bndlem  13900  sin01bnd  13901  cos01bnd  13902  sin01gt0  13906  cos01gt0  13907  sin02gt0  13908  absefi  13912  absef  13913  absefib  13914  efieq1re  13915  eirrlem  13918  rpnnen2lem5  13933  rpnnen2lem8  13936  rpnnen2lem9  13937  rpnnen2lem11  13939  rpnnen2  13940  moddvds  13974  odd2np1  14027  divalglem5  14036  bitsp1o  14064  bitsfzo  14066  bitscmp  14069  sadcaddlem  14088  nn0seqcvgd  14180  sqnprm  14220  isprm5  14234  nonsq  14273  eulerthlem2  14293  prmdiveq  14297  odzdvds  14303  pythagtriplem14  14333  pcid  14377  fldivp1  14397  pcfac  14399  pockthlem  14404  prmreclem3  14417  prmreclem4  14418  prmreclem5  14419  prmrec  14421  4sqlem5  14441  4sqlem10  14446  mul4sqlem  14452  4sqlem15  14458  4sqlem16  14459  mulgneg  16138  ghmmulg  16257  odmodnn0  16542  mndodconglem  16543  pgpfaclem2  17111  isabvd  17447  abv1z  17459  abvneg  17461  abvrec  17463  abvdiv  17464  abvdom  17465  rege0subm  18452  cnsubrg  18456  gzrngunitlem  18460  prmirredlem  18500  prmirredlemOLD  18503  remulg  18620  regsumsupp  18635  bl2in  20880  blhalf  20885  blssps  20904  blss  20905  methaus  21000  nrmmetd  21072  nm2dif  21121  nminvr  21155  nmdvr  21156  nlmmul0or  21169  nrginvrcnlem  21176  nmolb2d  21202  nmoi2  21214  nmoleub  21215  nmo0  21219  nmoeq0  21220  nmoco  21221  nmotri  21223  nmoid  21226  blcvx  21280  xrsxmet  21291  recld2  21296  reconnlem2  21309  opnreen  21313  metdstri  21332  metnrmlem3  21342  icchmeo  21418  icopnfcnv  21419  icopnfhmeo  21420  iccpnfhmeo  21422  xrhmeo  21423  icccvx  21427  cnheiborlem  21431  evth  21436  lebnumii  21443  pcoass  21501  pcorevlem  21503  pcorev2  21505  pi1xfrcnv  21534  nmoleub2lem  21574  nmoleub2lem3  21575  nmoleub3  21579  cphsqrtcl2  21610  ipcau2  21654  tchcphlem1  21655  tchcphlem2  21656  tchcph  21657  iscau3  21694  rrxnm  21800  rrxcph  21801  csbren  21803  trirn  21804  rrxmval  21809  rrxmetlem  21811  rrxmet  21812  rrxdstprj1  21813  minveclem2  21818  minveclem3b  21820  minveclem4  21824  minveclem6  21826  minveclem7  21827  pjthlem1  21829  ivthlem2  21841  ivthlem3  21842  ivth2  21844  ovolfsval  21859  ovollb2lem  21876  ovolctb  21878  ovolunlem1a  21884  ovolunnul  21888  ovolfiniun  21889  ovoliunlem1  21890  ovoliun2  21894  shft2rab  21896  ovolshftlem1  21897  sca2rab  21900  ovolscalem1  21901  ovolsca  21903  ovolicc1  21904  ovolicc2lem4  21908  ovolicopnf  21912  cmmbl  21922  nulmbl  21923  nulmbl2  21924  unmbl  21925  volinun  21933  volfiniun  21934  voliunlem1  21937  voliunlem3  21939  ioombl1lem3  21947  ioombl1lem4  21948  ovolioo  21955  ioorcl2  21958  uniioovol  21965  uniioombllem3  21971  uniioombllem4  21972  uniioombllem5  21973  uniioombllem6  21974  dyadovol  21979  dyaddisjlem  21981  opnmbllem  21987  vitalilem1  21994  vitalilem2  21995  vitalilem3  21996  vitalilem4  21997  ismbf  22014  mbfmulc2lem  22031  mbfmulc2re  22032  mbfmulc2  22047  mbfinf  22049  itg1val2  22068  itg11  22075  i1fmullem  22078  i1fadd  22079  itg1addlem4  22083  itg1addlem5  22084  i1fmulclem  22086  i1fmulc  22087  itg1mulc  22088  itg1sub  22093  itg10a  22094  itg1ge0a  22095  itg1climres  22098  mbfi1fseqlem3  22101  mbfi1fseqlem4  22102  mbfi1fseqlem5  22103  mbfi1fseqlem6  22104  mbfi1flimlem  22106  mbfmullem2  22108  itg2const  22124  itg2const2  22125  itg2mulclem  22130  itg2mulc  22131  itg2splitlem  22132  itg2split  22133  itg2monolem1  22134  itg2monolem3  22136  itg2addlem  22142  itgcl  22167  itgcnlem  22173  itgrevallem1  22178  itgposval  22179  iblneg  22186  itgneg  22187  i1fibl  22191  itgitg1  22192  itgconst  22202  ibladd  22204  itgaddlem2  22207  iblabslem  22211  iblabs  22212  iblabsr  22213  iblmulc2  22214  itgmulc2lem2  22216  itgmulc2  22217  itgabs  22218  itgsplit  22219  bddmulibl  22222  dvcjbr  22329  dvfre  22331  dvexp3  22356  dveflem  22357  dvferm1lem  22362  dvferm2lem  22364  rolle  22368  cmvth  22369  mvth  22370  dvlip  22371  dvlipcn  22372  c1liplem1  22374  c1lip1  22375  dveq0  22378  dv11cn  22379  dvlt0  22383  dvle  22385  dvivthlem1  22386  dvivth  22388  lhop1lem  22391  lhop1  22392  lhop2  22393  lhop  22394  dvcvx  22398  dvfsumle  22399  dvfsumge  22400  dvfsumabs  22401  dvfsumlem1  22404  dvfsumlem2  22405  dvfsumlem4  22407  dvfsumrlimge0  22408  dvfsumrlim2  22410  dvfsum2  22412  ftc1a  22415  ftc1lem4  22417  ftc1lem5  22418  plyeq0lem  22584  coemulhi  22627  plyrecj  22652  plydivlem3  22667  aalioulem2  22705  aalioulem3  22706  aalioulem4  22707  aalioulem5  22708  aalioulem6  22709  aaliou  22710  aaliou2  22712  aaliou2b  22713  aaliou3lem3  22716  aaliou3lem7  22721  aaliou3lem9  22722  taylthlem2  22745  ulmcn  22770  ulmdvlem1  22771  mtest  22775  mtestbdd  22776  itgulm  22779  radcnvlem1  22784  radcnvlem2  22785  radcnvlt1  22789  radcnvle  22791  dvradcnv  22792  pserulm  22793  abelthlem2  22803  abelthlem5  22806  abelthlem7  22809  abelth2  22813  reeff1olem  22817  efcvx  22820  pilem2  22823  pilem3  22824  sincosq2sgn  22868  sincosq3sgn  22869  sincosq4sgn  22870  coseq0negpitopi  22872  tanrpcl  22873  tangtx  22874  tanabsge  22875  sinq12gt0  22876  sinq34lt0t  22878  cosq14gt0  22879  cosq14ge0  22880  pige3  22886  coskpi  22889  sineq0  22890  cosordlem  22894  sinord  22897  tanord1  22900  tanord  22901  tanregt0  22902  efif1olem2  22906  efif1olem4  22908  eff1olem  22911  rzgrp  22917  logrnaddcl  22938  logneg  22948  lognegb  22950  reexplog  22955  relogexp  22956  logfac  22961  efiarg  22968  cosargd  22969  cosarg0d  22970  argregt0  22971  argrege0  22972  argimgt0  22973  logneg2  22976  logmul2  22977  logdiv2  22978  abslogle  22979  tanarg  22980  logdivlti  22981  divlogrlim  22992  logcnlem2  23000  logcnlem3  23001  logcnlem4  23002  logcn  23004  logf1o2  23007  advlog  23011  advlogexp  23012  efopnlem1  23013  logtayllem  23016  logtayl  23017  logccv  23020  logcxp  23026  mulcxp  23042  divcxp  23044  cxpmul  23045  cxproot  23047  cxpmul2z  23048  abscxp  23049  abscxp2  23050  cxplt  23051  cxplea  23053  cxple2  23054  cxple2a  23056  cxplt3  23057  cxpsqrtlem  23059  cxpsqrt  23060  logsqrt  23061  dvcxp2  23093  cxpcn3lem  23097  resqrtcn  23099  cxpaddlelem  23101  cxpaddle  23102  abscxpbnd  23103  root1id  23104  root1eq1  23105  root1cj  23106  cxpeq  23107  loglesqrt  23108  cosangneg2d  23115  angrtmuld  23116  ang180lem2  23118  lawcoslem1  23123  lawcos  23124  pythag  23125  isosctrlem1  23128  isosctrlem2  23129  isosctrlem3  23130  ssscongptld  23132  chordthmlem  23139  chordthmlem2  23140  chordthmlem3  23141  chordthmlem4  23142  chordthmlem5  23143  heron  23145  asinsinlem  23198  reasinsin  23203  acosrecl  23210  atancj  23217  atanrecl  23218  atanlogaddlem  23220  atanlogsublem  23222  atanbndlem  23232  atans2  23238  ressatans  23241  atantayl  23244  leibpilem2  23248  leibpi  23249  leibpisum  23250  log2tlbnd  23252  log2ublem2  23254  birthdaylem2  23258  birthdaylem3  23259  cxp2limlem  23281  cxp2lim  23282  cxploglim  23283  cxploglim2  23284  divsqrtsumo1  23289  cvxcl  23290  scvxcvx  23291  jensenlem2  23293  jensen  23294  amgmlem  23295  logdiflbnd  23300  emcllem2  23302  emcllem3  23303  emcllem5  23305  emcllem6  23306  emcllem7  23307  harmonicbnd4  23316  fsumharmonic  23317  ftalem1  23322  ftalem2  23323  ftalem4  23325  ftalem5  23326  basellem3  23332  basellem4  23333  basellem5  23334  basellem6  23335  basellem7  23336  basellem8  23337  basellem9  23338  efnnfsumcl  23352  chtprm  23403  chpp1  23405  chtdif  23408  efchtdvds  23409  prmorcht  23428  mumullem2  23430  fsumfldivdiaglem  23441  ppiub  23455  chtleppi  23461  chtublem  23462  chtub  23463  pclogsum  23466  vmasum  23467  logfac2  23468  chpval2  23469  chpchtsum  23470  chpub  23471  logfaclbnd  23473  logfacbnd3  23474  logfacrlim  23475  logexprlim  23476  logfacrlim2  23477  mersenne  23478  dchrabs  23511  dchrptlem1  23515  dchrptlem2  23516  bcmax  23529  bcp1ctr  23530  bposlem1  23535  bposlem9  23543  lgsvalmod  23566  lgsdilem  23573  lgsne0  23584  lgsqrlem2  23593  lgseisenlem1  23600  lgseisenlem2  23601  lgseisen  23604  lgsquadlem1  23605  lgsquadlem2  23606  mul2sq  23616  2sqlem3  23617  2sqlem8  23623  chebbnd1lem1  23630  chebbnd1lem2  23631  chebbnd1lem3  23632  chtppilimlem1  23634  chtppilimlem2  23635  chtppilim  23636  chto1ub  23637  chto1lb  23639  chpchtlim  23640  chpo1ub  23641  vmadivsum  23643  vmadivsumb  23644  rplogsumlem1  23645  rplogsumlem2  23646  rpvmasumlem  23648  dchrisumlema  23649  dchrisumlem1  23650  dchrisumlem2  23651  dchrisumlem3  23652  dchrmusumlema  23654  dchrmusum2  23655  dchrvmasumlem1  23656  dchrvmasum2lem  23657  dchrvmasum2if  23658  dchrvmasumlem2  23659  dchrvmasumlem3  23660  dchrvmasumiflem1  23662  dchrvmasumiflem2  23663  dchrisum0flblem1  23669  dchrisum0fno1  23672  rpvmasum2  23673  dchrisum0re  23674  dchrisum0lema  23675  dchrisum0lem1b  23676  dchrisum0lem1  23677  dchrisum0lem2a  23678  dchrisum0lem2  23679  dchrisum0lem3  23680  dchrmusumlem  23683  dchrvmasumlem  23684  rpvmasum  23687  rplogsum  23688  dirith2  23689  mudivsum  23691  mulogsumlem  23692  mulogsum  23693  logdivsum  23694  mulog2sumlem1  23695  mulog2sumlem2  23696  mulog2sumlem3  23697  vmalogdivsum2  23699  vmalogdivsum  23700  2vmadivsumlem  23701  logsqvma  23703  logsqvma2  23704  log2sumbnd  23705  selberglem1  23706  selberglem2  23707  selberglem3  23708  selberg  23709  selbergb  23710  selberg2lem  23711  selberg2  23712  selberg2b  23713  chpdifbndlem1  23714  logdivbnd  23717  selberg3lem1  23718  selberg3lem2  23719  selberg3  23720  selberg4lem1  23721  selberg4  23722  pntrmax  23725  pntrsumo1  23726  pntrsumbnd  23727  pntrsumbnd2  23728  selbergr  23729  selberg3r  23730  selberg4r  23731  selberg34r  23732  pntsval2  23737  pntrlog2bndlem1  23738  pntrlog2bndlem2  23739  pntrlog2bndlem3  23740  pntrlog2bndlem4  23741  pntrlog2bndlem5  23742  pntrlog2bndlem6a  23743  pntrlog2bndlem6  23744  pntrlog2bnd  23745  pntpbnd1a  23746  pntpbnd1  23747  pntpbnd2  23748  pntibndlem2  23752  pntibndlem3  23753  pntlemb  23758  pntlemg  23759  pntlemh  23760  pntlemn  23761  pntlemr  23763  pntlemj  23764  pntlemf  23766  pntlemk  23767  pntlemo  23768  pntlem3  23770  pntleml  23772  pnt2  23774  pnt  23775  abvcxp  23776  ostth2lem1  23779  qabvexp  23787  padicabv  23791  padicabvcxp  23793  ostth2lem2  23795  ostth2lem3  23796  ostth2lem4  23797  ostth2  23798  ostth3  23799  ttgcontlem1  24164  fveecn  24181  eqeelen  24183  brbtwn2  24184  colinearalglem4  24188  colinearalg  24189  axsegconlem9  24204  axsegconlem10  24205  ax5seglem1  24207  ax5seglem2  24208  ax5seglem3  24210  ax5seglem5  24212  ax5seglem6  24213  ax5seglem9  24216  ax5seg  24217  axbtwnid  24218  axpaschlem  24219  axpasch  24220  axeuclidlem  24241  axcontlem2  24244  axcontlem4  24246  axcontlem7  24249  axcontlem8  24250  eupap1  24952  nvm1  25543  nvpi  25545  nvz0  25547  nvmtri  25550  nvabs  25552  nvge0  25553  nv1  25555  smcnlem  25583  ipval2lem4  25592  ipval2  25593  4ipval2  25594  4ipval3  25598  ipidsq  25599  dipcj  25603  dip0r  25606  ipz  25608  nmoub3i  25664  nmlno0lem  25684  nmblolbii  25690  blocnilem  25695  cncph  25710  ipasslem4  25725  ipasslem5  25726  ipblnfi  25747  minvecolem2  25767  minvecolem4  25772  minvecolem6  25774  minvecolem7  25775  htthlem  25810  normpyc  26039  hhph  26071  bcs2  26075  norm1  26143  norm1exi  26144  pjhthlem1  26285  eigvalcl  26856  eighmorth  26859  nmlnop0iALT  26890  nmbdoplbi  26919  nmcexi  26921  nmcoplbi  26923  nmbdfnlbi  26944  nmcfnlbi  26947  riesz4i  26958  cnlnadjlem2  26963  cnlnadjlem7  26968  nmopcoi  26990  nmopcoadji  26996  branmfn  27000  leopnmid  27033  opsqrlem1  27035  hst1h  27122  hstle  27125  hstoh  27127  sto2i  27132  stadd3i  27143  strlem1  27145  golem1  27166  stcltrlem1  27171  cdj1i  27328  cdj3lem1  27329  cdj3lem3b  27335  cdj3i  27336  lt2addrd  27539  mul2lt0rlt0  27541  mul2lt0rgt0  27542  mul2lt0llt0  27543  mul2lt0lgt0  27544  mul2lt0bi  27545  le2halvesd  27552  fzsplit3  27575  bcm1n  27576  bhmafibid1  27609  bhmafibid2  27610  2sqmod  27613  regsumfsum  27749  elunitcn  27857  sqsscirc1  27867  sqsscirc2  27868  cnre2csqima  27870  rmulccn  27887  xrge0iifcnv  27892  xrge0iifhom  27896  zrhnm  27927  rezh  27929  nexple  27982  nnlogbexp  27997  logbrec  27998  indsum  28013  esumpcvgval  28061  dya2ub  28218  dya2icoseg  28225  eulerpartlemgc  28278  ballotlemsi  28430  sgnmul  28458  sgnsub  28460  eluzmn  28468  plymulx0  28481  signsply0  28485  signsvtp  28517  signsvtn  28518  signsvfpn  28519  signsvfnn  28520  zetacvg  28534  lgamgulmlem2  28549  lgamgulmlem3  28550  lgamgulmlem4  28551  lgamgulmlem5  28552  lgamgulmlem6  28553  lgamgulm2  28555  lgambdd  28556  lgamcvg2  28574  gamcvg  28575  gamcvg2lem  28578  regamcl  28580  relgamcl  28581  lgam1  28583  subfacval2  28608  subfaclim  28609  subfacval3  28610  rescon  28668  sinccvglem  29015  circum  29017  possumd  29093  climlec3  29097  faclimlem1  29143  faclimlem2  29144  faclimlem3  29145  faclim  29146  iprodfac  29147  faclim2  29148  bpolydiflem  29791  bpoly4  29796  supadd  30017  ltflcei  30018  sin2h  30020  cos2h  30021  tan2h  30022  opnmbllem0  30025  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  mbfposadd  30037  itg2addnclem  30041  itg2addnclem2  30042  itg2addnclem3  30043  itg2addnc  30044  itg2gt0cn  30045  ibladdnc  30047  itgaddnclem2  30049  iblabsnclem  30053  iblabsnc  30054  iblmulc2nc  30055  itgmulc2nclem2  30057  itgmulc2nc  30058  itgabsnc  30059  bddiblnc  30060  ftc1cnnclem  30063  ftc1cnnc  30064  ftc1anclem1  30065  ftc1anclem2  30066  ftc1anclem3  30067  ftc1anclem4  30068  ftc1anclem5  30069  ftc1anclem6  30070  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  areacirclem1  30082  areacirclem5  30086  areacirc  30087  mettrifi  30225  lmclim2  30226  geomcau  30227  isbnd3  30255  ssbnd  30259  cntotbnd  30267  bfplem1  30293  bfplem2  30294  bfp  30295  rrnmet  30300  rrndstprj1  30301  rrndstprj2  30302  rrncmslem  30303  rrnequiv  30306  rrntotbnd  30307  ismrer1  30309  eldioph2lem1  30668  lzenom  30678  rencldnfilem  30729  icodiamlt  30731  irrapxlem1  30733  irrapxlem2  30734  irrapxlem3  30735  irrapxlem4  30736  irrapxlem5  30737  pellexlem2  30741  pellexlem6  30745  pell1234qrreccl  30765  pell14qrgt0  30770  pell14qrdivcl  30776  pell14qrexpclnn0  30777  pell14qrexpcl  30778  pell14qrdich  30780  pell1qrgaplem  30784  pellfundex  30797  reglogmul  30804  reglogexp  30805  reglogbas  30806  reglog1  30807  pellfund14  30809  rmspecsqrtnq  30817  rmspecfund  30820  monotoddzzfi  30853  expmordi  30858  jm2.24nn  30872  jm2.17a  30873  jm2.17b  30874  jm2.17c  30875  jm2.24  30876  acongrep  30893  fzmaxdif  30894  acongeq  30896  modabsdifz  30902  jm2.19lem4  30909  jm2.19  30910  jm2.26lem3  30918  jm3.1lem1  30934  jm3.1lem2  30935  itgpowd  31158  areaquad  31160  cvgdvgrat  31170  radcnvrat  31171  hashnzfzclim  31203  dvconstbi  31215  oddfl  31408  dstregt0  31412  zltlesub  31417  lt2addmuld  31422  sublt0d  31444  lt3addmuld  31450  fperiodmullem  31452  fperiodmul  31453  lt4addmuld  31455  iooabslt  31468  iccshift  31494  iooshift  31498  fmul01  31502  fmul01lt1lem1  31506  fmul01lt1lem2  31507  climinf  31520  limcrecl  31543  lptre2pt  31554  limcleqr  31558  0ellimcdiv  31563  limclner  31565  sinaover2ne0  31575  cncfperiod  31588  ioccncflimc  31595  cncficcgt0  31598  icocncflimc  31599  cncfshiftioo  31602  cncfiooicc  31604  fperdvper  31619  dvbdfbdioolem1  31629  dvbdfbdioolem2  31630  dvbdfbdioo  31631  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc1  31634  ioodvbdlimc2lem  31635  ioodvbdlimc2  31636  itgcoscmulx  31658  volioc  31661  itgsincmulx  31663  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  stoweidlem7  31678  stoweidlem11  31682  stoweidlem13  31684  stoweidlem17  31688  stoweidlem19  31690  stoweidlem20  31691  stoweidlem21  31692  stoweidlem22  31693  stoweidlem23  31694  stoweidlem24  31695  stoweidlem26  31697  stoweidlem32  31703  stoweidlem36  31707  stoweidlem44  31715  stoweidlem47  31718  wallispilem3  31738  wallispi2lem1  31742  stirlinglem1  31745  stirlinglem5  31749  stirlinglem11  31755  stirlinglem12  31756  stirlinglem14  31758  dirkerval2  31765  dirkerre  31766  dirkertrigeqlem2  31770  dirkertrigeq  31772  dirkeritg  31773  dirkercncflem1  31774  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem4  31782  fourierdlem6  31784  fourierdlem7  31785  fourierdlem13  31791  fourierdlem14  31792  fourierdlem16  31794  fourierdlem18  31796  fourierdlem19  31797  fourierdlem21  31799  fourierdlem22  31800  fourierdlem24  31802  fourierdlem26  31804  fourierdlem28  31806  fourierdlem30  31808  fourierdlem35  31813  fourierdlem39  31817  fourierdlem40  31818  fourierdlem41  31819  fourierdlem42  31820  fourierdlem43  31821  fourierdlem44  31822  fourierdlem47  31825  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem53  31831  fourierdlem56  31834  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem60  31838  fourierdlem61  31839  fourierdlem62  31840  fourierdlem63  31841  fourierdlem64  31842  fourierdlem65  31843  fourierdlem66  31844  fourierdlem68  31846  fourierdlem70  31848  fourierdlem71  31849  fourierdlem72  31850  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem77  31855  fourierdlem78  31856  fourierdlem79  31857  fourierdlem80  31858  fourierdlem81  31859  fourierdlem83  31861  fourierdlem84  31862  fourierdlem85  31863  fourierdlem87  31865  fourierdlem88  31866  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem92  31870  fourierdlem93  31871  fourierdlem95  31873  fourierdlem97  31875  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  fourierdlem109  31887  fourierdlem111  31889  fourierdlem112  31890  fouriercnp  31898  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  sigaras  31910  sigarms  31911  sigarls  31912  sigarexp  31914  sigarperm  31915  sigarimcd  31917  sigarcol  31919  sharhght  31920  cevathlem2  31923  isosctrlem1ALT  33467  sineq0ALT  33470  absmulrposd  37640  extoimad  37650  imo72b2lem0  37651  imo72b2lem1  37657  imo72b2  37662