Theorem recnd 11374

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 11327	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11235  ℝcr 11236

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-resscn 11294

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  00id  11522  mul02lem1  11523  addrid  11527  cnegex  11528  ltadd1  11821  leadd2  11823  ltsubadd  11824  ltsubadd2  11825  lesubadd  11826  lesubadd2  11827  lesub1  11848  lesub2  11849  ltnegcon1  11855  ltnegcon2  11856  add20  11866  subge0  11867  suble0  11868  lesub0  11871  mulge0  11872  eqord2  11885  lesub3d  11972  possumd  11979  sublt0d  11980  rereccl  12073  redivcl  12074  recgt0  12201  prodgt0  12202  ltmul1a  12204  ltdiv1  12219  ltmuldiv  12228  ltrec  12237  recp1lt1  12253  recreclt  12254  ledivp1  12257  supadd  12323  infrenegsup  12338  rimul  12349  cru  12350  avglt1  12622  avglt2  12623  lt2addmuld  12634  div4p1lem1div2  12639  nn0cnd  12707  zcn  12736  zeo  12823  zcnd  12842  eluzmn  13010  eluzelcn  13015  cnref1o  13151  rpcn  13169  rpcnd  13204  ltaddrp2d  13236  mul2lt0rlt0  13262  mul2lt0rgt0  13263  mul2lt0llt0  13264  mul2lt0lgt0  13265  mul2lt0bi  13266  prodge0rd  13267  prodge0ld  13268  qbtwnre  13367  xralrple  13373  xpncan  13419  xmulcom  13434  xmulneg1  13437  xlemul1  13458  elunitcn  13637  icoshftf1o  13643  lincmb01cmp  13664  iccf1o  13665  divfl0  14002  fladdz  14003  flzadd  14004  flhalf  14008  ceim1l  14025  intfracq  14037  fldiv  14038  modvalr  14050  flpmodeq  14052  mod0  14054  modlt  14058  moddiffl  14060  modfrac  14062  flmod  14063  intfrac  14064  modmulnn  14067  modvalp1  14068  modid  14074  modcyc  14084  modadd1  14086  modaddb  14087  modaddabs  14089  modmuladdnn0  14096  negmod  14097  modadd2mod  14102  modnegd  14107  modadd12d  14108  modsub12d  14109  modmulmodr  14118  modaddmulmod  14119  moddi  14120  modsubdir  14121  modeqmodmin  14122  modirr  14123  addmodlteq  14127  seqf1olem1  14222  serle  14238  expcl2lem  14254  expnegz  14277  expaddzlem  14286  expaddz  14287  expmulz  14289  sq11  14312  ltexp2a  14347  expmordi  14348  leexp2a  14353  leexp2r  14355  exple1  14358  expubnd  14359  bernneq2  14413  expmulnbnd  14418  discr1  14422  discr  14423  faclbnd  14473  bcp1nk  14500  cshweqrep  15012  sgnsub  15300  sgnmul  15301  remim  15325  reim0b  15327  rereb  15328  mulre  15329  cjreb  15331  recj  15332  reneg  15333  readd  15334  resub  15335  remullem  15336  remul2  15338  rediv  15339  imcj  15340  imneg  15341  imadd  15342  imsub  15343  immul2  15345  imdiv  15346  cjcj  15348  cjadd  15349  ipcnval  15351  cjmulval  15353  cjneg  15355  imval2  15359  cjreim2  15369  01sqrexlem5  15454  01sqrexlem7  15456  resqrtthlem  15462  remsqsqrt  15464  sqrtmul  15467  sqrtdiv  15473  sqrtneg  15475  sqrtmsq  15478  absdiv  15503  absid  15504  absexp  15512  absexpz  15513  absimle  15517  abslt  15523  absle  15524  abssubne0  15525  releabs  15530  recval  15531  abstri  15539  abs2difabs  15543  abs1m  15544  abslem2  15548  absrdbnd  15550  sqreulem  15568  sqreu  15569  amgm2  15578  icodiamlt  15646  bhmafibid1  15676  bhmafibid2  15677  lo1bddrp  15733  o1lo1  15745  rlimrecl  15788  rlimge0  15789  climrecl  15791  climge0  15792  climabs0  15793  reccn2  15805  o1rlimmul  15827  lo1mul2  15837  lo1sub  15839  climle  15848  climsqz  15849  climsqz2  15850  rlimsqz  15858  rlimsqz2  15859  climlec2  15867  isercolllem1  15873  climsup  15878  caucvgrlem  15881  caurcvgr  15882  caucvgrlem2  15883  iseraltlem1  15890  iseraltlem2  15891  iseraltlem3  15892  iseralt  15893  isumrecl  15972  isumge0  15973  fsumless  16004  fsumge1  16005  fsum00  16006  fsumle  16007  fsumlt  16008  fsumabs  16009  o1fsum  16021  seqabs  16022  cvgcmp  16024  cvgcmpce  16026  abscvgcvg  16027  indsum  16036  indsumhash  16037  isumrpcl  16053  isumle  16054  isumless  16055  isumsup  16057  climcndslem1  16059  climcndslem2  16060  climcnds  16061  flo1  16064  supcvg  16066  trireciplem  16072  trirecip  16073  explecnv  16075  geo2sum  16083  geo2lim  16085  geomulcvg  16086  cvgrat  16093  mertenslem1  16094  mertenslem2  16095  fprodabs  16182  fprodle  16204  iprodrecl  16210  bpolydiflem  16261  bpoly4  16266  efcllem  16284  ege2le3  16297  efaddlem  16300  efgt0  16312  eftlub  16318  effsumlt  16320  eflt  16326  eflegeo  16330  resin4p  16347  recos4p  16348  retanhcl  16368  tanhlt1  16369  efeul  16371  ef01bndlem  16393  sin01bnd  16394  cos01bnd  16395  sin01gt0  16399  cos01gt0  16400  sin02gt0  16401  absefi  16405  absef  16406  absefib  16407  efieq1re  16408  eirrlem  16413  rpnnen2lem5  16427  rpnnen2lem8  16430  rpnnen2lem9  16431  rpnnen2lem11  16433  rpnnen2lem12  16434  moddvds  16474  odd2np1  16552  divalglem5  16608  bitsp1o  16644  bitsfzo  16646  bitscmp  16649  sadcaddlem  16668  nn0seqcvgd  16786  sqnprm  16919  isprm5  16924  nonsq  16976  eulerthlem2  17000  prmdiveq  17004  odzdvds  17014  vfermltlALT  17021  pythagtriplem14  17047  pcid  17092  fldivp1  17116  pcfac  17118  pockthlem  17124  prmreclem3  17137  prmreclem4  17138  prmreclem5  17139  prmrec  17141  4sqlem5  17161  4sqlem10  17166  mul4sqlem  17172  4sqlem15  17178  4sqlem16  17179  mulgneg  19343  ghmmulg  19483  odmodnn0  19796  mndodconglem  19797  pgpfaclem2  20340  isabvd  21111  abv1z  21123  abvneg  21125  abvrec  21127  abvdiv  21128  abvdom  21129  rege0subm  21773  cnsubrg  21777  gzrngunitlem  21782  regsumfsum  21785  prmirredlem  21822  remulg  21957  rzgrp  21973  bl2in  24763  blhalf  24768  blssps  24787  blss  24788  methaus  24883  nrmmetd  24937  nm2dif  24988  nminvr  25032  nmdvr  25033  nlmmul0or  25046  nrginvrcnlem  25054  nmolb2d  25081  nmoi2  25093  nmoleub  25094  nmo0  25098  nmoeq0  25099  nmoco  25100  nmotri  25102  nmoid  25105  blcvx  25161  xrsxmet  25173  recld2  25178  reconnlem2  25191  opnreen  25195  metdstri  25215  metnrmlem3  25225  icchmeo  25306  icopnfcnv  25307  icopnfhmeo  25308  iccpnfhmeo  25310  xrhmeo  25311  icccvx  25315  cnheiborlem  25319  evth  25324  lebnumii  25331  pcoass  25389  pcorevlem  25391  pcorev2  25393  pi1xfrcnv  25422  nmoleub2lem  25479  nmoleub2lem3  25480  nmoleub3  25484  ncvsm1  25519  ncvspi  25521  ncvs1  25522  cphsqrtcl2  25551  ipcau2  25599  tcphcphlem1  25600  tcphcphlem2  25601  tcphcph  25602  cphipval2  25606  cphipval  25608  iscau3  25643  rrxnm  25756  rrxcph  25757  csbren  25764  trirn  25765  rrxmval  25770  rrxmetlem  25772  rrxmet  25773  rrxdstprj1  25774  ehl1eudis  25785  ehl2eudis  25787  minveclem2  25791  minveclem3b  25793  minveclem4  25797  minveclem6  25799  minveclem7  25800  pjthlem1  25802  ivthlem2  25817  ivthlem3  25818  ivth2  25820  ovolfsval  25835  ovollb2lem  25853  ovolctb  25855  ovolunlem1a  25861  ovolunnul  25865  ovolfiniun  25866  ovoliunlem1  25867  ovoliun2  25871  shft2rab  25873  ovolshftlem1  25874  sca2rab  25877  ovolscalem1  25878  ovolsca  25880  ovolicc1  25881  ovolicc2lem4  25885  ovolicopnf  25889  cmmbl  25899  nulmbl  25900  nulmbl2  25901  unmbl  25902  volinun  25911  volfiniun  25912  voliunlem1  25915  voliunlem3  25917  ioombl1lem3  25925  ioombl1lem4  25926  ovolioo  25933  ioorcl2  25937  uniioovol  25944  uniioombllem3  25950  uniioombllem4  25951  uniioombllem5  25952  uniioombllem6  25953  dyadovol  25958  dyaddisjlem  25960  opnmbllem  25966  vitalilem1  25973  vitalilem2  25974  vitalilem3  25975  vitalilem4  25976  ismbf  25993  mbfmulc2lem  26012  mbfmulc2re  26013  mbfmulc2  26028  mbfinf  26030  itg1val2  26049  itg11  26056  i1fmullem  26059  i1fadd  26060  itg1addlem4  26064  itg1addlem5  26065  i1fmulclem  26067  i1fmulc  26068  itg1mulc  26069  itg1sub  26074  itg10a  26075  itg1ge0a  26076  itg1climres  26079  mbfi1fseqlem3  26082  mbfi1fseqlem4  26083  mbfi1fseqlem5  26084  mbfi1fseqlem6  26085  mbfi1flimlem  26087  mbfmullem2  26089  itg2const  26105  itg2const2  26106  itg2mulclem  26111  itg2mulc  26112  itg2splitlem  26113  itg2split  26114  itg2monolem1  26115  itg2monolem3  26117  itg2addlem  26123  itgcl  26148  itgcnlem  26154  itgrevallem1  26159  itgposval  26160  iblneg  26167  itgneg  26168  i1fibl  26172  itgitg1  26173  itgconst  26183  ibladd  26185  itgaddlem2  26188  iblabslem  26192  iblabs  26193  iblabsr  26194  iblmulc2  26195  itgmulc2lem2  26197  itgmulc2  26198  itgabs  26199  itgsplit  26200  bddmulibl  26203  bddiblnc  26206  dvcjbr  26313  dvfre  26315  dvexp3  26342  dveflem  26343  dvferm1lem  26348  dvferm2lem  26350  rolle  26354  cmvth  26355  mvth  26356  dvlip  26357  dvlipcn  26358  c1liplem1  26360  c1lip1  26361  dveq0  26364  dv11cn  26365  dvlt0  26369  dvle  26371  dvivthlem1  26372  dvivth  26374  lhop1lem  26377  lhop1  26378  lhop2  26379  lhop  26380  dvcvx  26384  dvfsumle  26385  dvfsumge  26386  dvfsumabs  26387  dvfsumlem1  26390  dvfsumlem2  26391  dvfsumlem4  26393  dvfsumrlimge0  26394  dvfsumrlim2  26396  dvfsum2  26398  ftc1a  26401  ftc1lem4  26403  ftc1lem5  26404  itgpowd  26414  plyeq0lem  26573  coemulhi  26617  plyrecj  26642  plyn0mulidp  26646  plydivlem3  26660  aalioulem2  26706  aalioulem3  26707  aalioulem4  26708  aalioulem5  26709  aalioulem6  26710  aaliou  26711  aaliou2  26713  aaliou2b  26714  aaliou3lem3  26717  aaliou3lem7  26722  aaliou3lem9  26723  taylthlem2  26747  ulmcn  26772  ulmdvlem1  26773  mtest  26777  mtestbdd  26778  itgulm  26781  radcnvlem1  26786  radcnvlem2  26787  radcnvlt1  26791  radcnvle  26793  dvradcnv  26794  pserulm  26795  abelthlem2  26805  abelthlem5  26808  abelthlem7  26811  abelth2  26815  reeff1olem  26819  efcvx  26822  pilem2  26825  pilem3  26826  sincosq2sgn  26874  sincosq3sgn  26875  sincosq4sgn  26876  coseq0negpitopi  26878  tanrpcl  26879  tangtx  26880  tanabsge  26881  sinq12gt0  26882  sinq34lt0t  26884  cosq14gt0  26885  cosq14ge0  26886  pige3ALT  26894  coskpi  26897  cos02pilt1  26900  cosordlem  26904  sinord  26908  tanord1  26911  tanord  26912  tanregt0  26913  efif1olem2  26917  efif1olem4  26919  eff1olem  26922  logrnaddcl  26948  logneg  26962  lognegb  26964  reexplog  26969  relogexp  26970  logfac  26975  efiarg  26981  cosargd  26982  cosarg0d  26983  argregt0  26984  argrege0  26985  argimgt0  26986  logneg2  26989  logmul2  26990  logdiv2  26991  abslogle  26992  tanarg  26993  logdivlti  26994  divlogrlim  27009  logcnlem2  27017  logcnlem3  27018  logcnlem4  27019  logcn  27021  logf1o2  27024  advlog  27028  advlogexp  27029  efopnlem1  27030  logtayllem  27033  logtayl  27034  logccv  27037  logcxp  27043  mulcxp  27059  divcxp  27061  cxpmul  27062  cxproot  27064  cxpmul2z  27065  abscxp  27066  abscxp2  27067  cxplt  27068  cxplea  27070  cxple2  27071  cxple2a  27073  cxplt3  27074  cxpsqrtlem  27076  cxpsqrt  27077  logsqrt  27078  dvcxp2  27115  cxpcn3lem  27121  resqrtcn  27123  cxpaddlelem  27125  cxpaddle  27126  abscxpbnd  27127  root1id  27128  root1eq1  27129  root1cj  27130  cxpeq  27131  loglesqrt  27135  relogbmul  27151  nnlogbexp  27155  logbrec  27156  cosangneg2d  27181  angrtmuld  27182  ang180lem2  27184  lawcoslem1  27189  lawcos  27190  pythag  27191  isosctrlem1  27192  isosctrlem2  27193  isosctrlem3  27194  ssscongptld  27196  chordthmlem  27206  chordthmlem2  27207  chordthmlem3  27208  chordthmlem4  27209  chordthmlem5  27210  heron  27212  asinsinlem  27265  reasinsin  27270  acosrecl  27277  atancj  27284  atanrecl  27285  atanlogaddlem  27287  atanlogsublem  27289  atanbndlem  27299  atans2  27305  ressatans  27308  atantayl  27311  leibpilem2  27315  leibpi  27316  leibpisum  27317  log2tlbnd  27319  log2ublem2  27321  birthdaylem2  27326  birthdaylem3  27327  cxp2limlem  27349  cxp2lim  27350  cxploglim  27351  cxploglim2  27352  divsqrtsumo1  27357  cvxcl  27358  scvxcvx  27359  jensenlem2  27361  jensen  27362  amgmlem  27363  logdiflbnd  27368  emcllem2  27370  emcllem3  27371  emcllem5  27373  emcllem6  27374  emcllem7  27375  harmonicbnd4  27384  fsumharmonic  27385  zetacvg  27388  lgamgulmlem2  27403  lgamgulmlem3  27404  lgamgulmlem4  27405  lgamgulmlem5  27406  lgamgulmlem6  27407  lgamgulm2  27409  lgambdd  27410  lgamcvg2  27428  gamcvg  27429  gamcvg2lem  27432  regamcl  27434  relgamcl  27435  lgam1  27437  ftalem1  27446  ftalem2  27447  ftalem4  27449  ftalem5  27450  basellem3  27456  basellem4  27457  basellem5  27458  basellem6  27459  basellem7  27460  basellem8  27461  basellem9  27462  efnnfsumcl  27476  chtprm  27526  chpp1  27528  chtdif  27531  efchtdvds  27532  prmorcht  27551  mumullem2  27553  fsumfldivdiaglem  27562  ppiub  27577  chtleppi  27583  chtublem  27584  chtub  27585  pclogsum  27588  vmasum  27589  logfac2  27590  chpval2  27591  chpchtsum  27592  chpub  27593  logfaclbnd  27595  logfacbnd3  27596  logfacrlim  27597  logexprlim  27598  logfacrlim2  27599  mersenne  27600  dchrabs  27633  dchrptlem1  27637  dchrptlem2  27638  bcmax  27651  bcp1ctr  27652  bposlem1  27657  bposlem9  27665  lgsvalmod  27689  lgsdilem  27697  lgsne0  27708  lgsqrlem2  27720  gausslemma2dlem1a  27738  gausslemma2dlem6  27745  lgseisenlem1  27748  lgseisenlem2  27749  lgseisen  27752  lgsquadlem1  27753  lgsquadlem2  27754  mul2sq  27792  2sqlem3  27793  2sqlem8  27799  2sqmod  27809  2sqreulem1  27819  2sqreunnlem1  27822  chebbnd1lem1  27842  chebbnd1lem2  27843  chebbnd1lem3  27844  chtppilimlem1  27846  chtppilimlem2  27847  chtppilim  27848  chto1ub  27849  chto1lb  27851  chpchtlim  27852  chpo1ub  27853  vmadivsum  27855  vmadivsumb  27856  rplogsumlem1  27857  rplogsumlem2  27858  rpvmasumlem  27860  dchrisumlema  27861  dchrisumlem1  27862  dchrisumlem2  27863  dchrisumlem3  27864  dchrmusumlema  27866  dchrmusum2  27867  dchrvmasumlem1  27868  dchrvmasum2lem  27869  dchrvmasum2if  27870  dchrvmasumlem2  27871  dchrvmasumlem3  27872  dchrvmasumiflem1  27874  dchrvmasumiflem2  27875  dchrisum0flblem1  27881  dchrisum0fno1  27884  rpvmasum2  27885  dchrisum0re  27886  dchrisum0lema  27887  dchrisum0lem1b  27888  dchrisum0lem1  27889  dchrisum0lem2a  27890  dchrisum0lem2  27891  dchrisum0lem3  27892  dchrmusumlem  27895  dchrvmasumlem  27896  rpvmasum  27899  rplogsum  27900  dirith2  27901  mudivsum  27903  mulogsumlem  27904  mulogsum  27905  logdivsum  27906  mulog2sumlem1  27907  mulog2sumlem2  27908  mulog2sumlem3  27909  vmalogdivsum2  27911  vmalogdivsum  27912  2vmadivsumlem  27913  logsqvma  27915  logsqvma2  27916  log2sumbnd  27917  selberglem1  27918  selberglem2  27919  selberglem3  27920  selberg  27921  selbergb  27922  selberg2lem  27923  selberg2  27924  selberg2b  27925  chpdifbndlem1  27926  logdivbnd  27929  selberg3lem1  27930  selberg3lem2  27931  selberg3  27932  selberg4lem1  27933  selberg4  27934  pntrmax  27937  pntrsumo1  27938  pntrsumbnd  27939  pntrsumbnd2  27940  selbergr  27941  selberg3r  27942  selberg4r  27943  selberg34r  27944  pntsval2  27949  pntrlog2bndlem1  27950  pntrlog2bndlem2  27951  pntrlog2bndlem3  27952  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  pntrlog2bndlem6a  27955  pntrlog2bndlem6  27956  pntrlog2bnd  27957  pntpbnd1a  27958  pntpbnd1  27959  pntpbnd2  27960  pntibndlem2  27964  pntibndlem3  27965  pntlemb  27970  pntlemg  27971  pntlemh  27972  pntlemn  27973  pntlemr  27975  pntlemj  27976  pntlemf  27978  pntlemk  27979  pntlemo  27980  pntlem3  27982  pntleml  27984  pnt2  27986  pnt  27987  abvcxp  27988  ostth2lem1  27991  qabvexp  27999  padicabv  28003  padicabvcxp  28005  ostth2lem2  28007  ostth2lem3  28008  ostth2lem4  28009  ostth2  28010  ostth3  28011  ttgcontlem1  29508  fveecn  29526  eqeelen  29528  brbtwn2  29529  colinearalglem4  29533  colinearalg  29534  axsegconlem9  29549  axsegconlem10  29550  ax5seglem1  29552  ax5seglem2  29553  ax5seglem3  29555  ax5seglem5  29557  ax5seglem6  29558  ax5seglem9  29561  ax5seg  29562  axbtwnid  29563  axpaschlem  29564  axpasch  29565  axeuclidlem  29586  axcontlem2  29589  axcontlem4  29591  axcontlem7  29594  axcontlem8  29595  elntg2  29609  nrt2irr  31120  nvm1  31313  nvpi  31315  nvz0  31316  nvmtri  31319  nvabs  31320  nvge0  31321  nv1  31323  smcnlem  31345  ipval2lem4  31354  ipval2  31355  4ipval2  31356  ipidsq  31358  dipcj  31362  dip0r  31365  ipz  31367  nmoub3i  31421  nmlno0lem  31441  nmblolbii  31447  blocnilem  31452  cncph  31467  ipasslem4  31482  ipasslem5  31483  ipblnfi  31503  minvecolem2  31523  minvecolem4  31528  minvecolem6  31530  minvecolem7  31531  htthlem  31565  normpyc  31794  hhph  31826  bcs2  31830  norm1  31897  norm1exi  31898  pjhthlem1  32039  eigvalcl  32609  eighmorth  32612  nmlnop0iALT  32643  nmbdoplbi  32672  nmcexi  32674  nmcoplbi  32676  nmbdfnlbi  32697  nmcfnlbi  32700  riesz4i  32711  cnlnadjlem2  32716  cnlnadjlem7  32721  nmopcoi  32743  nmopcoadji  32749  branmfn  32753  leopnmid  32786  opsqrlem1  32788  hst1h  32875  hstle  32878  hstoh  32880  sto2i  32885  stadd3i  32896  strlem1  32898  golem1  32919  stcltrlem1  32924  cdj1i  33081  cdj3lem1  33082  cdj3lem3b  33088  cdj3i  33089  sgnval2  33413  re0cj  33421  receqid  33422  pythagreim  33423  lt2addrd  33428  le2halvesd  33434  fzsplit3  33471  bcm1n  33473  expgt0b  33494  fsumiunle  33506  nexple  33510  expevenpos  33512  oexpled  33513  wrdt2ind  33602  psgnfzto1stlem  33750  ccfldsrarelvec  34407  ccfldextdgrr  34408  constrrtll  34467  constrrtlc1  34468  constrrtlc2  34469  constrconj  34481  nn0constr  34497  constrnegcl  34499  constrdircl  34501  iconstr  34502  constrremulcl  34503  constrrecl  34505  constrimcl  34506  constrmulcl  34507  constrreinvcl  34508  constrinvcl  34509  constrresqrtcl  34513  constrabscl  34514  constrsqrtcl  34515  cos9thpiminplylem1  34518  sqsscirc1  34644  sqsscirc2  34645  cnre2csqima  34647  rmulccn  34664  xrge0iifcnv  34669  xrge0iifhom  34673  zrhnm  34703  rezh  34705  esumpcvgval  34814  esumcvgsum  34824  dya2ub  35006  dya2icoseg  35013  eulerpartlemgc  35098  ballotlemsi  35251  signsply0  35284  signsvtp  35316  signsvtn  35317  signsvfpn  35318  signsvfnn  35319  divsqrtid  35327  reprgt  35354  reprinfz1  35355  breprexplemc  35365  circlemethhgt  35376  hgt750lemd  35381  hgt750lemf  35386  hgt750lemg  35387  hgt750lemb  35389  hgt750lema  35390  hgt750leme  35391  tgoldbachgtde  35393  subfacval2  36153  subfaclim  36154  subfacval3  36155  resconn  36212  sinccvglem  36638  circum  36640  climlec3  36707  faclimlem1  36716  faclimlem2  36717  faclimlem3  36718  faclim  36719  iprodfac  36720  faclim2  36721  dnicld1  37546  dnizeq0  37549  dnizphlfeqhlf  37550  dnibndlem2  37553  dnibndlem3  37554  dnibndlem5  37556  dnibndlem6  37557  dnibndlem7  37558  dnibndlem8  37559  dnibndlem9  37560  dnibndlem10  37561  dnibndlem11  37562  dnibndlem12  37563  dnibndlem13  37564  dnibnd  37565  dnicn  37566  knoppcnlem4  37570  knoppcnlem5  37571  knoppcnlem6  37572  knoppcnlem8  37574  knoppcnlem9  37575  knoppcnlem10  37576  knoppcnlem11  37577  unblimceq0  37581  unbdqndv2lem1  37583  unbdqndv2lem2  37584  knoppndvlem1  37586  knoppndvlem6  37591  knoppndvlem8  37593  knoppndvlem9  37594  knoppndvlem10  37595  knoppndvlem11  37596  knoppndvlem12  37597  knoppndvlem14  37599  knoppndvlem15  37600  knoppndvlem17  37602  knoppndvlem18  37603  knoppndvlem19  37604  knoppndvlem20  37605  knoppndvlem21  37606  irrdifflemf  38507  irrdiff  38508  qdiff  38509  ltflcei  38792  sin2h  38794  cos2h  38795  tan2h  38796  poimirlem29  38828  opnmbllem0  38835  mblfinlem2  38837  mblfinlem3  38838  mblfinlem4  38839  mbfposadd  38846  itg2addnclem  38850  itg2addnclem2  38851  itg2addnclem3  38852  itg2addnc  38853  itg2gt0cn  38854  ibladdnc  38856  itgaddnclem2  38858  iblabsnclem  38862  iblabsnc  38863  iblmulc2nc  38864  itgmulc2nclem2  38866  itgmulc2nc  38867  itgabsnc  38868  ftc1cnnclem  38870  ftc1cnnc  38871  ftc1anclem1  38872  ftc1anclem2  38873  ftc1anclem3  38874  ftc1anclem4  38875  ftc1anclem5  38876  ftc1anclem6  38877  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  areacirclem1  38887  areacirclem5  38891  areacirc  38892  mettrifi  38950  lmclim2  38951  geomcau  38952  isbnd3  38977  ssbnd  38981  cntotbnd  38989  bfplem1  39015  bfplem2  39016  bfp  39017  rrnmet  39022  rrndstprj1  39023  rrndstprj2  39024  rrncmslem  39025  rrnequiv  39028  rrntotbnd  39029  ismrer1  39031  lcmineqlem18  43355  lcmineqlem19  43356  lcmineqlem20  43357  lcmineqlem21  43358  lcmineqlem22  43359  3lexlogpow5ineq2  43364  3lexlogpow2ineq1  43367  3lexlogpow2ineq2  43368  3lexlogpow5ineq5  43369  dvrelogpow2b  43377  aks4d1p1p2  43379  aks4d1p1p4  43380  dvle2  43381  aks4d1p1p6  43382  aks4d1p1p7  43383  aks4d1p1p5  43384  aks4d1p1  43385  aks4d1p3  43387  aks4d1p5  43389  aks4d1p6  43390  aks4d1p7d1  43391  aks4d1p7  43392  aks4d1p8d2  43394  aks4d1p8  43396  posbezout  43409  aks6d1c1  43425  hashscontpow1  43430  aks6d1c3  43432  aks6d1c4  43433  aks6d1c2lem4  43436  aks6d1c2  43439  aks6d1c5lem3  43446  aks6d1c5lem2  43447  2np3bcnp1  43453  sticksstones6  43460  sticksstones10  43464  sticksstones12a  43466  sticksstones12  43467  aks6d1c6lem4  43482  bcled  43487  bcle2d  43488  aks6d1c7lem1  43489  aks6d1c7lem2  43490  remulcan2d  43567  readdridaddlidd  43568  readdrcl2d  43592  sumcubes  43630  oexpreposd  43639  expeqidd  43642  rxp112d  43656  rxp11d  43659  readvrec2  43672  readvrec  43673  resuppsinopn  43674  readvcot  43675  resubeulem1  43686  resubeulem2  43687  readdsub  43695  resubsub4  43700  resubidaddlidlem  43705  resubdi  43707  sn-addlid  43715  remul02  43716  remul01  43718  renegneg  43723  readdcan2  43724  renegid2  43725  sn-it0e0  43727  sn-negex12  43728  reixi  43734  remulinvcom  43744  remullid  43745  remulcand  43750  rediveud  43754  redivrec2d  43771  rediv23d  43772  redivdird  43773  sn-0tie0  43775  zaddcomlem  43787  zaddcom  43788  renegmulnnass  43789  mulgt0b1d  43796  mulgt0b2d  43802  mullt0b1d  43807  sn-itrere  43812  sn-retire  43813  cnreeu  43814  frlmvscadiccat  43833  abvexp  43856  dffltz  43930  fltnltalem  43933  fltnlta  43934  negexpidd  43952  3cubeslem1  43954  3cubeslem2  43955  3cubeslem4  43959  eldioph2lem1  44031  lzenom  44041  rencldnfilem  44087  irrapxlem1  44089  irrapxlem2  44090  irrapxlem3  44091  irrapxlem4  44092  irrapxlem5  44093  pellexlem2  44097  pellexlem6  44101  pell1234qrreccl  44121  pell14qrgt0  44126  pell14qrdivcl  44132  pell14qrexpclnn0  44133  pell14qrexpcl  44134  pell14qrdich  44136  pell1qrgaplem  44140  pellfundex  44153  reglogmul  44160  reglogexp  44161  reglogbas  44162  reglog1  44163  pellfund14  44165  rmspecfund  44176  monotoddzzfi  44209  jm2.24nn  44226  jm2.17a  44227  jm2.17b  44228  jm2.17c  44229  jm2.24  44230  acongrep  44247  fzmaxdif  44248  acongeq  44250  modabsdifz  44253  jm2.19lem4  44259  jm2.19  44260  jm2.26lem3  44268  jm3.1lem1  44284  jm3.1lem2  44285  areaquad  44473  sqrtcvallem4  44894  sqrtcval  44896  sqrtcval2  44897  absmulrposd  45414  extoimad  45419  imo72b2lem0  45420  imo72b2lem1  45424  imo72b2  45427  int-addcomd  45428  int-addassocd  45429  int-addsimpd  45430  int-mulcomd  45431  int-mulassocd  45432  int-mulsimpd  45433  int-leftdistd  45434  int-rightdistd  45435  int-sqdefd  45436  int-mul11d  45437  int-mul12d  45438  int-add01d  45439  int-add02d  45440  int-sqgeq0d  45441  int-eqmvtd  45444  cvgdvgrat  45552  radcnvrat  45553  hashnzfzclim  45561  dvconstbi  45573  binomcxplemnn0  45588  binomcxplemnotnn0  45595  isosctrlem1ALT  46170  sineq0ALT  46173  infnsuprnmpt  46529  oddfl  46561  dstregt0  46565  zltlesub  46568  lt3addmuld  46584  fperiodmullem  46586  fperiodmul  46587  lt4addmuld  46589  fzdifsuc2  46593  supxrgere  46612  supxrgelem  46616  suplesup  46618  supsubc  46632  xralrple2  46633  abslt2sqd  46639  xralrple3  46652  reclt0d  46665  ltmulneg  46670  rexabslelem  46695  supminfrnmpt  46722  leneg2d  46725  leneg3d  46734  supminfxr  46741  absimnre  46753  absimlere  46756  iooabslt  46778  iccshift  46797  iooshift  46801  sqrlearg  46832  fmul01  46859  fmul01lt1lem1  46863  fmul01lt1lem2  46864  fprodabs2  46874  climinf  46885  limcrecl  46908  lptre2pt  46917  limcleqr  46921  0ellimcdiv  46926  limclner  46928  climleltrp  46953  climinf2mpt  46991  climinf3  46993  climxrre  47027  climliminflimsupd  47078  liminfltlem  47081  liminflimsupclim  47084  cnrefiisplem  47106  sinaover2ne0  47145  cncfperiod  47156  ioccncflimc  47162  cncficcgt0  47165  icocncflimc  47166  cncfshiftioo  47169  cncfiooicc  47171  fperdvper  47196  dvbdfbdioolem1  47205  dvbdfbdioolem2  47206  dvbdfbdioo  47207  ioodvbdlimc1lem1  47208  ioodvbdlimc1lem2  47209  ioodvbdlimc1  47210  ioodvbdlimc2lem  47211  ioodvbdlimc2  47212  dvnmul  47220  dvnprodlem1  47223  dvnprodlem2  47224  itgcoscmulx  47246  volioc  47249  itgsincmulx  47251  itgiccshift  47257  itgperiod  47258  itgsbtaddcnst  47259  volico  47260  voliooico  47269  voliccico  47276  stoweidlem7  47284  stoweidlem11  47288  stoweidlem13  47290  stoweidlem17  47294  stoweidlem19  47296  stoweidlem20  47297  stoweidlem21  47298  stoweidlem22  47299  stoweidlem23  47300  stoweidlem24  47301  stoweidlem26  47303  stoweidlem32  47309  stoweidlem36  47313  stoweidlem44  47321  stoweidlem47  47324  wallispilem3  47344  wallispi2lem1  47348  stirlinglem1  47351  stirlinglem5  47355  stirlinglem11  47361  stirlinglem12  47362  stirlinglem14  47364  dirkerval2  47371  dirkerre  47372  dirkertrigeqlem2  47376  dirkertrigeq  47378  dirkeritg  47379  dirkercncflem1  47380  dirkercncflem2  47381  dirkercncflem4  47383  fourierdlem4  47388  fourierdlem6  47390  fourierdlem7  47391  fourierdlem13  47397  fourierdlem14  47398  fourierdlem16  47400  fourierdlem18  47402  fourierdlem19  47403  fourierdlem21  47405  fourierdlem22  47406  fourierdlem24  47408  fourierdlem26  47410  fourierdlem28  47412  fourierdlem30  47414  fourierdlem35  47419  fourierdlem39  47423  fourierdlem40  47424  fourierdlem41  47425  fourierdlem42  47426  fourierdlem43  47427  fourierdlem44  47428  fourierdlem47  47430  fourierdlem48  47431  fourierdlem49  47432  fourierdlem50  47433  fourierdlem51  47434  fourierdlem53  47436  fourierdlem56  47439  fourierdlem57  47440  fourierdlem58  47441  fourierdlem59  47442  fourierdlem60  47443  fourierdlem61  47444  fourierdlem62  47445  fourierdlem63  47446  fourierdlem64  47447  fourierdlem65  47448  fourierdlem66  47449  fourierdlem68  47451  fourierdlem70  47453  fourierdlem71  47454  fourierdlem72  47455  fourierdlem73  47456  fourierdlem74  47457  fourierdlem75  47458  fourierdlem76  47459  fourierdlem77  47460  fourierdlem78  47461  fourierdlem79  47462  fourierdlem80  47463  fourierdlem81  47464  fourierdlem83  47466  fourierdlem84  47467  fourierdlem85  47468  fourierdlem87  47470  fourierdlem88  47471  fourierdlem89  47472  fourierdlem90  47473  fourierdlem91  47474  fourierdlem92  47475  fourierdlem93  47476  fourierdlem95  47478  fourierdlem97  47480  fourierdlem101  47484  fourierdlem103  47486  fourierdlem104  47487  fourierdlem107  47490  fourierdlem109  47492  fourierdlem111  47494  fourierdlem112  47495  fouriercnp  47503  sqwvfoura  47505  sqwvfourb  47506  fouriersw  47508  etransclem14  47525  etransclem18  47529  etransclem23  47534  etransclem24  47535  etransclem27  47538  etransclem46  47557  etransclem48  47559  qndenserrnbllem  47571  ioorrnopnlem  47581  sge0tsms  47657  sge0cl  47658  sge0split  47686  sge0iunmptlemfi  47690  sge0rpcpnf  47698  sge0isum  47704  sge0ad2en  47708  sge0xaddlem1  47710  sge0xaddlem2  47711  sge0gtfsumgt  47720  sge0seq  47723  meadif  47756  meaiininclem  47763  carageniuncllem1  47798  carageniuncllem2  47799  hoicvr  47825  hoicvrrex  47833  ovnsubaddlem1  47847  hsphoidmvle2  47862  hsphoidmvle  47863  hoidmvval0  47864  hoiprodp1  47865  hoidmv1lelem1  47868  hoidmv1lelem2  47869  hoidmv1le  47871  hoidmvlelem1  47872  hoidmvlelem2  47873  hoidmvlelem3  47874  hoiqssbllem2  47900  hspmbllem1  47903  ovolval2lem  47920  ovolval3  47924  ovolval5lem1  47929  ovnovollem1  47933  ovnovollem2  47934  vonioolem1  47957  vonioo  47959  vonicclem1  47960  vonicc  47962  smfaddlem1  48040  smflimlem4  48051  smfmullem1  48068  smfmullem2  48069  smfmullem3  48070  smfdiv  48074  smfneg  48080  sigaras  48132  sigarms  48133  sigarls  48134  sigarexp  48136  sigarperm  48137  sigarimcd  48139  sigarcol  48141  sharhght  48142  cevathlem2  48145  readdcnnred  48640  resubcnnred  48641  cndivrenred  48643  flmrecm1  48680  fldivmod  48681  ceildivmod  48682  m1mod0mod1  48697  m1modmmod  48701  difmodm1lt  48702  requad01  48986  requad1  48987  requad2  48988  fpprwppr  49104  bgoldbtbndlem2  49171  gpgvtxedg1  49429  ltsubaddb  49951  ltsubsubb  49952  ltsubadd2b  49953  flsubz  49959  logblt1b  50001  dignn0fr  50038  dignn0flhalflem1  50052  dignn0flhalflem2  50053  nn0sumshdiglemA  50056  affinecomb1  50139  affinecomb2  50140  resum2sqorgt0  50146  rrx2pnedifcoorneor  50154  rrx2pnedifcoorneorr  50155  ehl2eudisval0  50163  eenglngeehlnmlem1  50175  eenglngeehlnmlem2  50176  rrx2vlinest  50178  rrx2linest  50179  rrx2linest2  50181  2sphere0  50187  line2ylem  50188  line2  50189  line2xlem  50190  line2x  50191  line2y  50192  itscnhlc0yqe  50196  itschlc0yqe  50197  itsclc0yqsol  50201  itscnhlc0xyqsol  50202  itschlc0xyqsol1  50203  itschlc0xyqsol  50204  itsclc0xyqsolr  50206  itsclinecirc0b  50211  itsclquadb  50213  itsclquadeu  50214  2itscplem1  50215  2itscplem2  50216  2itscplem3  50217  2itscp  50218  itscnhlinecirc02plem1  50219  itscnhlinecirc02plem2  50220  itscnhlinecirc02p  50222  inlinecirc02plem  50223  inlinecirc02p  50224  crosspdotsumlem  51386  crosspdotd  51387  crosspaltd  51388  crossp3d  51389  veronesev1lem  51395  veronesev2lem  51396  veronesev3lem  51397  veronesev4lem  51398  veronesev5lem  51399  veronesev6lem  51400  veroquadgsumlem  51405  amgmwlem  51409  amgmlemALT  51410