Theorem recnd 9621

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 9581	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 16	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1767   CCcc 9489   RRcr 9490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9548

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  00id  9753  mul02lem1  9754  addid1  9758  cnegex  9759  ltadd1  10018  leadd2  10020  ltsubadd  10021  ltsubadd2  10022  lesubadd  10023  lesubadd2  10024  lesub1  10045  lesub2  10046  ltnegcon1  10052  ltnegcon2  10053  add20  10063  subge0  10064  suble0  10065  lesub0  10068  mulge0  10069  eqord2  10083  rereccl  10261  redivcl  10262  recgt0  10385  prodgt0  10386  prodge0  10388  ltmul1a  10390  ltdiv1  10405  ltmuldiv  10414  ltrec  10425  recp1lt1  10442  recreclt  10443  ledivp1  10446  infmsup  10520  infmrcl  10521  rimul  10526  cru  10527  avglt1  10775  avglt2  10776  nn0cnd  10853  zcn  10868  zeo  10945  zcnd  10966  eluzelcn  11092  cnref1o  11214  rpcn  11227  rpcnd  11257  ltaddrp2d  11285  qbtwnre  11397  xralrple  11403  xpncan  11442  xmulcom  11457  xmulneg1  11460  xlemul1  11481  icoshftf1o  11642  lincmb01cmp  11662  iccf1o  11663  fladdz  11925  flzadd  11926  flhalf  11929  ceim1l  11941  intfracq  11953  fldiv  11954  modvalr  11966  flpmodeq  11968  mod0  11970  modlt  11973  moddiffl  11974  modfrac  11976  flmod  11977  intfrac  11978  modmulnn  11980  modvalp1  11981  modid  11987  modcyc  11998  modadd1  12000  modaddabs  12001  modadd2mod  12004  modnegd  12009  modadd12d  12010  modsub12d  12011  modaddmulmod  12020  moddi  12021  modsubdir  12022  modeqmodmin  12023  modirr  12024  seqf1olem1  12113  serle  12129  expcl2lem  12145  expnegz  12167  expaddzlem  12176  expaddz  12177  expmulz  12179  ltexp2a  12184  leexp2a  12188  leexp2r  12190  exple1  12192  expubnd  12193  sq11  12207  bernneq2  12260  expmulnbnd  12265  discr1  12269  discr  12270  faclbnd  12335  bcp1nk  12362  cshweqrep  12751  remim  12912  reim0b  12914  rereb  12915  mulre  12916  cjreb  12918  recj  12919  reneg  12920  readd  12921  resub  12922  remullem  12923  remul2  12925  rediv  12926  imcj  12927  imneg  12928  imadd  12929  imsub  12930  immul2  12932  imdiv  12933  cjcj  12935  cjadd  12936  ipcnval  12938  cjmulval  12940  cjneg  12942  imval2  12946  cjreim2  12956  sqr0lem  13036  sqrlem5  13042  sqrlem7  13044  resqrtthlem  13050  remsqsqrt  13052  sqrtmul  13055  sqrtdiv  13061  sqrtneg  13063  sqrtmsq  13066  absdiv  13090  absid  13091  absexp  13099  absexpz  13100  absimle  13104  abslt  13109  absle  13110  abssubne0  13111  releabs  13116  recval  13117  abstri  13125  abs2difabs  13129  abs1m  13130  abslem2  13134  absrdbnd  13136  sqreulem  13154  sqreu  13155  amgm2  13164  lo1bddrp  13310  o1lo1  13322  rlimrecl  13365  rlimge0  13366  climrecl  13368  climge0  13369  climabs0  13370  reccn2  13381  o1rlimmul  13403  lo1mul2  13413  lo1sub  13415  climle  13424  climsqz  13425  climsqz2  13426  rlimsqz  13434  rlimsqz2  13435  rlimno1  13438  climlec2  13443  isercolllem1  13449  climsup  13454  caucvgrlem  13457  caurcvgr  13458  caucvgrlem2  13459  iseraltlem1  13466  iseraltlem2  13467  iseraltlem3  13468  iseralt  13469  isumrecl  13542  isumge0  13543  fsumless  13572  fsumge1  13573  fsum00  13574  fsumle  13575  fsumlt  13576  fsumabs  13577  o1fsum  13589  seqabs  13590  cvgcmp  13592  cvgcmpce  13594  abscvgcvg  13595  isumrpcl  13617  isumle  13618  isumless  13619  isumsup  13621  climcndslem1  13623  climcndslem2  13624  climcnds  13625  flo1  13628  supcvg  13629  trireciplem  13635  trirecip  13636  explecnv  13638  geo2sum  13644  geo2lim  13646  geomulcvg  13647  cvgrat  13654  mertenslem1  13655  mertenslem2  13656  efcllem  13674  ege2le3  13686  efaddlem  13689  efgt0  13698  eftlub  13704  effsumlt  13706  eflt  13712  eflegeo  13716  resin4p  13733  recos4p  13734  retanhcl  13754  tanhlt1  13755  efeul  13757  ef01bndlem  13779  sin01bnd  13780  cos01bnd  13781  sin01gt0  13785  cos01gt0  13786  sin02gt0  13787  absefi  13791  absef  13792  absefib  13793  efieq1re  13794  eirrlem  13797  rpnnen2lem5  13812  rpnnen2lem8  13815  rpnnen2lem9  13816  rpnnen2lem11  13818  rpnnen2  13819  moddvds  13853  odd2np1  13904  divalglem5  13913  bitsp1o  13941  bitsfzo  13943  bitscmp  13946  sadcaddlem  13965  nn0seqcvgd  14057  sqnprm  14097  isprm5  14111  nonsq  14150  eulerthlem2  14170  prmdiveq  14174  odzdvds  14180  pythagtriplem14  14210  pcid  14254  fldivp1  14274  pcfac  14276  pockthlem  14281  prmreclem3  14294  prmreclem4  14295  prmreclem5  14296  prmrec  14298  4sqlem5  14318  4sqlem10  14323  mul4sqlem  14329  4sqlem15  14335  4sqlem16  14336  mulgneg  15967  ghmmulg  16081  odmodnn0  16367  mndodconglem  16368  pgpfaclem2  16932  isabvd  17264  abv1z  17276  abvneg  17278  abvrec  17280  abvdiv  17281  abvdom  17282  rege0subm  18258  cnsubrg  18262  gzrngunitlem  18266  prmirredlem  18306  prmirredlemOLD  18309  remulg  18426  regsumsupp  18441  bl2in  20654  blhalf  20659  blssps  20678  blss  20679  methaus  20774  nrmmetd  20846  nm2dif  20895  nminvr  20929  nmdvr  20930  nlmmul0or  20943  nrginvrcnlem  20950  nmolb2d  20976  nmoi2  20988  nmoleub  20989  nmo0  20993  nmoeq0  20994  nmoco  20995  nmotri  20997  nmoid  21000  blcvx  21054  xrsxmet  21065  recld2  21070  reconnlem2  21083  opnreen  21087  metdstri  21106  metnrmlem3  21116  icchmeo  21192  icopnfcnv  21193  icopnfhmeo  21194  iccpnfhmeo  21196  xrhmeo  21197  icccvx  21201  cnheiborlem  21205  evth  21210  lebnumii  21217  pcoass  21275  pcorevlem  21277  pcorev2  21279  pi1xfrcnv  21308  nmoleub2lem  21348  nmoleub2lem3  21349  nmoleub3  21353  cphsqrtcl2  21384  ipcau2  21428  tchcphlem1  21429  tchcphlem2  21430  tchcph  21431  iscau3  21468  rrxnm  21574  rrxcph  21575  csbren  21577  trirn  21578  rrxmval  21583  rrxmetlem  21585  rrxmet  21586  rrxdstprj1  21587  minveclem2  21592  minveclem3b  21594  minveclem4  21598  minveclem6  21600  minveclem7  21601  pjthlem1  21603  ivthlem2  21615  ivthlem3  21616  ivth2  21618  ovolfsval  21633  ovollb2lem  21650  ovolctb  21652  ovolunlem1a  21658  ovolunnul  21662  ovolfiniun  21663  ovoliunlem1  21664  ovoliun2  21668  shft2rab  21670  ovolshftlem1  21671  sca2rab  21674  ovolscalem1  21675  ovolsca  21677  ovolicc1  21678  ovolicc2lem4  21682  ovolicopnf  21686  cmmbl  21696  nulmbl  21697  nulmbl2  21698  unmbl  21699  volinun  21707  volfiniun  21708  voliunlem1  21711  voliunlem3  21713  ioombl1lem3  21721  ioombl1lem4  21722  ovolioo  21729  ioorcl2  21732  uniioovol  21739  uniioombllem3  21745  uniioombllem4  21746  uniioombllem5  21747  uniioombllem6  21748  dyadovol  21753  dyaddisjlem  21755  opnmbllem  21761  vitalilem1  21768  vitalilem2  21769  vitalilem3  21770  vitalilem4  21771  ismbf  21788  mbfmulc2lem  21805  mbfmulc2re  21806  mbfmulc2  21821  mbfinf  21823  itg1val2  21842  itg11  21849  i1fmullem  21852  i1fadd  21853  itg1addlem4  21857  itg1addlem5  21858  i1fmulclem  21860  i1fmulc  21861  itg1mulc  21862  itg1sub  21867  itg10a  21868  itg1ge0a  21869  itg1climres  21872  mbfi1fseqlem3  21875  mbfi1fseqlem4  21876  mbfi1fseqlem5  21877  mbfi1fseqlem6  21878  mbfi1flimlem  21880  mbfmullem2  21882  itg2const  21898  itg2const2  21899  itg2mulclem  21904  itg2mulc  21905  itg2splitlem  21906  itg2split  21907  itg2monolem1  21908  itg2monolem3  21910  itg2addlem  21916  itgcl  21941  itgcnlem  21947  itgrevallem1  21952  itgposval  21953  iblneg  21960  itgneg  21961  i1fibl  21965  itgitg1  21966  itgconst  21976  ibladd  21978  itgaddlem2  21981  iblabslem  21985  iblabs  21986  iblabsr  21987  iblmulc2  21988  itgmulc2lem2  21990  itgmulc2  21991  itgabs  21992  itgsplit  21993  bddmulibl  21996  dvcjbr  22103  dvfre  22105  dvexp3  22130  dveflem  22131  dvferm1lem  22136  dvferm2lem  22138  rolle  22142  cmvth  22143  mvth  22144  dvlip  22145  dvlipcn  22146  c1liplem1  22148  c1lip1  22149  dveq0  22152  dv11cn  22153  dvlt0  22157  dvle  22159  dvivthlem1  22160  dvivth  22162  lhop1lem  22165  lhop1  22166  lhop2  22167  lhop  22168  dvcvx  22172  dvfsumle  22173  dvfsumge  22174  dvfsumabs  22175  dvfsumlem1  22178  dvfsumlem2  22179  dvfsumlem4  22181  dvfsumrlimge0  22182  dvfsumrlim2  22184  dvfsum2  22186  ftc1a  22189  ftc1lem4  22191  ftc1lem5  22192  plyeq0lem  22358  coemulhi  22401  plyrecj  22426  plydivlem3  22441  aalioulem2  22479  aalioulem3  22480  aalioulem4  22481  aalioulem5  22482  aalioulem6  22483  aaliou  22484  aaliou2  22486  aaliou2b  22487  aaliou3lem3  22490  aaliou3lem7  22495  aaliou3lem9  22496  taylthlem2  22519  ulmcn  22544  ulmdvlem1  22545  mtest  22549  mtestbdd  22550  itgulm  22553  radcnvlem1  22558  radcnvlem2  22559  radcnvlt1  22563  radcnvle  22565  dvradcnv  22566  pserulm  22567  abelthlem2  22577  abelthlem5  22580  abelthlem7  22583  abelth2  22587  reeff1olem  22591  efcvx  22594  pilem2  22597  pilem3  22598  sincosq2sgn  22641  sincosq3sgn  22642  sincosq4sgn  22643  coseq0negpitopi  22645  tanrpcl  22646  tangtx  22647  tanabsge  22648  sinq12gt0  22649  sinq34lt0t  22651  cosq14gt0  22652  cosq14ge0  22653  pige3  22659  coskpi  22662  sineq0  22663  cosordlem  22667  sinord  22670  tanord1  22673  tanord  22674  tanregt0  22675  efif1olem2  22679  efif1olem4  22681  eff1olem  22684  logrnaddcl  22706  logneg  22716  lognegb  22718  reexplog  22723  relogexp  22724  logfac  22729  efiarg  22736  cosargd  22737  cosarg0d  22738  argregt0  22739  argrege0  22740  argimgt0  22741  logneg2  22744  logmul2  22745  logdiv2  22746  abslogle  22747  tanarg  22748  logdivlti  22749  divlogrlim  22760  logcnlem2  22768  logcnlem3  22769  logcnlem4  22770  logcn  22772  logf1o2  22775  advlog  22779  advlogexp  22780  efopnlem1  22781  logtayllem  22784  logtayl  22785  logccv  22788  logcxp  22794  mulcxp  22810  divcxp  22812  cxpmul  22813  cxproot  22815  cxpmul2z  22816  abscxp  22817  abscxp2  22818  cxplt  22819  cxplea  22821  cxple2  22822  cxple2a  22824  cxplt3  22825  cxpsqrtlem  22827  cxpsqrt  22828  logsqrt  22829  dvcxp2  22861  cxpcn3lem  22865  resqrtcn  22867  cxpaddlelem  22869  cxpaddle  22870  abscxpbnd  22871  root1id  22872  root1eq1  22873  root1cj  22874  cxpeq  22875  loglesqrt  22876  cosangneg2d  22883  angrtmuld  22884  ang180lem2  22886  lawcoslem1  22891  lawcos  22892  pythag  22893  isosctrlem1  22896  isosctrlem2  22897  isosctrlem3  22898  ssscongptld  22900  chordthmlem  22907  chordthmlem2  22908  chordthmlem3  22909  chordthmlem4  22910  chordthmlem5  22911  heron  22913  asinsinlem  22966  reasinsin  22971  acosrecl  22978  atancj  22985  atanrecl  22986  atanlogaddlem  22988  atanlogsublem  22990  atanbndlem  23000  atans2  23006  ressatans  23009  atantayl  23012  leibpilem2  23016  leibpi  23017  leibpisum  23018  log2tlbnd  23020  log2ublem2  23022  birthdaylem2  23026  birthdaylem3  23027  cxp2limlem  23049  cxp2lim  23050  cxploglim  23051  cxploglim2  23052  divsqrtsumo1  23057  cvxcl  23058  scvxcvx  23059  jensenlem2  23061  jensen  23062  amgmlem  23063  logdiflbnd  23068  emcllem2  23070  emcllem3  23071  emcllem5  23073  emcllem6  23074  emcllem7  23075  harmonicbnd4  23084  fsumharmonic  23085  ftalem1  23090  ftalem2  23091  ftalem4  23093  ftalem5  23094  basellem3  23100  basellem4  23101  basellem5  23102  basellem6  23103  basellem7  23104  basellem8  23105  basellem9  23106  efnnfsumcl  23120  chtprm  23171  chpp1  23173  chtdif  23176  efchtdvds  23177  prmorcht  23196  mumullem2  23198  fsumfldivdiaglem  23209  ppiub  23223  chtleppi  23229  chtublem  23230  chtub  23231  pclogsum  23234  vmasum  23235  logfac2  23236  chpval2  23237  chpchtsum  23238  chpub  23239  logfaclbnd  23241  logfacbnd3  23242  logfacrlim  23243  logexprlim  23244  logfacrlim2  23245  mersenne  23246  dchrabs  23279  dchrptlem1  23283  dchrptlem2  23284  bcmax  23297  bcp1ctr  23298  bposlem1  23303  bposlem9  23311  lgsvalmod  23334  lgsdilem  23341  lgsne0  23352  lgsqrlem2  23361  lgseisenlem1  23368  lgseisenlem2  23369  lgseisen  23372  lgsquadlem1  23373  lgsquadlem2  23374  mul2sq  23384  2sqlem3  23385  2sqlem8  23391  chebbnd1lem1  23398  chebbnd1lem2  23399  chebbnd1lem3  23400  chtppilimlem1  23402  chtppilimlem2  23403  chtppilim  23404  chto1ub  23405  chto1lb  23407  chpchtlim  23408  chpo1ub  23409  vmadivsum  23411  vmadivsumb  23412  rplogsumlem1  23413  rplogsumlem2  23414  rpvmasumlem  23416  dchrisumlema  23417  dchrisumlem1  23418  dchrisumlem2  23419  dchrisumlem3  23420  dchrmusumlema  23422  dchrmusum2  23423  dchrvmasumlem1  23424  dchrvmasum2lem  23425  dchrvmasum2if  23426  dchrvmasumlem2  23427  dchrvmasumlem3  23428  dchrvmasumiflem1  23430  dchrvmasumiflem2  23431  dchrisum0flblem1  23437  dchrisum0fno1  23440  rpvmasum2  23441  dchrisum0re  23442  dchrisum0lema  23443  dchrisum0lem1b  23444  dchrisum0lem1  23445  dchrisum0lem2a  23446  dchrisum0lem2  23447  dchrisum0lem3  23448  dchrmusumlem  23451  dchrvmasumlem  23452  rpvmasum  23455  rplogsum  23456  dirith2  23457  mudivsum  23459  mulogsumlem  23460  mulogsum  23461  logdivsum  23462  mulog2sumlem1  23463  mulog2sumlem2  23464  mulog2sumlem3  23465  vmalogdivsum2  23467  vmalogdivsum  23468  2vmadivsumlem  23469  logsqvma  23471  logsqvma2  23472  log2sumbnd  23473  selberglem1  23474  selberglem2  23475  selberglem3  23476  selberg  23477  selbergb  23478  selberg2lem  23479  selberg2  23480  selberg2b  23481  chpdifbndlem1  23482  logdivbnd  23485  selberg3lem1  23486  selberg3lem2  23487  selberg3  23488  selberg4lem1  23489  selberg4  23490  pntrmax  23493  pntrsumo1  23494  pntrsumbnd  23495  pntrsumbnd2  23496  selbergr  23497  selberg3r  23498  selberg4r  23499  selberg34r  23500  pntsval2  23505  pntrlog2bndlem1  23506  pntrlog2bndlem2  23507  pntrlog2bndlem3  23508  pntrlog2bndlem4  23509  pntrlog2bndlem5  23510  pntrlog2bndlem6a  23511  pntrlog2bndlem6  23512  pntrlog2bnd  23513  pntpbnd1a  23514  pntpbnd1  23515  pntpbnd2  23516  pntibndlem2  23520  pntibndlem3  23521  pntlemb  23526  pntlemg  23527  pntlemh  23528  pntlemn  23529  pntlemr  23531  pntlemj  23532  pntlemf  23534  pntlemk  23535  pntlemo  23536  pntlem3  23538  pntleml  23540  pnt2  23542  pnt  23543  abvcxp  23544  ostth2lem1  23547  qabvexp  23555  padicabv  23559  padicabvcxp  23561  ostth2lem2  23563  ostth2lem3  23564  ostth2lem4  23565  ostth2  23566  ostth3  23567  ttgcontlem1  23880  fveecn  23897  eqeelen  23899  brbtwn2  23900  colinearalglem4  23904  colinearalg  23905  axsegconlem9  23920  axsegconlem10  23921  ax5seglem1  23923  ax5seglem2  23924  ax5seglem3  23926  ax5seglem5  23928  ax5seglem6  23929  ax5seglem9  23932  ax5seg  23933  axbtwnid  23934  axpaschlem  23935  axpasch  23936  axeuclidlem  23957  axcontlem2  23960  axcontlem4  23962  axcontlem7  23965  axcontlem8  23966  eupap1  24668  nvm1  25259  nvpi  25261  nvz0  25263  nvmtri  25266  nvabs  25268  nvge0  25269  nv1  25271  smcnlem  25299  ipval2lem4  25308  ipval2  25309  4ipval2  25310  4ipval3  25314  ipidsq  25315  dipcj  25319  dip0r  25322  ipz  25324  nmoub3i  25380  nmlno0lem  25400  nmblolbii  25406  blocnilem  25411  cncph  25426  ipasslem4  25441  ipasslem5  25442  ipblnfi  25463  minvecolem2  25483  minvecolem4  25488  minvecolem6  25490  minvecolem7  25491  htthlem  25526  normpyc  25755  hhph  25787  bcs2  25791  norm1  25859  norm1exi  25860  pjhthlem1  26001  eigvalcl  26572  eighmorth  26575  nmlnop0iALT  26606  nmbdoplbi  26635  nmcexi  26637  nmcoplbi  26639  nmbdfnlbi  26660  nmcfnlbi  26663  riesz4i  26674  cnlnadjlem2  26679  cnlnadjlem7  26684  nmopcoi  26706  nmopcoadji  26712  branmfn  26716  leopnmid  26749  opsqrlem1  26751  hst1h  26838  hstle  26841  hstoh  26843  sto2i  26848  stadd3i  26859  strlem1  26861  golem1  26882  stcltrlem1  26887  cdj1i  27044  cdj3lem1  27045  cdj3lem3b  27051  cdj3i  27052  lt2addrd  27247  mul2lt0rlt0  27249  mul2lt0rgt0  27250  mul2lt0llt0  27251  mul2lt0lgt0  27252  mul2lt0bi  27253  le2halvesd  27260  fzsplit3  27283  bcm1n  27284  elunitcn  27532  sqsscirc1  27542  sqsscirc2  27543  cnre2csqima  27545  rmulccn  27562  xrge0iifcnv  27567  xrge0iifhom  27571  zrhnm  27602  nexple  27661  nnlogbexp  27676  logbrec  27677  indsum  27692  esumpcvgval  27740  dya2ub  27897  dya2icoseg  27904  eulerpartlemgc  27957  ballotlemsi  28109  sgnmul  28137  sgnsub  28139  eluzmn  28147  signsvtp  28196  signsvtn  28197  signsvfpn  28198  signsvfnn  28199  zetacvg  28213  lgamgulmlem2  28228  lgamgulmlem3  28229  lgamgulmlem4  28230  lgamgulmlem5  28231  lgamgulmlem6  28232  lgamgulm2  28234  lgambdd  28235  lgamcvg2  28253  gamcvg  28254  gamcvg2lem  28257  regamcl  28259  relgamcl  28260  lgam1  28262  subfacval2  28287  subfaclim  28288  subfacval3  28289  rescon  28347  sinccvglem  28529  circum  28531  possumd  28608  climlec3  28613  fprodabs  28696  iprodrecl  28714  faclimlem1  28761  faclimlem2  28762  faclimlem3  28763  faclim  28764  iprodfac  28765  faclim2  28766  bpolydiflem  29409  bpoly4  29414  supadd  29635  ltflcei  29636  sin2h  29638  cos2h  29639  tan2h  29640  opnmbllem0  29643  mblfinlem2  29645  mblfinlem3  29646  mblfinlem4  29647  mbfposadd  29655  itg2addnclem  29659  itg2addnclem2  29660  itg2addnclem3  29661  itg2addnc  29662  itg2gt0cn  29663  ibladdnc  29665  itgaddnclem2  29667  iblabsnclem  29671  iblabsnc  29672  iblmulc2nc  29673  itgmulc2nclem2  29675  itgmulc2nc  29676  itgabsnc  29677  bddiblnc  29678  ftc1cnnclem  29681  ftc1cnnc  29682  ftc1anclem1  29683  ftc1anclem2  29684  ftc1anclem3  29685  ftc1anclem4  29686  ftc1anclem5  29687  ftc1anclem6  29688  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  areacirclem1  29700  areacirclem5  29704  areacirc  29705  nn0prpwlem  29733  mettrifi  29869  lmclim2  29870  geomcau  29871  isbnd3  29899  ssbnd  29903  cntotbnd  29911  bfplem1  29937  bfplem2  29938  bfp  29939  rrnmet  29944  rrndstprj1  29945  rrndstprj2  29946  rrncmslem  29947  rrnequiv  29950  rrntotbnd  29951  ismrer1  29953  eldioph2lem1  30313  lzenom  30323  rencldnfilem  30374  icodiamlt  30376  irrapxlem1  30378  irrapxlem2  30379  irrapxlem3  30380  irrapxlem4  30381  irrapxlem5  30382  pellexlem2  30386  pellexlem6  30390  pell1234qrreccl  30410  pell14qrgt0  30415  pell14qrdivcl  30421  pell14qrexpclnn0  30422  pell14qrexpcl  30423  pell14qrdich  30425  pell1qrgaplem  30429  pellfundex  30442  reglogmul  30449  reglogexp  30450  reglogbas  30451  reglog1  30452  pellfund14  30454  rmspecsqrtnq  30462  rmspecfund  30465  rmym1  30491  rmyluc  30493  monotoddzzfi  30498  expmordi  30503  jm2.24nn  30517  jm2.17a  30518  jm2.17b  30519  jm2.17c  30520  jm2.24  30521  acongrep  30538  fzmaxdif  30539  acongeq  30541  modabsdifz  30547  jm2.19lem4  30554  jm2.19  30555  jm2.26lem3  30563  jm3.1lem1  30579  jm3.1lem2  30580  itgpowd  30803  areaquad  30805  hashnzfzclim  30843  dvconstbi  30855  oddfl  31052  dstregt0  31056  zltlesub  31061  lt2addmuld  31066  2timesgt  31068  sublt0d  31088  lt3addmuld  31094  fperiodmullem  31096  fperiodmul  31097  lt4addmuld  31099  iooabslt  31112  fmul01  31146  fmul01lt1lem1  31150  fmul01lt1lem2  31151  climinf  31164  limcrecl  31187  sumnnodd  31188  lptre2pt  31198  addlimc  31206  0ellimcdiv  31207  cncfperiod  31233  cncficcgt0  31243  cncfshiftioo  31247  cncfiooicc  31249  dvdivbd  31269  dvbdfbdioolem1  31274  dvbdfbdioolem2  31275  dvbdfbdioo  31276  ioodvbdlimc1lem1  31277  ioodvbdlimc1lem2  31278  ioodvbdlimc2lem  31280  volioc  31306  stoweidlem7  31323  stoweidlem11  31327  stoweidlem13  31329  stoweidlem17  31333  stoweidlem19  31335  stoweidlem20  31336  stoweidlem21  31337  stoweidlem22  31338  stoweidlem23  31339  stoweidlem24  31340  stoweidlem26  31342  stoweidlem32  31348  stoweidlem36  31352  stoweidlem44  31360  stoweidlem47  31363  wallispilem3  31383  wallispi2lem1  31387  stirlinglem1  31390  stirlinglem5  31394  stirlinglem11  31400  stirlinglem12  31401  stirlinglem14  31403  dirkerval2  31410  dirkerre  31411  dirkertrigeqlem2  31415  dirkertrigeq  31417  dirkeritg  31418  dirkercncflem1  31419  dirkercncflem2  31420  dirkercncflem4  31422  fourierdlem4  31427  fourierdlem6  31429  fourierdlem7  31430  fourierdlem11  31434  fourierdlem13  31436  fourierdlem14  31437  fourierdlem15  31438  fourierdlem16  31439  fourierdlem18  31441  fourierdlem21  31444  fourierdlem22  31445  fourierdlem24  31447  fourierdlem26  31449  fourierdlem28  31451  fourierdlem30  31453  fourierdlem35  31458  fourierdlem39  31462  fourierdlem41  31464  fourierdlem42  31465  fourierdlem43  31466  fourierdlem44  31467  fourierdlem45  31468  fourierdlem47  31470  fourierdlem48  31471  fourierdlem50  31473  fourierdlem51  31474  fourierdlem53  31476  fourierdlem57  31480  fourierdlem58  31481  fourierdlem59  31482  fourierdlem60  31483  fourierdlem61  31484  fourierdlem63  31486  fourierdlem64  31487  fourierdlem65  31488  fourierdlem66  31489  fourierdlem68  31491  fourierdlem70  31493  fourierdlem71  31494  fourierdlem72  31495  fourierdlem73  31496  fourierdlem74  31497  fourierdlem75  31498  fourierdlem76  31499  fourierdlem77  31500  fourierdlem78  31501  fourierdlem79  31502  fourierdlem83  31506  fourierdlem84  31507  fourierdlem87  31510  fourierdlem89  31512  fourierdlem90  31513  fourierdlem91  31514  fourierdlem92  31515  fourierdlem95  31518  fourierdlem97  31520  fourierdlem101  31524  fourierdlem103  31526  fourierdlem104  31527  fourierdlem107  31530  fourierdlem109  31532  fourierdlem112  31535  fouriercnp  31543  sqwvfoura  31545  sqwvfourb  31546  fouriersw  31548  sigaras  31555  sigarms  31556  sigarls  31557  sigarexp  31559  sigarperm  31560  sigarimcd  31562  sigarcol  31564  sharhght  31565  cevathlem2  31568  isosctrlem1ALT  32823  sineq0ALT  32826