Theorem recnd 9669

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

Syntax hints:   -> wi 4   e. wcel 1887   CCcc 9537   RRcr 9538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-resscn 9596

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418

This theorem is referenced by:  00id  9808  mul02lem1  9809  addid1  9813  cnegex  9814  ltadd1  10081  leadd2  10083  ltsubadd  10084  ltsubadd2  10085  lesubadd  10086  lesubadd2  10087  lesub1  10108  lesub2  10109  ltnegcon1  10115  ltnegcon2  10116  add20  10126  subge0  10127  suble0  10128  lesub0  10131  mulge0  10132  eqord2  10145  lesub3d  10231  sublt0d  10238  rereccl  10325  redivcl  10326  recgt0  10449  prodgt0  10450  prodge0  10452  ltmul1a  10454  ltdiv1  10469  ltmuldiv  10478  ltrec  10488  recp1lt1  10504  recreclt  10505  ledivp1  10508  supadd  10575  infrenegsup  10591  infmsupOLD  10592  infmrclOLD  10593  rimul  10600  cru  10601  avglt1  10850  avglt2  10851  nn0cnd  10927  zcn  10942  zeo  11021  zcnd  11041  eluzelcn  11170  cnref1o  11297  rpcn  11310  rpcnd  11343  ltaddrp2d  11372  mul2lt0rlt0  11398  mul2lt0rgt0  11399  mul2lt0llt0  11400  mul2lt0lgt0  11401  mul2lt0bi  11402  qbtwnre  11492  xralrple  11498  xpncan  11537  xmulcom  11552  xmulneg1  11555  xlemul1  11576  icoshftf1o  11755  lincmb01cmp  11775  iccf1o  11776  fladdz  12058  flzadd  12059  flhalf  12062  ceim1l  12074  intfracq  12086  fldiv  12087  modvalr  12099  flpmodeq  12101  mod0  12103  modlt  12107  moddiffl  12108  modfrac  12110  flmod  12111  intfrac  12112  modmulnn  12114  modvalp1  12115  modid  12121  modcyc  12132  modadd1  12134  modaddabs  12135  negmod  12138  modadd2mod  12140  modnegd  12145  modadd12d  12146  modsub12d  12147  modaddmulmod  12156  moddi  12157  modsubdir  12158  modeqmodmin  12159  modirr  12160  seqf1olem1  12252  serle  12268  expcl2lem  12284  expnegz  12306  expaddzlem  12315  expaddz  12316  expmulz  12318  ltexp2a  12324  leexp2a  12328  leexp2r  12330  exple1  12332  expubnd  12333  sq11  12347  bernneq2  12399  expmulnbnd  12404  discr1  12408  discr  12409  faclbnd  12475  bcp1nk  12502  cshweqrep  12920  remim  13180  reim0b  13182  rereb  13183  mulre  13184  cjreb  13186  recj  13187  reneg  13188  readd  13189  resub  13190  remullem  13191  remul2  13193  rediv  13194  imcj  13195  imneg  13196  imadd  13197  imsub  13198  immul2  13200  imdiv  13201  cjcj  13203  cjadd  13204  ipcnval  13206  cjmulval  13208  cjneg  13210  imval2  13214  cjreim2  13224  sqr0lem  13304  sqrlem5  13310  sqrlem7  13312  resqrtthlem  13318  remsqsqrt  13320  sqrtmul  13323  sqrtdiv  13329  sqrtneg  13331  sqrtmsq  13334  absdiv  13358  absid  13359  absexp  13367  absexpz  13368  absimle  13372  abslt  13377  absle  13378  abssubne0  13379  releabs  13384  recval  13385  abstri  13393  abs2difabs  13397  abs1m  13398  abslem2  13402  absrdbnd  13404  sqreulem  13422  sqreu  13423  amgm2  13432  icodiamlt  13497  lo1bddrp  13589  o1lo1  13601  rlimrecl  13644  rlimge0  13645  climrecl  13647  climge0  13648  climabs0  13649  reccn2  13660  o1rlimmul  13682  lo1mul2  13692  lo1sub  13694  climle  13703  climsqz  13704  climsqz2  13705  rlimsqz  13713  rlimsqz2  13714  climlec2  13722  isercolllem1  13728  climsup  13733  caucvgrlem  13736  caucvgrlemOLD  13737  caurcvgr  13738  caurcvgrOLD  13739  caucvgrlem2  13740  iseraltlem1  13748  iseraltlem2  13749  iseraltlem3  13750  iseralt  13751  isumrecl  13826  isumge0  13827  fsumless  13856  fsumge1  13857  fsum00  13858  fsumle  13859  fsumlt  13860  fsumabs  13861  o1fsum  13873  seqabs  13874  cvgcmp  13876  cvgcmpce  13878  abscvgcvg  13879  isumrpcl  13901  isumle  13902  isumless  13903  isumsup  13905  climcndslem1  13907  climcndslem2  13908  climcnds  13909  flo1  13912  supcvg  13914  trireciplem  13920  trirecip  13921  explecnv  13923  geo2sum  13929  geo2lim  13931  geomulcvg  13932  cvgrat  13939  mertenslem1  13940  mertenslem2  13941  fprodabs  14028  fprodle  14050  iprodrecl  14055  bpolydiflem  14107  bpoly4  14112  efcllem  14132  ege2le3  14144  efaddlem  14147  efgt0  14157  eftlub  14163  effsumlt  14165  eflt  14171  eflegeo  14175  resin4p  14192  recos4p  14193  retanhcl  14213  tanhlt1  14214  efeul  14216  ef01bndlem  14238  sin01bnd  14239  cos01bnd  14240  sin01gt0  14244  cos01gt0  14245  sin02gt0  14246  absefi  14250  absef  14251  absefib  14252  efieq1re  14253  eirrlem  14256  rpnnen2lem5  14271  rpnnen2lem8  14274  rpnnen2lem9  14275  rpnnen2lem11  14277  rpnnen2  14278  moddvds  14312  odd2np1  14365  divalglem5OLD  14376  divalglem5  14377  bitsp1o  14406  bitsfzo  14409  bitscmp  14412  sadcaddlem  14431  nn0seqcvgd  14529  sqnprm  14646  isprm5  14651  nonsq  14708  eulerthlem2  14730  prmdiveq  14734  odzdvds  14740  odzdvdsOLD  14746  vfermltlALT  14753  pythagtriplem14  14778  pcid  14822  fldivp1  14842  pcfac  14844  pockthlem  14849  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  prmrec  14866  4sqlem5  14886  4sqlem10  14891  mul4sqlem  14897  4sqlem15OLD  14903  4sqlem16OLD  14904  4sqlem15  14909  4sqlem16  14910  mulgneg  16776  ghmmulg  16895  odmodnn0  17189  mndodconglem  17190  pgpfaclem2  17715  isabvd  18048  abv1z  18060  abvneg  18062  abvrec  18064  abvdiv  18065  abvdom  18066  rege0subm  19024  cnsubrg  19028  gzrngunitlem  19032  regsumfsum  19035  prmirredlem  19064  remulg  19175  regsumsupp  19190  bl2in  21415  blhalf  21420  blssps  21439  blss  21440  methaus  21535  nrmmetd  21589  nm2dif  21638  nminvr  21672  nmdvr  21673  nlmmul0or  21686  nrginvrcnlem  21693  nmolb2d  21723  nmoi2  21735  nmoleub  21736  nmoi2OLD  21751  nmoleubOLD  21752  nmo0  21756  nmoeq0  21757  nmoco  21758  nmotri  21760  nmoid  21763  blcvx  21816  xrsxmet  21827  recld2  21832  reconnlem2  21845  opnreen  21849  metdstri  21868  metnrmlem3  21878  metdstriOLD  21883  metnrmlem3OLD  21893  icchmeo  21969  icopnfcnv  21970  icopnfhmeo  21971  iccpnfhmeo  21973  xrhmeo  21974  icccvx  21978  cnheiborlem  21982  evth  21987  lebnumii  21997  pcoass  22055  pcorevlem  22057  pcorev2  22059  pi1xfrcnv  22088  nmoleub2lem  22128  nmoleub2lem3  22129  nmoleub3  22133  cphsqrtcl2  22164  ipcau2  22208  tchcphlem1  22209  tchcphlem2  22210  tchcph  22211  iscau3  22248  rrxnm  22350  rrxcph  22351  csbren  22353  trirn  22354  rrxmval  22359  rrxmetlem  22361  rrxmet  22362  rrxdstprj1  22363  minveclem2  22368  minveclem3b  22370  minveclem4  22374  minveclem6  22376  minveclem7  22377  minveclem2OLD  22380  minveclem3bOLD  22382  minveclem4OLD  22386  minveclem6OLD  22388  minveclem7OLD  22389  pjthlem1  22391  ivthlem2  22403  ivthlem3  22404  ivth2  22406  ovolfsval  22423  ovollb2lem  22441  ovolctb  22443  ovolunlem1a  22449  ovolunnul  22453  ovolfiniun  22454  ovoliunlem1  22455  ovoliun2  22459  shft2rab  22461  ovolshftlem1  22462  sca2rab  22465  ovolscalem1  22466  ovolsca  22468  ovolicc1  22469  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolicopnf  22478  cmmbl  22488  nulmbl  22489  nulmbl2  22490  unmbl  22491  volinun  22499  volfiniun  22500  voliunlem1  22503  voliunlem3  22505  ioombl1lem3  22513  ioombl1lem4  22514  ovolioo  22521  ioorcl2  22524  uniioovol  22536  uniioombllem3  22543  uniioombllem4  22544  uniioombllem5  22545  uniioombllem6  22546  dyadovol  22551  dyaddisjlem  22553  opnmbllem  22559  vitalilem1  22566  vitalilem2  22567  vitalilem3  22568  vitalilem4  22569  ismbf  22586  mbfmulc2lem  22603  mbfmulc2re  22604  mbfmulc2  22619  mbfinf  22621  mbfinfOLD  22622  itg1val2  22642  itg11  22649  i1fmullem  22652  i1fadd  22653  itg1addlem4  22657  itg1addlem5  22658  i1fmulclem  22660  i1fmulc  22661  itg1mulc  22662  itg1sub  22667  itg10a  22668  itg1ge0a  22669  itg1climres  22672  mbfi1fseqlem3  22675  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  mbfi1flimlem  22680  mbfmullem2  22682  itg2const  22698  itg2const2  22699  itg2mulclem  22704  itg2mulc  22705  itg2splitlem  22706  itg2split  22707  itg2monolem1  22708  itg2monolem3  22710  itg2addlem  22716  itgcl  22741  itgcnlem  22747  itgrevallem1  22752  itgposval  22753  iblneg  22760  itgneg  22761  i1fibl  22765  itgitg1  22766  itgconst  22776  ibladd  22778  itgaddlem2  22781  iblabslem  22785  iblabs  22786  iblabsr  22787  iblmulc2  22788  itgmulc2lem2  22790  itgmulc2  22791  itgabs  22792  itgsplit  22793  bddmulibl  22796  dvcjbr  22903  dvfre  22905  dvexp3  22930  dveflem  22931  dvferm1lem  22936  dvferm2lem  22938  rolle  22942  cmvth  22943  mvth  22944  dvlip  22945  dvlipcn  22946  c1liplem1  22948  c1lip1  22949  dveq0  22952  dv11cn  22953  dvlt0  22957  dvle  22959  dvivthlem1  22960  dvivth  22962  lhop1lem  22965  lhop1  22966  lhop2  22967  lhop  22968  dvcvx  22972  dvfsumle  22973  dvfsumge  22974  dvfsumabs  22975  dvfsumlem1  22978  dvfsumlem2  22979  dvfsumlem4  22981  dvfsumrlimge0  22982  dvfsumrlim2  22984  dvfsum2  22986  ftc1a  22989  ftc1lem4  22991  ftc1lem5  22992  plyeq0lem  23164  coemulhi  23208  plyrecj  23233  plydivlem3  23248  aalioulem2  23289  aalioulem3  23290  aalioulem4  23291  aalioulem5  23292  aalioulem6  23293  aaliou  23294  aaliou2  23296  aaliou2b  23297  aaliou3lem3  23300  aaliou3lem7  23305  aaliou3lem9  23306  taylthlem2  23329  ulmcn  23354  ulmdvlem1  23355  mtest  23359  mtestbdd  23360  itgulm  23363  radcnvlem1  23368  radcnvlem2  23369  radcnvlt1  23373  radcnvle  23375  dvradcnv  23376  pserulm  23377  abelthlem2  23387  abelthlem5  23390  abelthlem7  23393  abelth2  23397  reeff1olem  23401  efcvx  23404  pilem2  23407  pilem2OLD  23408  pilem3  23409  pilem3OLD  23410  sincosq2sgn  23454  sincosq3sgn  23455  sincosq4sgn  23456  coseq0negpitopi  23458  tanrpcl  23459  tangtx  23460  tanabsge  23461  sinq12gt0  23462  sinq34lt0t  23464  cosq14gt0  23465  cosq14ge0  23466  pige3  23472  coskpi  23475  sineq0  23476  cosordlem  23480  sinord  23483  tanord1  23486  tanord  23487  tanregt0  23488  efif1olem2  23492  efif1olem4  23494  eff1olem  23497  rzgrp  23503  logrnaddcl  23524  logneg  23537  lognegb  23539  reexplog  23544  relogexp  23545  logfac  23550  efiarg  23556  cosargd  23557  cosarg0d  23558  argregt0  23559  argrege0  23560  argimgt0  23561  logneg2  23564  logmul2  23565  logdiv2  23566  abslogle  23567  tanarg  23568  logdivlti  23569  divlogrlim  23580  logcnlem2  23588  logcnlem3  23589  logcnlem4  23590  logcn  23592  logf1o2  23595  advlog  23599  advlogexp  23600  efopnlem1  23601  logtayllem  23604  logtayl  23605  logccv  23608  logcxp  23614  mulcxp  23630  divcxp  23632  cxpmul  23633  cxproot  23635  cxpmul2z  23636  abscxp  23637  abscxp2  23638  cxplt  23639  cxplea  23641  cxple2  23642  cxple2a  23644  cxplt3  23645  cxpsqrtlem  23647  cxpsqrt  23648  logsqrt  23649  dvcxp2  23681  cxpcn3lem  23687  resqrtcn  23689  cxpaddlelem  23691  cxpaddle  23692  abscxpbnd  23693  root1id  23694  root1eq1  23695  root1cj  23696  cxpeq  23697  loglesqrt  23698  relogbmul  23714  nnlogbexp  23718  logbrec  23719  cosangneg2d  23736  angrtmuld  23737  ang180lem2  23739  lawcoslem1  23744  lawcos  23745  pythag  23746  isosctrlem1  23747  isosctrlem2  23748  isosctrlem3  23749  ssscongptld  23751  chordthmlem  23758  chordthmlem2  23759  chordthmlem3  23760  chordthmlem4  23761  chordthmlem5  23762  heron  23764  asinsinlem  23817  reasinsin  23822  acosrecl  23829  atancj  23836  atanrecl  23837  atanlogaddlem  23839  atanlogsublem  23841  atanbndlem  23851  atans2  23857  ressatans  23860  atantayl  23863  leibpilem2  23867  leibpi  23868  leibpisum  23869  log2tlbnd  23871  log2ublem2  23873  birthdaylem2  23878  birthdaylem3  23879  cxp2limlem  23901  cxp2lim  23902  cxploglim  23903  cxploglim2  23904  divsqrtsumo1  23909  cvxcl  23910  scvxcvx  23911  jensenlem2  23913  jensen  23914  amgmlem  23915  logdiflbnd  23920  emcllem2  23922  emcllem3  23923  emcllem5  23925  emcllem6  23926  emcllem7  23927  harmonicbnd4  23936  fsumharmonic  23937  zetacvg  23940  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamgulmlem4  23957  lgamgulmlem5  23958  lgamgulmlem6  23959  lgamgulm2  23961  lgambdd  23962  lgamcvg2  23980  gamcvg  23981  gamcvg2lem  23984  regamcl  23986  relgamcl  23987  lgam1  23989  ftalem1  23997  ftalem2  23998  ftalem4  24000  ftalem5  24001  ftalem4OLD  24002  ftalem5OLD  24003  basellem3  24009  basellem4  24010  basellem5  24011  basellem6  24012  basellem7  24013  basellem8  24014  basellem9  24015  efnnfsumcl  24029  chtprm  24080  chpp1  24082  chtdif  24085  efchtdvds  24086  prmorcht  24105  mumullem2  24107  fsumfldivdiaglem  24118  ppiub  24132  chtleppi  24138  chtublem  24139  chtub  24140  pclogsum  24143  vmasum  24144  logfac2  24145  chpval2  24146  chpchtsum  24147  chpub  24148  logfaclbnd  24150  logfacbnd3  24151  logfacrlim  24152  logexprlim  24153  logfacrlim2  24154  mersenne  24155  dchrabs  24188  dchrptlem1  24192  dchrptlem2  24193  bcmax  24206  bcp1ctr  24207  bposlem1  24212  bposlem9  24220  lgsvalmod  24243  lgsdilem  24250  lgsne0  24261  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem2  24278  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  mul2sq  24293  2sqlem3  24294  2sqlem8  24300  chebbnd1lem1  24307  chebbnd1lem2  24308  chebbnd1lem3  24309  chtppilimlem1  24311  chtppilimlem2  24312  chtppilim  24313  chto1ub  24314  chto1lb  24316  chpchtlim  24317  chpo1ub  24318  vmadivsum  24320  vmadivsumb  24321  rplogsumlem1  24322  rplogsumlem2  24323  rpvmasumlem  24325  dchrisumlema  24326  dchrisumlem1  24327  dchrisumlem2  24328  dchrisumlem3  24329  dchrmusumlema  24331  dchrmusum2  24332  dchrvmasumlem1  24333  dchrvmasum2lem  24334  dchrvmasum2if  24335  dchrvmasumlem2  24336  dchrvmasumlem3  24337  dchrvmasumiflem1  24339  dchrvmasumiflem2  24340  dchrisum0flblem1  24346  dchrisum0fno1  24349  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lema  24352  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2a  24355  dchrisum0lem2  24356  dchrisum0lem3  24357  dchrmusumlem  24360  dchrvmasumlem  24361  rpvmasum  24364  rplogsum  24365  dirith2  24366  mudivsum  24368  mulogsumlem  24369  mulogsum  24370  logdivsum  24371  mulog2sumlem1  24372  mulog2sumlem2  24373  mulog2sumlem3  24374  vmalogdivsum2  24376  vmalogdivsum  24377  2vmadivsumlem  24378  logsqvma  24380  logsqvma2  24381  log2sumbnd  24382  selberglem1  24383  selberglem2  24384  selberglem3  24385  selberg  24386  selbergb  24387  selberg2lem  24388  selberg2  24389  selberg2b  24390  chpdifbndlem1  24391  logdivbnd  24394  selberg3lem1  24395  selberg3lem2  24396  selberg3  24397  selberg4lem1  24398  selberg4  24399  pntrmax  24402  pntrsumo1  24403  pntrsumbnd  24404  pntrsumbnd2  24405  selbergr  24406  selberg3r  24407  selberg4r  24408  selberg34r  24409  pntsval2  24414  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntrlog2bndlem6a  24420  pntrlog2bndlem6  24421  pntrlog2bnd  24422  pntpbnd1a  24423  pntpbnd1  24424  pntpbnd2  24425  pntibndlem2  24429  pntibndlem3  24430  pntlemb  24435  pntlemg  24436  pntlemh  24437  pntlemn  24438  pntlemr  24440  pntlemj  24441  pntlemf  24443  pntlemk  24444  pntlemo  24445  pntlem3  24447  pntleml  24449  pnt2  24451  pnt  24452  abvcxp  24453  ostth2lem1  24456  qabvexp  24464  padicabv  24468  padicabvcxp  24470  ostth2lem2  24472  ostth2lem3  24473  ostth2lem4  24474  ostth2  24475  ostth3  24476  ttgcontlem1  24915  fveecn  24932  eqeelen  24934  brbtwn2  24935  colinearalglem4  24939  colinearalg  24940  axsegconlem9  24955  axsegconlem10  24956  ax5seglem1  24958  ax5seglem2  24959  ax5seglem3  24961  ax5seglem5  24963  ax5seglem6  24964  ax5seglem9  24967  ax5seg  24968  axbtwnid  24969  axpaschlem  24970  axpasch  24971  axeuclidlem  24992  axcontlem2  24995  axcontlem4  24997  axcontlem7  25000  axcontlem8  25001  eupap1  25704  nvm1  26293  nvpi  26295  nvz0  26297  nvmtri  26300  nvabs  26302  nvge0  26303  nv1  26305  smcnlem  26333  ipval2lem4  26342  ipval2  26343  4ipval2  26344  4ipval3  26348  ipidsq  26349  dipcj  26353  dip0r  26356  ipz  26358  nmoub3i  26414  nmlno0lem  26434  nmblolbii  26440  blocnilem  26445  cncph  26460  ipasslem4  26475  ipasslem5  26476  ipblnfi  26497  minvecolem2  26517  minvecolem4  26522  minvecolem6  26524  minvecolem7  26525  minvecolem2OLD  26527  minvecolem4OLD  26532  minvecolem6OLD  26534  minvecolem7OLD  26535  htthlem  26570  normpyc  26799  hhph  26831  bcs2  26835  norm1  26902  norm1exi  26903  pjhthlem1  27044  eigvalcl  27614  eighmorth  27617  nmlnop0iALT  27648  nmbdoplbi  27677  nmcexi  27679  nmcoplbi  27681  nmbdfnlbi  27702  nmcfnlbi  27705  riesz4i  27716  cnlnadjlem2  27721  cnlnadjlem7  27726  nmopcoi  27748  nmopcoadji  27754  branmfn  27758  leopnmid  27791  opsqrlem1  27793  hst1h  27880  hstle  27883  hstoh  27885  sto2i  27890  stadd3i  27901  strlem1  27903  golem1  27924  stcltrlem1  27929  cdj1i  28086  cdj3lem1  28087  cdj3lem3b  28093  cdj3i  28094  lt2addrd  28326  le2halvesd  28335  fzsplit3  28370  bcm1n  28371  bhmafibid1  28405  bhmafibid2  28406  2sqmod  28409  psgnfzto1stlem  28613  elunitcn  28704  sqsscirc1  28714  sqsscirc2  28715  cnre2csqima  28717  rmulccn  28734  xrge0iifcnv  28739  xrge0iifhom  28743  zrhnm  28773  rezh  28775  nexple  28831  indsum  28844  esumpcvgval  28899  esumcvgsum  28909  dya2ub  29092  dya2icoseg  29099  omssubadd  29128  omssubaddOLD  29132  eulerpartlemgc  29195  ballotlemsi  29347  ballotlemsiOLD  29385  sgnmul  29413  sgnsub  29415  eluzmn  29423  plymulx0  29436  signsply0  29440  signsvtp  29472  signsvtn  29473  signsvfpn  29474  signsvfnn  29475  subfacval2  29910  subfaclim  29911  subfacval3  29912  rescon  29969  sinccvglem  30316  circum  30318  possumd  30366  climlec3  30369  faclimlem1  30379  faclimlem2  30380  faclimlem3  30381  faclim  30382  iprodfac  30383  faclim2  30384  ltflcei  31933  sin2h  31935  cos2h  31936  tan2h  31937  poimirlem29  31969  opnmbllem0  31976  mblfinlem2  31978  mblfinlem3  31979  mblfinlem4  31980  mbfposadd  31988  itg2addnclem  31993  itg2addnclem2  31994  itg2addnclem3  31995  itg2addnc  31996  itg2gt0cn  31997  ibladdnc  31999  itgaddnclem2  32001  iblabsnclem  32005  iblabsnc  32006  iblmulc2nc  32007  itgmulc2nclem2  32009  itgmulc2nc  32010  itgabsnc  32011  bddiblnc  32012  ftc1cnnclem  32015  ftc1cnnc  32016  ftc1anclem1  32017  ftc1anclem2  32018  ftc1anclem3  32019  ftc1anclem4  32020  ftc1anclem5  32021  ftc1anclem6  32022  ftc1anclem7  32023  ftc1anclem8  32024  ftc1anc  32025  areacirclem1  32032  areacirclem5  32036  areacirc  32037  mettrifi  32086  lmclim2  32087  geomcau  32088  isbnd3  32116  ssbnd  32120  cntotbnd  32128  bfplem1  32154  bfplem2  32155  bfp  32156  rrnmet  32161  rrndstprj1  32162  rrndstprj2  32163  rrncmslem  32164  rrnequiv  32167  rrntotbnd  32168  ismrer1  32170  eldioph2lem1  35602  lzenom  35612  rencldnfilem  35663  irrapxlem1  35666  irrapxlem2  35667  irrapxlem3  35668  irrapxlem4  35669  irrapxlem5  35670  pellexlem2  35674  pellexlem6  35678  pell1234qrreccl  35700  pell14qrgt0  35705  pell14qrdivcl  35711  pell14qrexpclnn0  35712  pell14qrexpcl  35713  pell14qrdich  35715  pell1qrgaplem  35719  pellfundex  35734  reglogmul  35741  reglogexp  35742  reglogbas  35743  reglog1  35744  pellfund14  35746  rmspecsqrtnq  35754  rmspecfund  35757  monotoddzzfi  35790  expmordi  35795  jm2.24nn  35809  jm2.17a  35810  jm2.17b  35811  jm2.17c  35812  jm2.24  35813  acongrep  35830  fzmaxdif  35831  acongeq  35833  modabsdifz  35839  jm2.19lem4  35847  jm2.19  35848  jm2.26lem3  35856  jm3.1lem1  35872  jm3.1lem2  35873  itgpowd  36099  areaquad  36101  absmulrposd  36597  extoimad  36607  imo72b2lem0  36608  imo72b2lem1  36614  imo72b2  36619  int-addcomd  36620  int-addassocd  36621  int-addsimpd  36622  int-mulcomd  36623  int-mulassocd  36624  int-mulsimpd  36625  int-leftdistd  36626  int-rightdistd  36627  int-sqdefd  36628  int-mul11d  36629  int-mul12d  36630  int-add01d  36631  int-add02d  36632  int-sqgeq0d  36633  int-eqmvtd  36636  cvgdvgrat  36662  radcnvrat  36663  hashnzfzclim  36671  dvconstbi  36683  binomcxplemnn0  36698  binomcxplemnotnn0  36705  isosctrlem1ALT  37331  sineq0ALT  37334  oddfl  37487  dstregt0  37491  zltlesub  37495  lt2addmuld  37499  lt3addmuld  37519  fperiodmullem  37521  fperiodmul  37522  lt4addmuld  37524  fzdifsuc2  37530  supxrgere  37556  supxrgelem  37560  suplesup  37562  supsubc  37576  xralrple2  37577  abslt2sqd  37583  iooabslt  37596  iccshift  37619  iooshift  37623  fmul01  37658  fmul01lt1lem1  37662  fmul01lt1lem2  37663  fprodabs2  37675  climinf  37684  climinfOLD  37685  limcrecl  37709  lptre2pt  37720  limcleqr  37725  0ellimcdiv  37730  limclner  37732  sinaover2ne0  37743  cncfperiod  37756  ioccncflimc  37763  cncficcgt0  37766  icocncflimc  37767  cncfshiftioo  37770  cncfiooicc  37772  fperdvper  37790  dvbdfbdioolem1  37800  dvbdfbdioolem2  37801  dvbdfbdioo  37802  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc1  37807  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  ioodvbdlimc2  37810  dvnmul  37818  dvnprodlem1  37821  dvnprodlem2  37822  itgcoscmulx  37846  volioc  37849  itgsincmulx  37851  itgiccshift  37857  itgperiod  37858  itgsbtaddcnst  37859  stoweidlem7  37867  stoweidlem11  37871  stoweidlem13  37873  stoweidlem17  37877  stoweidlem19  37879  stoweidlem20  37880  stoweidlem21  37881  stoweidlem22  37882  stoweidlem23  37883  stoweidlem24  37884  stoweidlem26  37886  stoweidlem32  37893  stoweidlem36  37897  stoweidlem44  37905  stoweidlem47  37908  wallispilem3  37929  wallispi2lem1  37933  stirlinglem1  37936  stirlinglem5  37940  stirlinglem11  37946  stirlinglem12  37947  stirlinglem14  37949  dirkerval2  37956  dirkerre  37957  dirkertrigeqlem2  37961  dirkertrigeq  37963  dirkeritg  37964  dirkercncflem1  37965  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem4  37973  fourierdlem6  37975  fourierdlem7  37976  fourierdlem13  37982  fourierdlem14  37983  fourierdlem16  37985  fourierdlem18  37987  fourierdlem19  37988  fourierdlem21  37990  fourierdlem22  37991  fourierdlem24  37993  fourierdlem26  37995  fourierdlem28  37997  fourierdlem30  37999  fourierdlem35  38005  fourierdlem39  38009  fourierdlem40  38010  fourierdlem41  38011  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem43  38014  fourierdlem44  38015  fourierdlem47  38017  fourierdlem48  38018  fourierdlem49  38019  fourierdlem50  38020  fourierdlem51  38021  fourierdlem53  38023  fourierdlem56  38026  fourierdlem57  38027  fourierdlem58  38028  fourierdlem59  38029  fourierdlem60  38030  fourierdlem61  38031  fourierdlem62  38032  fourierdlem63  38033  fourierdlem64  38034  fourierdlem65  38035  fourierdlem66  38036  fourierdlem68  38038  fourierdlem70  38040  fourierdlem71  38041  fourierdlem72  38042  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem77  38047  fourierdlem78  38048  fourierdlem79  38049  fourierdlem80  38050  fourierdlem81  38051  fourierdlem83  38053  fourierdlem84  38054  fourierdlem85  38055  fourierdlem87  38057  fourierdlem88  38058  fourierdlem89  38059  fourierdlem90  38060  fourierdlem91  38061  fourierdlem92  38062  fourierdlem93  38063  fourierdlem95  38065  fourierdlem97  38067  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fourierdlem107  38077  fourierdlem109  38079  fourierdlem111  38081  fourierdlem112  38082  fouriercnp  38090  sqwvfoura  38092  sqwvfourb  38093  fouriersw  38095  etransclem14  38113  etransclem18  38117  etransclem23  38122  etransclem24  38123  etransclem27  38126  etransclem46  38145  etransclem48OLD  38147  etransclem48  38148  qndenserrnbllem  38163  sge0tsms  38222  sge0cl  38223  sge0split  38251  sge0iunmptlemfi  38255  sge0rpcpnf  38263  sge0isum  38269  sge0ad2en  38273  sge0xaddlem1  38275  sge0xaddlem2  38276  sge0gtfsumgt  38285  carageniuncllem1  38342  carageniuncllem2  38343  volico  38363  hoicvrrex  38378  ovnsubaddlem1  38392  hsphoidmvle2  38407  hsphoidmvle  38408  hoidmvval0  38409  hoiprodp1  38410  hoidmv1lelem1  38413  hoidmv1lelem2  38414  hoidmv1le  38416  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem3  38419  hoiqssbllem2  38445  hspmbllem1  38448  sigaras  38464  sigarms  38465  sigarls  38466  sigarexp  38468  sigarperm  38469  sigarimcd  38471  sigarcol  38473  sharhght  38474  cevathlem2  38477  m1mod0mod1  38723  bgoldbtbndlem2  38901  ltsubaddb  40364  ltsubsubb  40365  ltsubadd2b  40366  flsubz  40373  fldivmod  40374  m1modmmod  40377  logblt1b  40428  dignn0fr  40465  dignn0flhalflem1  40479  dignn0flhalflem2  40480  nn0sumshdiglemA  40483