Theorem recnd 11196

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
recnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		recn 11149	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2132  ℂcc 11057  ℝcr 11058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-resscn 11116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-clel 2827  df-ss 3912

This theorem is referenced by:  00id  11344  mul02lem1  11345  addrid  11349  cnegex  11350  ltadd1  11640  leadd2  11642  ltsubadd  11643  ltsubadd2  11644  lesubadd  11645  lesubadd2  11646  lesub1  11667  lesub2  11668  ltnegcon1  11674  ltnegcon2  11675  add20  11685  subge0  11686  suble0  11687  lesub0  11690  mulge0  11691  eqord2  11704  lesub3d  11791  possumd  11798  sublt0d  11799  rereccl  11895  redivcl  11896  recgt0  12023  prodgt0  12024  ltmul1a  12026  ltdiv1  12042  ltmuldiv  12051  ltrec  12060  recp1lt1  12076  recreclt  12077  ledivp1  12080  supadd  12146  infrenegsup  12161  rimul  12172  cru  12173  avglt1  12445  avglt2  12446  lt2addmuld  12457  div4p1lem1div2  12462  nn0cnd  12530  zcn  12559  zeo  12645  zcnd  12664  eluzmn  12832  eluzelcn  12837  cnref1o  12972  rpcn  12990  rpcnd  13025  ltaddrp2d  13057  mul2lt0rlt0  13083  mul2lt0rgt0  13084  mul2lt0llt0  13085  mul2lt0lgt0  13086  mul2lt0bi  13087  prodge0rd  13088  prodge0ld  13089  qbtwnre  13188  xralrple  13194  xpncan  13240  xmulcom  13255  xmulneg1  13258  xlemul1  13279  elunitcn  13458  icoshftf1o  13464  lincmb01cmp  13485  iccf1o  13486  divfl0  13820  fladdz  13821  flzadd  13822  flhalf  13826  ceim1l  13843  intfracq  13855  fldiv  13856  modvalr  13868  flpmodeq  13870  mod0  13872  modlt  13876  moddiffl  13878  modfrac  13880  flmod  13881  intfrac  13882  modmulnn  13885  modvalp1  13886  modid  13892  modcyc  13902  modadd1  13904  modaddb  13905  modaddabs  13907  modmuladdnn0  13914  negmod  13915  modadd2mod  13920  modnegd  13925  modadd12d  13926  modsub12d  13927  modmulmodr  13936  modaddmulmod  13937  moddi  13938  modsubdir  13939  modeqmodmin  13940  modirr  13941  addmodlteq  13945  seqf1olem1  14040  serle  14056  expcl2lem  14072  expnegz  14095  expaddzlem  14104  expaddz  14105  expmulz  14107  sq11  14130  ltexp2a  14165  expmordi  14166  leexp2a  14171  leexp2r  14173  exple1  14176  expubnd  14177  bernneq2  14229  expmulnbnd  14234  discr1  14238  discr  14239  faclbnd  14289  bcp1nk  14316  cshweqrep  14820  remim  15116  reim0b  15118  rereb  15119  mulre  15120  cjreb  15122  recj  15123  reneg  15124  readd  15125  resub  15126  remullem  15127  remul2  15129  rediv  15130  imcj  15131  imneg  15132  imadd  15133  imsub  15134  immul2  15136  imdiv  15137  cjcj  15139  cjadd  15140  ipcnval  15142  cjmulval  15144  cjneg  15146  imval2  15150  cjreim2  15160  01sqrexlem5  15245  01sqrexlem7  15247  resqrtthlem  15253  remsqsqrt  15255  sqrtmul  15258  sqrtdiv  15264  sqrtneg  15266  sqrtmsq  15269  absdiv  15294  absid  15295  absexp  15303  absexpz  15304  absimle  15308  abslt  15314  absle  15315  abssubne0  15316  releabs  15321  recval  15322  abstri  15330  abs2difabs  15334  abs1m  15335  abslem2  15339  absrdbnd  15341  sqreulem  15359  sqreu  15360  amgm2  15369  icodiamlt  15437  bhmafibid1  15467  bhmafibid2  15468  lo1bddrp  15524  o1lo1  15536  rlimrecl  15579  rlimge0  15580  climrecl  15582  climge0  15583  climabs0  15584  reccn2  15596  o1rlimmul  15618  lo1mul2  15628  lo1sub  15630  climle  15639  climsqz  15640  climsqz2  15641  rlimsqz  15649  rlimsqz2  15650  climlec2  15658  isercolllem1  15664  climsup  15669  caucvgrlem  15672  caurcvgr  15673  caucvgrlem2  15674  iseraltlem1  15681  iseraltlem2  15682  iseraltlem3  15683  iseralt  15684  isumrecl  15764  isumge0  15765  fsumless  15796  fsumge1  15797  fsum00  15798  fsumle  15799  fsumlt  15800  fsumabs  15801  o1fsum  15813  seqabs  15814  cvgcmp  15816  cvgcmpce  15818  abscvgcvg  15819  indsum  15828  indsumhash  15829  isumrpcl  15845  isumle  15846  isumless  15847  isumsup  15849  climcndslem1  15851  climcndslem2  15852  climcnds  15853  flo1  15856  supcvg  15858  trireciplem  15864  trirecip  15865  explecnv  15867  geo2sum  15875  geo2lim  15877  geomulcvg  15878  cvgrat  15885  mertenslem1  15886  mertenslem2  15887  fprodabs  15976  fprodle  15998  iprodrecl  16004  bpolydiflem  16056  bpoly4  16061  efcllem  16079  ege2le3  16092  efaddlem  16095  efgt0  16107  eftlub  16113  effsumlt  16115  eflt  16121  eflegeo  16125  resin4p  16142  recos4p  16143  retanhcl  16163  tanhlt1  16164  efeul  16166  ef01bndlem  16188  sin01bnd  16189  cos01bnd  16190  sin01gt0  16194  cos01gt0  16195  sin02gt0  16196  absefi  16200  absef  16201  absefib  16202  efieq1re  16203  eirrlem  16208  rpnnen2lem5  16222  rpnnen2lem8  16225  rpnnen2lem9  16226  rpnnen2lem11  16228  rpnnen2lem12  16229  moddvds  16269  odd2np1  16347  divalglem5  16403  bitsp1o  16439  bitsfzo  16441  bitscmp  16444  sadcaddlem  16463  nn0seqcvgd  16576  sqnprm  16709  isprm5  16714  nonsq  16766  eulerthlem2  16789  prmdiveq  16793  odzdvds  16803  vfermltlALT  16810  pythagtriplem14  16836  pcid  16881  fldivp1  16905  pcfac  16907  pockthlem  16913  prmreclem3  16926  prmreclem4  16927  prmreclem5  16928  prmrec  16930  4sqlem5  16950  4sqlem10  16955  mul4sqlem  16961  4sqlem15  16967  4sqlem16  16968  mulgneg  19106  ghmmulg  19240  odmodnn0  19552  mndodconglem  19553  pgpfaclem2  20096  isabvd  20830  abv1z  20842  abvneg  20844  abvrec  20846  abvdiv  20847  abvdom  20848  rege0subm  21444  cnsubrg  21448  gzrngunitlem  21453  regsumfsum  21456  prmirredlem  21493  remulg  21628  rzgrp  21644  bl2in  24429  blhalf  24434  blssps  24453  blss  24454  methaus  24549  nrmmetd  24603  nm2dif  24654  nminvr  24698  nmdvr  24699  nlmmul0or  24712  nrginvrcnlem  24720  nmolb2d  24747  nmoi2  24759  nmoleub  24760  nmo0  24764  nmoeq0  24765  nmoco  24766  nmotri  24768  nmoid  24771  blcvx  24827  xrsxmet  24839  recld2  24844  reconnlem2  24857  opnreen  24861  metdstri  24881  metnrmlem3  24891  icchmeo  24972  icopnfcnv  24973  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  icccvx  24981  cnheiborlem  24985  evth  24990  lebnumii  24997  pcoass  25055  pcorevlem  25057  pcorev2  25059  pi1xfrcnv  25088  nmoleub2lem  25145  nmoleub2lem3  25146  nmoleub3  25150  ncvsm1  25185  ncvspi  25187  ncvs1  25188  cphsqrtcl2  25217  ipcau2  25265  tcphcphlem1  25266  tcphcphlem2  25267  tcphcph  25268  cphipval2  25272  cphipval  25274  iscau3  25309  rrxnm  25422  rrxcph  25423  csbren  25430  trirn  25431  rrxmval  25436  rrxmetlem  25438  rrxmet  25439  rrxdstprj1  25440  ehl1eudis  25451  ehl2eudis  25453  minveclem2  25457  minveclem3b  25459  minveclem4  25463  minveclem6  25465  minveclem7  25466  pjthlem1  25468  ivthlem2  25483  ivthlem3  25484  ivth2  25486  ovolfsval  25501  ovollb2lem  25519  ovolctb  25521  ovolunlem1a  25527  ovolunnul  25531  ovolfiniun  25532  ovoliunlem1  25533  ovoliun2  25537  shft2rab  25539  ovolshftlem1  25540  sca2rab  25543  ovolscalem1  25544  ovolsca  25546  ovolicc1  25547  ovolicc2lem4  25551  ovolicopnf  25555  cmmbl  25565  nulmbl  25566  nulmbl2  25567  unmbl  25568  volinun  25577  volfiniun  25578  voliunlem1  25581  voliunlem3  25583  ioombl1lem3  25591  ioombl1lem4  25592  ovolioo  25599  ioorcl2  25603  uniioovol  25610  uniioombllem3  25616  uniioombllem4  25617  uniioombllem5  25618  uniioombllem6  25619  dyadovol  25624  dyaddisjlem  25626  opnmbllem  25632  vitalilem1  25639  vitalilem2  25640  vitalilem3  25641  vitalilem4  25642  ismbf  25659  mbfmulc2lem  25678  mbfmulc2re  25679  mbfmulc2  25694  mbfinf  25696  itg1val2  25715  itg11  25722  i1fmullem  25725  i1fadd  25726  itg1addlem4  25730  itg1addlem5  25731  i1fmulclem  25733  i1fmulc  25734  itg1mulc  25735  itg1sub  25740  itg10a  25741  itg1ge0a  25742  itg1climres  25745  mbfi1fseqlem3  25748  mbfi1fseqlem4  25749  mbfi1fseqlem5  25750  mbfi1fseqlem6  25751  mbfi1flimlem  25753  mbfmullem2  25755  itg2const  25771  itg2const2  25772  itg2mulclem  25777  itg2mulc  25778  itg2splitlem  25779  itg2split  25780  itg2monolem1  25781  itg2monolem3  25783  itg2addlem  25789  itgcl  25815  itgcnlem  25821  itgrevallem1  25826  itgposval  25827  iblneg  25834  itgneg  25835  i1fibl  25839  itgitg1  25840  itgconst  25850  ibladd  25852  itgaddlem2  25855  iblabslem  25859  iblabs  25860  iblabsr  25861  iblmulc2  25862  itgmulc2lem2  25864  itgmulc2  25865  itgabs  25866  itgsplit  25867  bddmulibl  25870  bddiblnc  25873  dvcjbr  25980  dvfre  25982  dvexp3  26009  dveflem  26010  dvferm1lem  26015  dvferm2lem  26017  rolle  26021  cmvth  26022  mvth  26023  dvlip  26024  dvlipcn  26025  c1liplem1  26027  c1lip1  26028  dveq0  26031  dv11cn  26032  dvlt0  26036  dvle  26038  dvivthlem1  26039  dvivth  26041  lhop1lem  26044  lhop1  26045  lhop2  26046  lhop  26047  dvcvx  26051  dvfsumle  26052  dvfsumge  26053  dvfsumabs  26054  dvfsumlem1  26057  dvfsumlem2  26058  dvfsumlem4  26060  dvfsumrlimge0  26061  dvfsumrlim2  26063  dvfsum2  26065  ftc1a  26068  ftc1lem4  26070  ftc1lem5  26071  itgpowd  26081  plyeq0lem  26239  coemulhi  26283  plyrecj  26310  plydivlem3  26325  aalioulem2  26363  aalioulem3  26364  aalioulem4  26365  aalioulem5  26366  aalioulem6  26367  aaliou  26368  aaliou2  26370  aaliou2b  26371  aaliou3lem3  26374  aaliou3lem7  26379  aaliou3lem9  26380  taylthlem2  26403  ulmcn  26428  ulmdvlem1  26429  mtest  26433  mtestbdd  26434  itgulm  26437  radcnvlem1  26442  radcnvlem2  26443  radcnvlt1  26447  radcnvle  26449  dvradcnv  26450  pserulm  26451  abelthlem2  26461  abelthlem5  26464  abelthlem7  26467  abelth2  26471  reeff1olem  26475  efcvx  26478  pilem2  26481  pilem3  26482  sincosq2sgn  26530  sincosq3sgn  26531  sincosq4sgn  26532  coseq0negpitopi  26534  tanrpcl  26535  tangtx  26536  tanabsge  26537  sinq12gt0  26538  sinq34lt0t  26540  cosq14gt0  26541  cosq14ge0  26542  pige3ALT  26551  coskpi  26554  cos02pilt1  26557  cosordlem  26561  sinord  26565  tanord1  26568  tanord  26569  tanregt0  26570  efif1olem2  26574  efif1olem4  26576  eff1olem  26579  logrnaddcl  26605  logneg  26619  lognegb  26621  reexplog  26626  relogexp  26627  logfac  26632  efiarg  26638  cosargd  26639  cosarg0d  26640  argregt0  26641  argrege0  26642  argimgt0  26643  logneg2  26646  logmul2  26647  logdiv2  26648  abslogle  26649  tanarg  26650  logdivlti  26651  divlogrlim  26666  logcnlem2  26674  logcnlem3  26675  logcnlem4  26676  logcn  26678  logf1o2  26681  advlog  26685  advlogexp  26686  efopnlem1  26687  logtayllem  26690  logtayl  26691  logccv  26694  logcxp  26700  mulcxp  26716  divcxp  26718  cxpmul  26719  cxproot  26721  cxpmul2z  26722  abscxp  26723  abscxp2  26724  cxplt  26725  cxplea  26727  cxple2  26728  cxple2a  26730  cxplt3  26731  cxpsqrtlem  26733  cxpsqrt  26734  logsqrt  26735  dvcxp2  26772  cxpcn3lem  26778  resqrtcn  26780  cxpaddlelem  26782  cxpaddle  26783  abscxpbnd  26784  root1id  26785  root1eq1  26786  root1cj  26787  cxpeq  26788  loglesqrt  26792  relogbmul  26808  nnlogbexp  26812  logbrec  26813  cosangneg2d  26838  angrtmuld  26839  ang180lem2  26841  lawcoslem1  26846  lawcos  26847  pythag  26848  isosctrlem1  26849  isosctrlem2  26850  isosctrlem3  26851  ssscongptld  26853  chordthmlem  26863  chordthmlem2  26864  chordthmlem3  26865  chordthmlem4  26866  chordthmlem5  26867  heron  26869  asinsinlem  26922  reasinsin  26927  acosrecl  26934  atancj  26941  atanrecl  26942  atanlogaddlem  26944  atanlogsublem  26946  atanbndlem  26956  atans2  26962  ressatans  26965  atantayl  26968  leibpilem2  26972  leibpi  26973  leibpisum  26974  log2tlbnd  26976  log2ublem2  26978  birthdaylem2  26983  birthdaylem3  26984  cxp2limlem  27006  cxp2lim  27007  cxploglim  27008  cxploglim2  27009  divsqrtsumo1  27014  cvxcl  27015  scvxcvx  27016  jensenlem2  27018  jensen  27019  amgmlem  27020  logdiflbnd  27025  emcllem2  27027  emcllem3  27028  emcllem5  27030  emcllem6  27031  emcllem7  27032  harmonicbnd4  27041  fsumharmonic  27042  zetacvg  27045  lgamgulmlem2  27060  lgamgulmlem3  27061  lgamgulmlem4  27062  lgamgulmlem5  27063  lgamgulmlem6  27064  lgamgulm2  27066  lgambdd  27067  lgamcvg2  27085  gamcvg  27086  gamcvg2lem  27089  regamcl  27091  relgamcl  27092  lgam1  27094  ftalem1  27103  ftalem2  27104  ftalem4  27106  ftalem5  27107  basellem3  27113  basellem4  27114  basellem5  27115  basellem6  27116  basellem7  27117  basellem8  27118  basellem9  27119  efnnfsumcl  27133  chtprm  27183  chpp1  27185  chtdif  27188  efchtdvds  27189  prmorcht  27208  mumullem2  27210  fsumfldivdiaglem  27219  ppiub  27234  chtleppi  27240  chtublem  27241  chtub  27242  pclogsum  27245  vmasum  27246  logfac2  27247  chpval2  27248  chpchtsum  27249  chpub  27250  logfaclbnd  27252  logfacbnd3  27253  logfacrlim  27254  logexprlim  27255  logfacrlim2  27256  mersenne  27257  dchrabs  27290  dchrptlem1  27294  dchrptlem2  27295  bcmax  27308  bcp1ctr  27309  bposlem1  27314  bposlem9  27322  lgsvalmod  27346  lgsdilem  27354  lgsne0  27365  lgsqrlem2  27377  gausslemma2dlem1a  27395  gausslemma2dlem6  27402  lgseisenlem1  27405  lgseisenlem2  27406  lgseisen  27409  lgsquadlem1  27410  lgsquadlem2  27411  mul2sq  27449  2sqlem3  27450  2sqlem8  27456  2sqmod  27466  2sqreulem1  27476  2sqreunnlem1  27479  chebbnd1lem1  27499  chebbnd1lem2  27500  chebbnd1lem3  27501  chtppilimlem1  27503  chtppilimlem2  27504  chtppilim  27505  chto1ub  27506  chto1lb  27508  chpchtlim  27509  chpo1ub  27510  vmadivsum  27512  vmadivsumb  27513  rplogsumlem1  27514  rplogsumlem2  27515  rpvmasumlem  27517  dchrisumlema  27518  dchrisumlem1  27519  dchrisumlem2  27520  dchrisumlem3  27521  dchrmusumlema  27523  dchrmusum2  27524  dchrvmasumlem1  27525  dchrvmasum2lem  27526  dchrvmasum2if  27527  dchrvmasumlem2  27528  dchrvmasumlem3  27529  dchrvmasumiflem1  27531  dchrvmasumiflem2  27532  dchrisum0flblem1  27538  dchrisum0fno1  27541  rpvmasum2  27542  dchrisum0re  27543  dchrisum0lema  27544  dchrisum0lem1b  27545  dchrisum0lem1  27546  dchrisum0lem2a  27547  dchrisum0lem2  27548  dchrisum0lem3  27549  dchrmusumlem  27552  dchrvmasumlem  27553  rpvmasum  27556  rplogsum  27557  dirith2  27558  mudivsum  27560  mulogsumlem  27561  mulogsum  27562  logdivsum  27563  mulog2sumlem1  27564  mulog2sumlem2  27565  mulog2sumlem3  27566  vmalogdivsum2  27568  vmalogdivsum  27569  2vmadivsumlem  27570  logsqvma  27572  logsqvma2  27573  log2sumbnd  27574  selberglem1  27575  selberglem2  27576  selberglem3  27577  selberg  27578  selbergb  27579  selberg2lem  27580  selberg2  27581  selberg2b  27582  chpdifbndlem1  27583  logdivbnd  27586  selberg3lem1  27587  selberg3lem2  27588  selberg3  27589  selberg4lem1  27590  selberg4  27591  pntrmax  27594  pntrsumo1  27595  pntrsumbnd  27596  pntrsumbnd2  27597  selbergr  27598  selberg3r  27599  selberg4r  27600  selberg34r  27601  pntsval2  27606  pntrlog2bndlem1  27607  pntrlog2bndlem2  27608  pntrlog2bndlem3  27609  pntrlog2bndlem4  27610  pntrlog2bndlem5  27611  pntrlog2bndlem6a  27612  pntrlog2bndlem6  27613  pntrlog2bnd  27614  pntpbnd1a  27615  pntpbnd1  27616  pntpbnd2  27617  pntibndlem2  27621  pntibndlem3  27622  pntlemb  27627  pntlemg  27628  pntlemh  27629  pntlemn  27630  pntlemr  27632  pntlemj  27633  pntlemf  27635  pntlemk  27636  pntlemo  27637  pntlem3  27639  pntleml  27641  pnt2  27643  pnt  27644  abvcxp  27645  ostth2lem1  27648  qabvexp  27656  padicabv  27660  padicabvcxp  27662  ostth2lem2  27664  ostth2lem3  27665  ostth2lem4  27666  ostth2  27667  ostth3  27668  ttgcontlem1  29020  fveecn  29038  eqeelen  29040  brbtwn2  29041  colinearalglem4  29045  colinearalg  29046  axsegconlem9  29061  axsegconlem10  29062  ax5seglem1  29064  ax5seglem2  29065  ax5seglem3  29067  ax5seglem5  29069  ax5seglem6  29070  ax5seglem9  29073  ax5seg  29074  axbtwnid  29075  axpaschlem  29076  axpasch  29077  axeuclidlem  29098  axcontlem2  29101  axcontlem4  29103  axcontlem7  29106  axcontlem8  29107  elntg2  29121  nrt2irr  30610  nvm1  30803  nvpi  30805  nvz0  30806  nvmtri  30809  nvabs  30810  nvge0  30811  nv1  30813  smcnlem  30835  ipval2lem4  30844  ipval2  30845  4ipval2  30846  ipidsq  30848  dipcj  30852  dip0r  30855  ipz  30857  nmoub3i  30911  nmlno0lem  30931  nmblolbii  30937  blocnilem  30942  cncph  30957  ipasslem4  30972  ipasslem5  30973  ipblnfi  30993  minvecolem2  31013  minvecolem4  31018  minvecolem6  31020  minvecolem7  31021  htthlem  31055  normpyc  31284  hhph  31316  bcs2  31320  norm1  31387  norm1exi  31388  pjhthlem1  31529  eigvalcl  32099  eighmorth  32102  nmlnop0iALT  32133  nmbdoplbi  32162  nmcexi  32164  nmcoplbi  32166  nmbdfnlbi  32187  nmcfnlbi  32190  riesz4i  32201  cnlnadjlem2  32206  cnlnadjlem7  32211  nmopcoi  32233  nmopcoadji  32239  branmfn  32243  leopnmid  32276  opsqrlem1  32278  hst1h  32365  hstle  32368  hstoh  32370  sto2i  32375  stadd3i  32386  strlem1  32388  golem1  32409  stcltrlem1  32414  cdj1i  32571  cdj3lem1  32572  cdj3lem3b  32578  cdj3i  32579  sgnval2  32876  re0cj  32884  receqid  32885  pythagreim  32886  lt2addrd  32891  le2halvesd  32897  fzsplit3  32934  bcm1n  32936  expgt0b  32958  fsumiunle  32970  sgnmul  32976  sgnsub  32978  nexple  32985  expevenpos  32987  oexpled  32988  wrdt2ind  33081  psgnfzto1stlem  33230  ccfldsrarelvec  33912  ccfldextdgrr  33913  constrrtll  33972  constrrtlc1  33973  constrrtlc2  33974  constrconj  33986  nn0constr  34002  constrnegcl  34004  constrdircl  34006  iconstr  34007  constrremulcl  34008  constrrecl  34010  constrimcl  34011  constrmulcl  34012  constrreinvcl  34013  constrinvcl  34014  constrresqrtcl  34018  constrabscl  34019  constrsqrtcl  34020  cos9thpiminplylem1  34023  sqsscirc1  34149  sqsscirc2  34150  cnre2csqima  34152  rmulccn  34169  xrge0iifcnv  34174  xrge0iifhom  34178  zrhnm  34208  rezh  34210  esumpcvgval  34319  esumcvgsum  34329  dya2ub  34511  dya2icoseg  34518  omssubadd  34541  eulerpartlemgc  34603  ballotlemsi  34756  plymulx0  34788  signsply0  34792  signsvtp  34824  signsvtn  34825  signsvfpn  34826  signsvfnn  34827  divsqrtid  34835  reprgt  34862  reprinfz1  34863  breprexplemc  34873  circlemethhgt  34884  hgt750lemd  34889  hgt750lemf  34894  hgt750lemg  34895  hgt750lemb  34897  hgt750lema  34898  hgt750leme  34899  tgoldbachgtde  34901  subfacval2  35475  subfaclim  35476  subfacval3  35477  resconn  35534  sinccvglem  35960  circum  35962  climlec3  36022  faclimlem1  36031  faclimlem2  36032  faclimlem3  36033  faclim  36034  iprodfac  36035  faclim2  36036  dnicld1  36848  dnizeq0  36851  dnizphlfeqhlf  36852  dnibndlem2  36855  dnibndlem3  36856  dnibndlem5  36858  dnibndlem6  36859  dnibndlem7  36860  dnibndlem8  36861  dnibndlem9  36862  dnibndlem10  36863  dnibndlem11  36864  dnibndlem12  36865  dnibndlem13  36866  dnibnd  36867  dnicn  36868  knoppcnlem4  36872  knoppcnlem5  36873  knoppcnlem6  36874  knoppcnlem8  36876  knoppcnlem9  36877  knoppcnlem10  36878  knoppcnlem11  36879  unblimceq0  36883  unbdqndv2lem1  36885  unbdqndv2lem2  36886  knoppndvlem1  36888  knoppndvlem6  36893  knoppndvlem8  36895  knoppndvlem9  36896  knoppndvlem10  36897  knoppndvlem11  36898  knoppndvlem12  36899  knoppndvlem14  36901  knoppndvlem15  36902  knoppndvlem17  36904  knoppndvlem18  36905  knoppndvlem19  36906  knoppndvlem20  36907  knoppndvlem21  36908  irrdifflemf  37755  irrdiff  37756  qdiff  37757  ltflcei  38045  sin2h  38047  cos2h  38048  tan2h  38049  poimirlem29  38086  opnmbllem0  38093  mblfinlem2  38095  mblfinlem3  38096  mblfinlem4  38097  mbfposadd  38104  itg2addnclem  38108  itg2addnclem2  38109  itg2addnclem3  38110  itg2addnc  38111  itg2gt0cn  38112  ibladdnc  38114  itgaddnclem2  38116  iblabsnclem  38120  iblabsnc  38121  iblmulc2nc  38122  itgmulc2nclem2  38124  itgmulc2nc  38125  itgabsnc  38126  ftc1cnnclem  38128  ftc1cnnc  38129  ftc1anclem1  38130  ftc1anclem2  38131  ftc1anclem3  38132  ftc1anclem4  38133  ftc1anclem5  38134  ftc1anclem6  38135  ftc1anclem7  38136  ftc1anclem8  38137  ftc1anc  38138  areacirclem1  38145  areacirclem5  38149  areacirc  38150  mettrifi  38194  lmclim2  38195  geomcau  38196  isbnd3  38221  ssbnd  38225  cntotbnd  38233  bfplem1  38259  bfplem2  38260  bfp  38261  rrnmet  38266  rrndstprj1  38267  rrndstprj2  38268  rrncmslem  38269  rrnequiv  38272  rrntotbnd  38273  ismrer1  38275  lcmineqlem18  42601  lcmineqlem19  42602  lcmineqlem20  42603  lcmineqlem21  42604  lcmineqlem22  42605  3lexlogpow5ineq2  42610  3lexlogpow2ineq1  42613  3lexlogpow2ineq2  42614  3lexlogpow5ineq5  42615  dvrelogpow2b  42623  aks4d1p1p2  42625  aks4d1p1p4  42626  dvle2  42627  aks4d1p1p6  42628  aks4d1p1p7  42629  aks4d1p1p5  42630  aks4d1p1  42631  aks4d1p3  42633  aks4d1p5  42635  aks4d1p6  42636  aks4d1p7d1  42637  aks4d1p7  42638  aks4d1p8d2  42640  aks4d1p8  42642  posbezout  42655  aks6d1c1  42671  hashscontpow1  42676  aks6d1c3  42678  aks6d1c4  42679  aks6d1c2lem4  42682  aks6d1c2  42685  aks6d1c5lem3  42692  aks6d1c5lem2  42693  2np3bcnp1  42699  sticksstones6  42706  sticksstones10  42710  sticksstones12a  42712  sticksstones12  42713  aks6d1c6lem4  42728  bcled  42733  bcle2d  42734  aks6d1c7lem1  42735  aks6d1c7lem2  42736  remulcan2d  42810  readdridaddlidd  42811  readdrcl2d  42820  sumcubes  42860  oexpreposd  42869  expeqidd  42872  rxp112d  42892  rxp11d  42895  readvrec2  42908  readvrec  42909  resuppsinopn  42910  readvcot  42911  resubeulem1  42922  resubeulem2  42923  readdsub  42931  resubsub4  42936  resubidaddlidlem  42941  resubdi  42943  sn-addlid  42951  remul02  42952  remul01  42954  renegneg  42959  readdcan2  42960  renegid2  42961  sn-it0e0  42963  sn-negex12  42964  reixi  42970  remulinvcom  42980  remullid  42981  remulcand  42986  rediveud  42990  redivrec2d  43007  rediv23d  43008  redivdird  43009  sn-0tie0  43011  zaddcomlem  43023  zaddcom  43024  renegmulnnass  43025  mulgt0b1d  43032  mulgt0b2d  43038  mullt0b1d  43043  sn-itrere  43048  sn-retire  43049  cnreeu  43050  frlmvscadiccat  43066  abvexp  43088  dffltz  43154  fltnltalem  43182  fltnlta  43183  negexpidd  43201  3cubeslem1  43203  3cubeslem2  43204  3cubeslem4  43208  eldioph2lem1  43279  lzenom  43289  rencldnfilem  43335  irrapxlem1  43337  irrapxlem2  43338  irrapxlem3  43339  irrapxlem4  43340  irrapxlem5  43341  pellexlem2  43345  pellexlem6  43349  pell1234qrreccl  43369  pell14qrgt0  43374  pell14qrdivcl  43380  pell14qrexpclnn0  43381  pell14qrexpcl  43382  pell14qrdich  43384  pell1qrgaplem  43388  pellfundex  43401  reglogmul  43408  reglogexp  43409  reglogbas  43410  reglog1  43411  pellfund14  43413  rmspecfund  43424  monotoddzzfi  43457  jm2.24nn  43474  jm2.17a  43475  jm2.17b  43476  jm2.17c  43477  jm2.24  43478  acongrep  43495  fzmaxdif  43496  acongeq  43498  modabsdifz  43501  jm2.19lem4  43507  jm2.19  43508  jm2.26lem3  43516  jm3.1lem1  43532  jm3.1lem2  43533  areaquad  43731  sqrtcvallem4  44153  sqrtcval  44155  sqrtcval2  44156  absmulrposd  44673  extoimad  44678  imo72b2lem0  44679  imo72b2lem1  44683  imo72b2  44686  int-addcomd  44687  int-addassocd  44688  int-addsimpd  44689  int-mulcomd  44690  int-mulassocd  44691  int-mulsimpd  44692  int-leftdistd  44693  int-rightdistd  44694  int-sqdefd  44695  int-mul11d  44696  int-mul12d  44697  int-add01d  44698  int-add02d  44699  int-sqgeq0d  44700  int-eqmvtd  44703  cvgdvgrat  44827  radcnvrat  44828  hashnzfzclim  44836  dvconstbi  44848  binomcxplemnn0  44863  binomcxplemnotnn0  44870  isosctrlem1ALT  45447  sineq0ALT  45450  infnsuprnmpt  45763  oddfl  45795  dstregt0  45799  zltlesub  45802  lt3addmuld  45818  fperiodmullem  45820  fperiodmul  45821  lt4addmuld  45823  fzdifsuc2  45827  supxrgere  45847  supxrgelem  45851  suplesup  45853  supsubc  45867  xralrple2  45868  abslt2sqd  45874  xralrple3  45887  reclt0d  45900  ltmulneg  45905  rexabslelem  45930  supminfrnmpt  45957  leneg2d  45960  leneg3d  45969  supminfxr  45976  absimnre  45988  absimlere  45991  iooabslt  46013  iccshift  46032  iooshift  46036  sqrlearg  46067  fmul01  46094  fmul01lt1lem1  46098  fmul01lt1lem2  46099  fprodabs2  46109  climinf  46120  limcrecl  46143  lptre2pt  46152  limcleqr  46156  0ellimcdiv  46161  limclner  46163  climleltrp  46188  climinf2mpt  46226  climinf3  46228  climxrre  46262  climliminflimsupd  46313  liminfltlem  46316  liminflimsupclim  46319  cnrefiisplem  46341  sinaover2ne0  46380  cncfperiod  46391  ioccncflimc  46397  cncficcgt0  46400  icocncflimc  46401  cncfshiftioo  46404  cncfiooicc  46406  fperdvper  46431  dvbdfbdioolem1  46440  dvbdfbdioolem2  46441  dvbdfbdioo  46442  ioodvbdlimc1lem1  46443  ioodvbdlimc1lem2  46444  ioodvbdlimc1  46445  ioodvbdlimc2lem  46446  ioodvbdlimc2  46447  dvnmul  46455  dvnprodlem1  46458  dvnprodlem2  46459  itgcoscmulx  46481  volioc  46484  itgsincmulx  46486  itgiccshift  46492  itgperiod  46493  itgsbtaddcnst  46494  volico  46495  voliooico  46504  voliccico  46511  stoweidlem7  46519  stoweidlem11  46523  stoweidlem13  46525  stoweidlem17  46529  stoweidlem19  46531  stoweidlem20  46532  stoweidlem21  46533  stoweidlem22  46534  stoweidlem23  46535  stoweidlem24  46536  stoweidlem26  46538  stoweidlem32  46544  stoweidlem36  46548  stoweidlem44  46556  stoweidlem47  46559  wallispilem3  46579  wallispi2lem1  46583  stirlinglem1  46586  stirlinglem5  46590  stirlinglem11  46596  stirlinglem12  46597  stirlinglem14  46599  dirkerval2  46606  dirkerre  46607  dirkertrigeqlem2  46611  dirkertrigeq  46613  dirkeritg  46614  dirkercncflem1  46615  dirkercncflem2  46616  dirkercncflem4  46618  fourierdlem4  46623  fourierdlem6  46625  fourierdlem7  46626  fourierdlem13  46632  fourierdlem14  46633  fourierdlem16  46635  fourierdlem18  46637  fourierdlem19  46638  fourierdlem21  46640  fourierdlem22  46641  fourierdlem24  46643  fourierdlem26  46645  fourierdlem28  46647  fourierdlem30  46649  fourierdlem35  46654  fourierdlem39  46658  fourierdlem40  46659  fourierdlem41  46660  fourierdlem42  46661  fourierdlem43  46662  fourierdlem44  46663  fourierdlem47  46665  fourierdlem48  46666  fourierdlem49  46667  fourierdlem50  46668  fourierdlem51  46669  fourierdlem53  46671  fourierdlem56  46674  fourierdlem57  46675  fourierdlem58  46676  fourierdlem59  46677  fourierdlem60  46678  fourierdlem61  46679  fourierdlem62  46680  fourierdlem63  46681  fourierdlem64  46682  fourierdlem65  46683  fourierdlem66  46684  fourierdlem68  46686  fourierdlem70  46688  fourierdlem71  46689  fourierdlem72  46690  fourierdlem73  46691  fourierdlem74  46692  fourierdlem75  46693  fourierdlem76  46694  fourierdlem77  46695  fourierdlem78  46696  fourierdlem79  46697  fourierdlem80  46698  fourierdlem81  46699  fourierdlem83  46701  fourierdlem84  46702  fourierdlem85  46703  fourierdlem87  46705  fourierdlem88  46706  fourierdlem89  46707  fourierdlem90  46708  fourierdlem91  46709  fourierdlem92  46710  fourierdlem93  46711  fourierdlem95  46713  fourierdlem97  46715  fourierdlem101  46719  fourierdlem103  46721  fourierdlem104  46722  fourierdlem107  46725  fourierdlem109  46727  fourierdlem111  46729  fourierdlem112  46730  fouriercnp  46738  sqwvfoura  46740  sqwvfourb  46741  fouriersw  46743  etransclem14  46760  etransclem18  46764  etransclem23  46769  etransclem24  46770  etransclem27  46773  etransclem46  46792  etransclem48  46794  qndenserrnbllem  46806  ioorrnopnlem  46816  sge0tsms  46892  sge0cl  46893  sge0split  46921  sge0iunmptlemfi  46925  sge0rpcpnf  46933  sge0isum  46939  sge0ad2en  46943  sge0xaddlem1  46945  sge0xaddlem2  46946  sge0gtfsumgt  46955  sge0seq  46958  meadif  46991  meaiininclem  46998  carageniuncllem1  47033  carageniuncllem2  47034  hoicvr  47060  hoicvrrex  47068  ovnsubaddlem1  47082  hsphoidmvle2  47097  hsphoidmvle  47098  hoidmvval0  47099  hoiprodp1  47100  hoidmv1lelem1  47103  hoidmv1lelem2  47104  hoidmv1le  47106  hoidmvlelem1  47107  hoidmvlelem2  47108  hoidmvlelem3  47109  hoiqssbllem2  47135  hspmbllem1  47138  ovolval2lem  47155  ovolval3  47159  ovolval5lem1  47164  ovnovollem1  47168  ovnovollem2  47169  vonioolem1  47192  vonioo  47194  vonicclem1  47195  vonicc  47197  smfaddlem1  47275  smflimlem4  47286  smfmullem1  47303  smfmullem2  47304  smfmullem3  47305  smfdiv  47309  smfneg  47315  sigaras  47367  sigarms  47368  sigarls  47369  sigarexp  47371  sigarperm  47372  sigarimcd  47374  sigarcol  47376  sharhght  47377  cevathlem2  47380  readdcnnred  47835  resubcnnred  47836  cndivrenred  47838  flmrecm1  47875  fldivmod  47876  ceildivmod  47877  m1mod0mod1  47892  m1modmmod  47896  difmodm1lt  47897  requad01  48181  requad1  48182  requad2  48183  fpprwppr  48299  bgoldbtbndlem2  48366  gpgvtxedg1  48624  ltsubaddb  49074  ltsubsubb  49075  ltsubadd2b  49076  flsubz  49082  logblt1b  49124  dignn0fr  49161  dignn0flhalflem1  49175  dignn0flhalflem2  49176  nn0sumshdiglemA  49179  affinecomb1  49262  affinecomb2  49263  resum2sqorgt0  49269  rrx2pnedifcoorneor  49276  rrx2pnedifcoorneorr  49277  ehl2eudisval0  49285  eenglngeehlnmlem1  49297  eenglngeehlnmlem2  49298  rrx2vlinest  49301  rrx2linest  49302  rrx2linest2  49304  2sphere0  49310  line2ylem  49311  line2  49312  line2xlem  49313  line2x  49314  line2y  49315  itscnhlc0yqe  49319  itschlc0yqe  49320  itsclc0yqsol  49324  itscnhlc0xyqsol  49325  itschlc0xyqsol1  49326  itschlc0xyqsol  49327  itsclc0xyqsolr  49329  itsclinecirc0b  49334  itsclquadb  49336  itsclquadeu  49337  2itscplem1  49338  2itscplem2  49339  2itscplem3  49340  2itscp  49341  itscnhlinecirc02plem1  49342  itscnhlinecirc02plem2  49343  itscnhlinecirc02p  49345  inlinecirc02plem  49346  inlinecirc02p  49347  amgmwlem  50361  amgmlemALT  50362