Theorem recnd 9687

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

Syntax hints:   -> wi 4   e. wcel 1904   CCcc 9555   RRcr 9556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-resscn 9614

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  00id  9826  mul02lem1  9827  addid1  9831  cnegex  9832  ltadd1  10102  leadd2  10104  ltsubadd  10105  ltsubadd2  10106  lesubadd  10107  lesubadd2  10108  lesub1  10129  lesub2  10130  ltnegcon1  10136  ltnegcon2  10137  add20  10147  subge0  10148  suble0  10149  lesub0  10152  mulge0  10153  eqord2  10166  lesub3d  10252  possumd  10259  sublt0d  10260  rereccl  10347  redivcl  10348  recgt0  10471  prodgt0  10472  prodge0  10474  ltmul1a  10476  ltdiv1  10491  ltmuldiv  10500  ltrec  10510  recp1lt1  10526  recreclt  10527  ledivp1  10530  supadd  10597  infrenegsup  10613  infmsupOLD  10614  infmrclOLD  10615  rimul  10622  cru  10623  avglt1  10873  avglt2  10874  lt2addmuld  10885  nn0cnd  10951  zcn  10966  zeo  11044  zcnd  11064  eluzmn  11189  eluzelcn  11194  cnref1o  11320  rpcn  11333  rpcnd  11366  ltaddrp2d  11395  mul2lt0rlt0  11421  mul2lt0rgt0  11422  mul2lt0llt0  11423  mul2lt0lgt0  11424  mul2lt0bi  11425  qbtwnre  11515  xralrple  11521  xpncan  11562  xmulcom  11577  xmulneg1  11580  xlemul1  11601  icoshftf1o  11781  lincmb01cmp  11801  iccf1o  11802  fladdz  12091  flzadd  12092  flhalf  12095  ceim1l  12107  intfracq  12119  fldiv  12120  modvalr  12132  flpmodeq  12134  mod0  12136  modlt  12140  moddiffl  12141  modfrac  12143  flmod  12144  intfrac  12145  modmulnn  12147  modvalp1  12148  modid  12154  modcyc  12165  modadd1  12167  modaddabs  12168  negmod  12171  modadd2mod  12174  modnegd  12179  modadd12d  12180  modsub12d  12181  modaddmulmod  12190  moddi  12191  modsubdir  12192  modeqmodmin  12193  modirr  12194  addmodlteq  12198  seqf1olem1  12290  serle  12306  expcl2lem  12322  expnegz  12344  expaddzlem  12353  expaddz  12354  expmulz  12356  ltexp2a  12362  leexp2a  12366  leexp2r  12368  exple1  12370  expubnd  12371  sq11  12385  bernneq2  12437  expmulnbnd  12442  discr1  12446  discr  12447  faclbnd  12513  bcp1nk  12540  cshweqrep  12977  remim  13257  reim0b  13259  rereb  13260  mulre  13261  cjreb  13263  recj  13264  reneg  13265  readd  13266  resub  13267  remullem  13268  remul2  13270  rediv  13271  imcj  13272  imneg  13273  imadd  13274  imsub  13275  immul2  13277  imdiv  13278  cjcj  13280  cjadd  13281  ipcnval  13283  cjmulval  13285  cjneg  13287  imval2  13291  cjreim2  13301  sqr0lem  13381  sqrlem5  13387  sqrlem7  13389  resqrtthlem  13395  remsqsqrt  13397  sqrtmul  13400  sqrtdiv  13406  sqrtneg  13408  sqrtmsq  13411  absdiv  13435  absid  13436  absexp  13444  absexpz  13445  absimle  13449  abslt  13454  absle  13455  abssubne0  13456  releabs  13461  recval  13462  abstri  13470  abs2difabs  13474  abs1m  13475  abslem2  13479  absrdbnd  13481  sqreulem  13499  sqreu  13500  amgm2  13509  icodiamlt  13574  lo1bddrp  13666  o1lo1  13678  rlimrecl  13721  rlimge0  13722  climrecl  13724  climge0  13725  climabs0  13726  reccn2  13737  o1rlimmul  13759  lo1mul2  13769  lo1sub  13771  climle  13780  climsqz  13781  climsqz2  13782  rlimsqz  13790  rlimsqz2  13791  climlec2  13799  isercolllem1  13805  climsup  13810  caucvgrlem  13813  caucvgrlemOLD  13814  caurcvgr  13815  caurcvgrOLD  13816  caucvgrlem2  13817  iseraltlem1  13825  iseraltlem2  13826  iseraltlem3  13827  iseralt  13828  isumrecl  13903  isumge0  13904  fsumless  13933  fsumge1  13934  fsum00  13935  fsumle  13936  fsumlt  13937  fsumabs  13938  o1fsum  13950  seqabs  13951  cvgcmp  13953  cvgcmpce  13955  abscvgcvg  13956  isumrpcl  13978  isumle  13979  isumless  13980  isumsup  13982  climcndslem1  13984  climcndslem2  13985  climcnds  13986  flo1  13989  supcvg  13991  trireciplem  13997  trirecip  13998  explecnv  14000  geo2sum  14006  geo2lim  14008  geomulcvg  14009  cvgrat  14016  mertenslem1  14017  mertenslem2  14018  fprodabs  14105  fprodle  14127  iprodrecl  14132  bpolydiflem  14184  bpoly4  14189  efcllem  14209  ege2le3  14221  efaddlem  14224  efgt0  14234  eftlub  14240  effsumlt  14242  eflt  14248  eflegeo  14252  resin4p  14269  recos4p  14270  retanhcl  14290  tanhlt1  14291  efeul  14293  ef01bndlem  14315  sin01bnd  14316  cos01bnd  14317  sin01gt0  14321  cos01gt0  14322  sin02gt0  14323  absefi  14327  absef  14328  absefib  14329  efieq1re  14330  eirrlem  14333  rpnnen2lem5  14348  rpnnen2lem8  14351  rpnnen2lem9  14352  rpnnen2lem11  14354  rpnnen2  14355  moddvds  14389  odd2np1  14443  divalglem5OLD  14455  divalglem5  14456  bitsp1o  14485  bitsfzo  14488  bitscmp  14491  sadcaddlem  14510  nn0seqcvgd  14608  sqnprm  14725  isprm5  14730  nonsq  14787  eulerthlem2  14809  prmdiveq  14813  odzdvds  14819  odzdvdsOLD  14825  vfermltlALT  14832  pythagtriplem14  14857  pcid  14901  fldivp1  14921  pcfac  14923  pockthlem  14928  prmreclem3  14941  prmreclem4  14942  prmreclem5  14943  prmrec  14945  4sqlem5  14965  4sqlem10  14970  mul4sqlem  14976  4sqlem15OLD  14982  4sqlem16OLD  14983  4sqlem15  14988  4sqlem16  14989  mulgneg  16854  ghmmulg  16973  odmodnn0  17267  mndodconglem  17268  pgpfaclem2  17793  isabvd  18126  abv1z  18138  abvneg  18140  abvrec  18142  abvdiv  18143  abvdom  18144  rege0subm  19101  cnsubrg  19105  gzrngunitlem  19109  regsumfsum  19112  prmirredlem  19141  remulg  19252  regsumsupp  19267  bl2in  21493  blhalf  21498  blssps  21517  blss  21518  methaus  21613  nrmmetd  21667  nm2dif  21716  nminvr  21750  nmdvr  21751  nlmmul0or  21764  nrginvrcnlem  21771  nmolb2d  21801  nmoi2  21813  nmoleub  21814  nmoi2OLD  21829  nmoleubOLD  21830  nmo0  21834  nmoeq0  21835  nmoco  21836  nmotri  21838  nmoid  21841  blcvx  21894  xrsxmet  21905  recld2  21910  reconnlem2  21923  opnreen  21927  metdstri  21946  metnrmlem3  21956  metdstriOLD  21961  metnrmlem3OLD  21971  icchmeo  22047  icopnfcnv  22048  icopnfhmeo  22049  iccpnfhmeo  22051  xrhmeo  22052  icccvx  22056  cnheiborlem  22060  evth  22065  lebnumii  22075  pcoass  22133  pcorevlem  22135  pcorev2  22137  pi1xfrcnv  22166  nmoleub2lem  22206  nmoleub2lem3  22207  nmoleub3  22211  cphsqrtcl2  22242  ipcau2  22286  tchcphlem1  22287  tchcphlem2  22288  tchcph  22289  iscau3  22326  rrxnm  22428  rrxcph  22429  csbren  22431  trirn  22432  rrxmval  22437  rrxmetlem  22439  rrxmet  22440  rrxdstprj1  22441  minveclem2  22446  minveclem3b  22448  minveclem4  22452  minveclem6  22454  minveclem7  22455  minveclem2OLD  22458  minveclem3bOLD  22460  minveclem4OLD  22464  minveclem6OLD  22466  minveclem7OLD  22467  pjthlem1  22469  ivthlem2  22481  ivthlem3  22482  ivth2  22484  ovolfsval  22501  ovollb2lem  22519  ovolctb  22521  ovolunlem1a  22527  ovolunnul  22531  ovolfiniun  22532  ovoliunlem1  22533  ovoliun2  22537  shft2rab  22539  ovolshftlem1  22540  sca2rab  22543  ovolscalem1  22544  ovolsca  22546  ovolicc1  22547  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicopnf  22556  cmmbl  22566  nulmbl  22567  nulmbl2  22568  unmbl  22569  volinun  22578  volfiniun  22579  voliunlem1  22582  voliunlem3  22584  ioombl1lem3  22592  ioombl1lem4  22593  ovolioo  22600  ioorcl2  22603  uniioovol  22615  uniioombllem3  22622  uniioombllem4  22623  uniioombllem5  22624  uniioombllem6  22625  dyadovol  22630  dyaddisjlem  22632  opnmbllem  22638  vitalilem1  22645  vitalilem2  22646  vitalilem3  22647  vitalilem4  22648  ismbf  22665  mbfmulc2lem  22682  mbfmulc2re  22683  mbfmulc2  22698  mbfinf  22700  mbfinfOLD  22701  itg1val2  22721  itg11  22728  i1fmullem  22731  i1fadd  22732  itg1addlem4  22736  itg1addlem5  22737  i1fmulclem  22739  i1fmulc  22740  itg1mulc  22741  itg1sub  22746  itg10a  22747  itg1ge0a  22748  itg1climres  22751  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1fseqlem6  22757  mbfi1flimlem  22759  mbfmullem2  22761  itg2const  22777  itg2const2  22778  itg2mulclem  22783  itg2mulc  22784  itg2splitlem  22785  itg2split  22786  itg2monolem1  22787  itg2monolem3  22789  itg2addlem  22795  itgcl  22820  itgcnlem  22826  itgrevallem1  22831  itgposval  22832  iblneg  22839  itgneg  22840  i1fibl  22844  itgitg1  22845  itgconst  22855  ibladd  22857  itgaddlem2  22860  iblabslem  22864  iblabs  22865  iblabsr  22866  iblmulc2  22867  itgmulc2lem2  22869  itgmulc2  22870  itgabs  22871  itgsplit  22872  bddmulibl  22875  dvcjbr  22982  dvfre  22984  dvexp3  23009  dveflem  23010  dvferm1lem  23015  dvferm2lem  23017  rolle  23021  cmvth  23022  mvth  23023  dvlip  23024  dvlipcn  23025  c1liplem1  23027  c1lip1  23028  dveq0  23031  dv11cn  23032  dvlt0  23036  dvle  23038  dvivthlem1  23039  dvivth  23041  lhop1lem  23044  lhop1  23045  lhop2  23046  lhop  23047  dvcvx  23051  dvfsumle  23052  dvfsumge  23053  dvfsumabs  23054  dvfsumlem1  23057  dvfsumlem2  23058  dvfsumlem4  23060  dvfsumrlimge0  23061  dvfsumrlim2  23063  dvfsum2  23065  ftc1a  23068  ftc1lem4  23070  ftc1lem5  23071  plyeq0lem  23243  coemulhi  23287  plyrecj  23312  plydivlem3  23327  aalioulem2  23368  aalioulem3  23369  aalioulem4  23370  aalioulem5  23371  aalioulem6  23372  aaliou  23373  aaliou2  23375  aaliou2b  23376  aaliou3lem3  23379  aaliou3lem7  23384  aaliou3lem9  23385  taylthlem2  23408  ulmcn  23433  ulmdvlem1  23434  mtest  23438  mtestbdd  23439  itgulm  23442  radcnvlem1  23447  radcnvlem2  23448  radcnvlt1  23452  radcnvle  23454  dvradcnv  23455  pserulm  23456  abelthlem2  23466  abelthlem5  23469  abelthlem7  23472  abelth2  23476  reeff1olem  23480  efcvx  23483  pilem2  23486  pilem2OLD  23487  pilem3  23488  pilem3OLD  23489  sincosq2sgn  23533  sincosq3sgn  23534  sincosq4sgn  23535  coseq0negpitopi  23537  tanrpcl  23538  tangtx  23539  tanabsge  23540  sinq12gt0  23541  sinq34lt0t  23543  cosq14gt0  23544  cosq14ge0  23545  pige3  23551  coskpi  23554  sineq0  23555  cosordlem  23559  sinord  23562  tanord1  23565  tanord  23566  tanregt0  23567  efif1olem2  23571  efif1olem4  23573  eff1olem  23576  rzgrp  23582  logrnaddcl  23603  logneg  23616  lognegb  23618  reexplog  23623  relogexp  23624  logfac  23629  efiarg  23635  cosargd  23636  cosarg0d  23637  argregt0  23638  argrege0  23639  argimgt0  23640  logneg2  23643  logmul2  23644  logdiv2  23645  abslogle  23646  tanarg  23647  logdivlti  23648  divlogrlim  23659  logcnlem2  23667  logcnlem3  23668  logcnlem4  23669  logcn  23671  logf1o2  23674  advlog  23678  advlogexp  23679  efopnlem1  23680  logtayllem  23683  logtayl  23684  logccv  23687  logcxp  23693  mulcxp  23709  divcxp  23711  cxpmul  23712  cxproot  23714  cxpmul2z  23715  abscxp  23716  abscxp2  23717  cxplt  23718  cxplea  23720  cxple2  23721  cxple2a  23723  cxplt3  23724  cxpsqrtlem  23726  cxpsqrt  23727  logsqrt  23728  dvcxp2  23760  cxpcn3lem  23766  resqrtcn  23768  cxpaddlelem  23770  cxpaddle  23771  abscxpbnd  23772  root1id  23773  root1eq1  23774  root1cj  23775  cxpeq  23776  loglesqrt  23777  relogbmul  23793  nnlogbexp  23797  logbrec  23798  cosangneg2d  23815  angrtmuld  23816  ang180lem2  23818  lawcoslem1  23823  lawcos  23824  pythag  23825  isosctrlem1  23826  isosctrlem2  23827  isosctrlem3  23828  ssscongptld  23830  chordthmlem  23837  chordthmlem2  23838  chordthmlem3  23839  chordthmlem4  23840  chordthmlem5  23841  heron  23843  asinsinlem  23896  reasinsin  23901  acosrecl  23908  atancj  23915  atanrecl  23916  atanlogaddlem  23918  atanlogsublem  23920  atanbndlem  23930  atans2  23936  ressatans  23939  atantayl  23942  leibpilem2  23946  leibpi  23947  leibpisum  23948  log2tlbnd  23950  log2ublem2  23952  birthdaylem2  23957  birthdaylem3  23958  cxp2limlem  23980  cxp2lim  23981  cxploglim  23982  cxploglim2  23983  divsqrtsumo1  23988  cvxcl  23989  scvxcvx  23990  jensenlem2  23992  jensen  23993  amgmlem  23994  logdiflbnd  23999  emcllem2  24001  emcllem3  24002  emcllem5  24004  emcllem6  24005  emcllem7  24006  harmonicbnd4  24015  fsumharmonic  24016  zetacvg  24019  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem4  24036  lgamgulmlem5  24037  lgamgulmlem6  24038  lgamgulm2  24040  lgambdd  24041  lgamcvg2  24059  gamcvg  24060  gamcvg2lem  24063  regamcl  24065  relgamcl  24066  lgam1  24068  ftalem1  24076  ftalem2  24077  ftalem4  24079  ftalem5  24080  ftalem4OLD  24081  ftalem5OLD  24082  basellem3  24088  basellem4  24089  basellem5  24090  basellem6  24091  basellem7  24092  basellem8  24093  basellem9  24094  efnnfsumcl  24108  chtprm  24159  chpp1  24161  chtdif  24164  efchtdvds  24165  prmorcht  24184  mumullem2  24186  fsumfldivdiaglem  24197  ppiub  24211  chtleppi  24217  chtublem  24218  chtub  24219  pclogsum  24222  vmasum  24223  logfac2  24224  chpval2  24225  chpchtsum  24226  chpub  24227  logfaclbnd  24229  logfacbnd3  24230  logfacrlim  24231  logexprlim  24232  logfacrlim2  24233  mersenne  24234  dchrabs  24267  dchrptlem1  24271  dchrptlem2  24272  bcmax  24285  bcp1ctr  24286  bposlem1  24291  bposlem9  24299  lgsvalmod  24322  lgsdilem  24329  lgsne0  24340  lgsqrlem2  24349  lgseisenlem1  24356  lgseisenlem2  24357  lgseisen  24360  lgsquadlem1  24361  lgsquadlem2  24362  mul2sq  24372  2sqlem3  24373  2sqlem8  24379  chebbnd1lem1  24386  chebbnd1lem2  24387  chebbnd1lem3  24388  chtppilimlem1  24390  chtppilimlem2  24391  chtppilim  24392  chto1ub  24393  chto1lb  24395  chpchtlim  24396  chpo1ub  24397  vmadivsum  24399  vmadivsumb  24400  rplogsumlem1  24401  rplogsumlem2  24402  rpvmasumlem  24404  dchrisumlema  24405  dchrisumlem1  24406  dchrisumlem2  24407  dchrisumlem3  24408  dchrmusumlema  24410  dchrmusum2  24411  dchrvmasumlem1  24412  dchrvmasum2lem  24413  dchrvmasum2if  24414  dchrvmasumlem2  24415  dchrvmasumlem3  24416  dchrvmasumiflem1  24418  dchrvmasumiflem2  24419  dchrisum0flblem1  24425  dchrisum0fno1  24428  rpvmasum2  24429  dchrisum0re  24430  dchrisum0lema  24431  dchrisum0lem1b  24432  dchrisum0lem1  24433  dchrisum0lem2a  24434  dchrisum0lem2  24435  dchrisum0lem3  24436  dchrmusumlem  24439  dchrvmasumlem  24440  rpvmasum  24443  rplogsum  24444  dirith2  24445  mudivsum  24447  mulogsumlem  24448  mulogsum  24449  logdivsum  24450  mulog2sumlem1  24451  mulog2sumlem2  24452  mulog2sumlem3  24453  vmalogdivsum2  24455  vmalogdivsum  24456  2vmadivsumlem  24457  logsqvma  24459  logsqvma2  24460  log2sumbnd  24461  selberglem1  24462  selberglem2  24463  selberglem3  24464  selberg  24465  selbergb  24466  selberg2lem  24467  selberg2  24468  selberg2b  24469  chpdifbndlem1  24470  logdivbnd  24473  selberg3lem1  24474  selberg3lem2  24475  selberg3  24476  selberg4lem1  24477  selberg4  24478  pntrmax  24481  pntrsumo1  24482  pntrsumbnd  24483  pntrsumbnd2  24484  selbergr  24485  selberg3r  24486  selberg4r  24487  selberg34r  24488  pntsval2  24493  pntrlog2bndlem1  24494  pntrlog2bndlem2  24495  pntrlog2bndlem3  24496  pntrlog2bndlem4  24497  pntrlog2bndlem5  24498  pntrlog2bndlem6a  24499  pntrlog2bndlem6  24500  pntrlog2bnd  24501  pntpbnd1a  24502  pntpbnd1  24503  pntpbnd2  24504  pntibndlem2  24508  pntibndlem3  24509  pntlemb  24514  pntlemg  24515  pntlemh  24516  pntlemn  24517  pntlemr  24519  pntlemj  24520  pntlemf  24522  pntlemk  24523  pntlemo  24524  pntlem3  24526  pntleml  24528  pnt2  24530  pnt  24531  abvcxp  24532  ostth2lem1  24535  qabvexp  24543  padicabv  24547  padicabvcxp  24549  ostth2lem2  24551  ostth2lem3  24552  ostth2lem4  24553  ostth2  24554  ostth3  24555  ttgcontlem1  24994  fveecn  25011  eqeelen  25013  brbtwn2  25014  colinearalglem4  25018  colinearalg  25019  axsegconlem9  25034  axsegconlem10  25035  ax5seglem1  25037  ax5seglem2  25038  ax5seglem3  25040  ax5seglem5  25042  ax5seglem6  25043  ax5seglem9  25046  ax5seg  25047  axbtwnid  25048  axpaschlem  25049  axpasch  25050  axeuclidlem  25071  axcontlem2  25074  axcontlem4  25076  axcontlem7  25079  axcontlem8  25080  eupap1  25783  nvm1  26374  nvpi  26376  nvz0  26378  nvmtri  26381  nvabs  26383  nvge0  26384  nv1  26386  smcnlem  26414  ipval2lem4  26423  ipval2  26424  4ipval2  26425  4ipval3  26429  ipidsq  26430  dipcj  26434  dip0r  26437  ipz  26439  nmoub3i  26495  nmlno0lem  26515  nmblolbii  26521  blocnilem  26526  cncph  26541  ipasslem4  26556  ipasslem5  26557  ipblnfi  26578  minvecolem2  26598  minvecolem4  26603  minvecolem6  26605  minvecolem7  26606  minvecolem2OLD  26608  minvecolem4OLD  26613  minvecolem6OLD  26615  minvecolem7OLD  26616  htthlem  26651  normpyc  26880  hhph  26912  bcs2  26916  norm1  26983  norm1exi  26984  pjhthlem1  27125  eigvalcl  27695  eighmorth  27698  nmlnop0iALT  27729  nmbdoplbi  27758  nmcexi  27760  nmcoplbi  27762  nmbdfnlbi  27783  nmcfnlbi  27786  riesz4i  27797  cnlnadjlem2  27802  cnlnadjlem7  27807  nmopcoi  27829  nmopcoadji  27835  branmfn  27839  leopnmid  27872  opsqrlem1  27874  hst1h  27961  hstle  27964  hstoh  27966  sto2i  27971  stadd3i  27982  strlem1  27984  golem1  28005  stcltrlem1  28010  cdj1i  28167  cdj3lem1  28168  cdj3lem3b  28174  cdj3i  28175  lt2addrd  28401  le2halvesd  28410  fzsplit3  28445  bcm1n  28446  bhmafibid1  28480  bhmafibid2  28481  2sqmod  28484  psgnfzto1stlem  28687  elunitcn  28778  sqsscirc1  28788  sqsscirc2  28789  cnre2csqima  28791  rmulccn  28808  xrge0iifcnv  28813  xrge0iifhom  28817  zrhnm  28847  rezh  28849  nexple  28905  indsum  28918  esumpcvgval  28973  esumcvgsum  28983  dya2ub  29165  dya2icoseg  29172  omssubadd  29201  omssubaddOLD  29205  eulerpartlemgc  29268  ballotlemsi  29420  ballotlemsiOLD  29458  sgnmul  29486  sgnsub  29488  plymulx0  29508  signsply0  29512  signsvtp  29544  signsvtn  29545  signsvfpn  29546  signsvfnn  29547  subfacval2  29982  subfaclim  29983  subfacval3  29984  rescon  30041  sinccvglem  30388  circum  30390  climlec3  30440  faclimlem1  30450  faclimlem2  30451  faclimlem3  30452  faclim  30453  iprodfac  30454  faclim2  30455  ltflcei  31997  sin2h  31999  cos2h  32000  tan2h  32001  poimirlem29  32033  opnmbllem0  32040  mblfinlem2  32042  mblfinlem3  32043  mblfinlem4  32044  mbfposadd  32052  itg2addnclem  32057  itg2addnclem2  32058  itg2addnclem3  32059  itg2addnc  32060  itg2gt0cn  32061  ibladdnc  32063  itgaddnclem2  32065  iblabsnclem  32069  iblabsnc  32070  iblmulc2nc  32071  itgmulc2nclem2  32073  itgmulc2nc  32074  itgabsnc  32075  bddiblnc  32076  ftc1cnnclem  32079  ftc1cnnc  32080  ftc1anclem1  32081  ftc1anclem2  32082  ftc1anclem3  32083  ftc1anclem4  32084  ftc1anclem5  32085  ftc1anclem6  32086  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  areacirclem1  32096  areacirclem5  32100  areacirc  32101  mettrifi  32150  lmclim2  32151  geomcau  32152  isbnd3  32180  ssbnd  32184  cntotbnd  32192  bfplem1  32218  bfplem2  32219  bfp  32220  rrnmet  32225  rrndstprj1  32226  rrndstprj2  32227  rrncmslem  32228  rrnequiv  32231  rrntotbnd  32232  ismrer1  32234  eldioph2lem1  35673  lzenom  35683  rencldnfilem  35734  irrapxlem1  35737  irrapxlem2  35738  irrapxlem3  35739  irrapxlem4  35740  irrapxlem5  35741  pellexlem2  35745  pellexlem6  35749  pell1234qrreccl  35771  pell14qrgt0  35776  pell14qrdivcl  35782  pell14qrexpclnn0  35783  pell14qrexpcl  35784  pell14qrdich  35786  pell1qrgaplem  35790  pellfundex  35805  reglogmul  35812  reglogexp  35813  reglogbas  35814  reglog1  35815  pellfund14  35817  rmspecsqrtnq  35825  rmspecfund  35828  monotoddzzfi  35861  expmordi  35866  jm2.24nn  35880  jm2.17a  35881  jm2.17b  35882  jm2.17c  35883  jm2.24  35884  acongrep  35901  fzmaxdif  35902  acongeq  35904  modabsdifz  35910  jm2.19lem4  35918  jm2.19  35919  jm2.26lem3  35927  jm3.1lem1  35943  jm3.1lem2  35944  itgpowd  36170  areaquad  36172  absmulrposd  36668  extoimad  36678  imo72b2lem0  36679  imo72b2lem1  36685  imo72b2  36689  int-addcomd  36690  int-addassocd  36691  int-addsimpd  36692  int-mulcomd  36693  int-mulassocd  36694  int-mulsimpd  36695  int-leftdistd  36696  int-rightdistd  36697  int-sqdefd  36698  int-mul11d  36699  int-mul12d  36700  int-add01d  36701  int-add02d  36702  int-sqgeq0d  36703  int-eqmvtd  36706  cvgdvgrat  36732  radcnvrat  36733  hashnzfzclim  36741  dvconstbi  36753  binomcxplemnn0  36768  binomcxplemnotnn0  36775  isosctrlem1ALT  37394  sineq0ALT  37397  oddfl  37577  dstregt0  37581  zltlesub  37585  lt3addmuld  37607  fperiodmullem  37609  fperiodmul  37610  lt4addmuld  37612  fzdifsuc2  37618  supxrgere  37643  supxrgelem  37647  suplesup  37649  supsubc  37663  xralrple2  37664  abslt2sqd  37670  iooabslt  37692  iccshift  37715  iooshift  37719  fmul01  37755  fmul01lt1lem1  37759  fmul01lt1lem2  37760  fprodabs2  37772  climinf  37781  climinfOLD  37782  limcrecl  37806  lptre2pt  37817  limcleqr  37822  0ellimcdiv  37827  limclner  37829  sinaover2ne0  37840  cncfperiod  37853  ioccncflimc  37860  cncficcgt0  37863  icocncflimc  37864  cncfshiftioo  37867  cncfiooicc  37869  fperdvper  37887  dvbdfbdioolem1  37897  dvbdfbdioolem2  37898  dvbdfbdioo  37899  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc1  37904  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  ioodvbdlimc2  37907  dvnmul  37915  dvnprodlem1  37918  dvnprodlem2  37919  itgcoscmulx  37943  volioc  37946  itgsincmulx  37948  itgiccshift  37954  itgperiod  37955  itgsbtaddcnst  37956  volico  37958  voliooico  37967  stoweidlem7  37979  stoweidlem11  37983  stoweidlem13  37985  stoweidlem17  37989  stoweidlem19  37991  stoweidlem20  37992  stoweidlem21  37993  stoweidlem22  37994  stoweidlem23  37995  stoweidlem24  37996  stoweidlem26  37998  stoweidlem32  38005  stoweidlem36  38009  stoweidlem44  38017  stoweidlem47  38020  wallispilem3  38041  wallispi2lem1  38045  stirlinglem1  38048  stirlinglem5  38052  stirlinglem11  38058  stirlinglem12  38059  stirlinglem14  38061  dirkerval2  38068  dirkerre  38069  dirkertrigeqlem2  38073  dirkertrigeq  38075  dirkeritg  38076  dirkercncflem1  38077  dirkercncflem2  38078  dirkercncflem4  38080  fourierdlem4  38085  fourierdlem6  38087  fourierdlem7  38088  fourierdlem13  38094  fourierdlem14  38095  fourierdlem16  38097  fourierdlem18  38099  fourierdlem19  38100  fourierdlem21  38102  fourierdlem22  38103  fourierdlem24  38105  fourierdlem26  38107  fourierdlem28  38109  fourierdlem30  38111  fourierdlem35  38117  fourierdlem39  38121  fourierdlem40  38122  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem43  38126  fourierdlem44  38127  fourierdlem47  38129  fourierdlem48  38130  fourierdlem49  38131  fourierdlem50  38132  fourierdlem51  38133  fourierdlem53  38135  fourierdlem56  38138  fourierdlem57  38139  fourierdlem58  38140  fourierdlem59  38141  fourierdlem60  38142  fourierdlem61  38143  fourierdlem62  38144  fourierdlem63  38145  fourierdlem64  38146  fourierdlem65  38147  fourierdlem66  38148  fourierdlem68  38150  fourierdlem70  38152  fourierdlem71  38153  fourierdlem72  38154  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem77  38159  fourierdlem78  38160  fourierdlem79  38161  fourierdlem80  38162  fourierdlem81  38163  fourierdlem83  38165  fourierdlem84  38166  fourierdlem85  38167  fourierdlem87  38169  fourierdlem88  38170  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  fourierdlem92  38174  fourierdlem93  38175  fourierdlem95  38177  fourierdlem97  38179  fourierdlem101  38183  fourierdlem103  38185  fourierdlem104  38186  fourierdlem107  38189  fourierdlem109  38191  fourierdlem111  38193  fourierdlem112  38194  fouriercnp  38202  sqwvfoura  38204  sqwvfourb  38205  fouriersw  38207  etransclem14  38225  etransclem18  38229  etransclem23  38234  etransclem24  38235  etransclem27  38238  etransclem46  38257  etransclem48OLD  38259  etransclem48  38260  qndenserrnbllem  38275  sge0tsms  38336  sge0cl  38337  sge0split  38365  sge0iunmptlemfi  38369  sge0rpcpnf  38377  sge0isum  38383  sge0ad2en  38387  sge0xaddlem1  38389  sge0xaddlem2  38390  sge0gtfsumgt  38399  sge0seq  38402  carageniuncllem1  38461  carageniuncllem2  38462  hoicvrrex  38496  ovnsubaddlem1  38510  hsphoidmvle2  38525  hsphoidmvle  38526  hoidmvval0  38527  hoiprodp1  38528  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1le  38534  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem3  38537  hoiqssbllem2  38563  hspmbllem1  38566  ovolval2lem  38583  ovolval3  38587  ovolval5lem1  38592  ovnovollem1  38596  ovnovollem2  38597  sigaras  38610  sigarms  38611  sigarls  38612  sigarexp  38614  sigarperm  38615  sigarimcd  38617  sigarcol  38619  sharhght  38620  cevathlem2  38623  m1mod0mod1  38868  bgoldbtbndlem2  39046  ltsubaddb  40819  ltsubsubb  40820  ltsubadd2b  40821  flsubz  40828  fldivmod  40829  m1modmmod  40832  logblt1b  40883  dignn0fr  40920  dignn0flhalflem1  40934  dignn0flhalflem2  40935  nn0sumshdiglemA  40938