Theorem recnd 11330

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11191  ℝcr 11192

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-resscn 11250

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

This theorem is used by:  00id  11478  mul02lem1  11479  addrid  11483  cnegex  11484  ltadd1  11776  leadd2  11778  ltsubadd  11779  ltsubadd2  11780  lesubadd  11781  lesubadd2  11782  lesub1  11803  lesub2  11804  ltnegcon1  11810  ltnegcon2  11811  add20  11821  subge0  11822  suble0  11823  lesub0  11826  mulge0  11827  eqord2  11840  lesub3d  11927  possumd  11934  sublt0d  11935  rereccl  12028  redivcl  12029  recgt0  12156  prodgt0  12157  ltmul1a  12159  ltdiv1  12174  ltmuldiv  12183  ltrec  12192  recp1lt1  12208  recreclt  12209  ledivp1  12212  supadd  12278  infrenegsup  12293  rimul  12304  cru  12305  avglt1  12577  avglt2  12578  lt2addmuld  12589  div4p1lem1div2  12594  nn0cnd  12662  zcn  12691  zeo  12778  zcnd  12797  eluzmn  12965  eluzelcn  12970  cnref1o  13106  rpcn  13124  rpcnd  13159  ltaddrp2d  13191  mul2lt0rlt0  13217  mul2lt0rgt0  13218  mul2lt0llt0  13219  mul2lt0lgt0  13220  mul2lt0bi  13221  prodge0rd  13222  prodge0ld  13223  qbtwnre  13322  xralrple  13328  xpncan  13374  xmulcom  13389  xmulneg1  13392  xlemul1  13413  elunitcn  13592  icoshftf1o  13598  lincmb01cmp  13619  iccf1o  13620  divfl0  13957  fladdz  13958  flzadd  13959  flhalf  13963  ceim1l  13980  intfracq  13992  fldiv  13993  modvalr  14005  flpmodeq  14007  mod0  14009  modlt  14013  moddiffl  14015  modfrac  14017  flmod  14018  intfrac  14019  modmulnn  14022  modvalp1  14023  modid  14029  modcyc  14039  modadd1  14041  modaddb  14042  modaddabs  14044  modmuladdnn0  14051  negmod  14052  modadd2mod  14057  modnegd  14062  modadd12d  14063  modsub12d  14064  modmulmodr  14073  modaddmulmod  14074  moddi  14075  modsubdir  14076  modeqmodmin  14077  modirr  14078  addmodlteq  14082  seqf1olem1  14177  serle  14193  expcl2lem  14209  expnegz  14232  expaddzlem  14241  expaddz  14242  expmulz  14244  sq11  14267  ltexp2a  14302  expmordi  14303  leexp2a  14308  leexp2r  14310  exple1  14313  expubnd  14314  bernneq2  14367  expmulnbnd  14372  discr1  14376  discr  14377  faclbnd  14427  bcp1nk  14454  cshweqrep  14965  sgnsub  15252  sgnmul  15253  remim  15277  reim0b  15279  rereb  15280  mulre  15281  cjreb  15283  recj  15284  reneg  15285  readd  15286  resub  15287  remullem  15288  remul2  15290  rediv  15291  imcj  15292  imneg  15293  imadd  15294  imsub  15295  immul2  15297  imdiv  15298  cjcj  15300  cjadd  15301  ipcnval  15303  cjmulval  15305  cjneg  15307  imval2  15311  cjreim2  15321  01sqrexlem5  15406  01sqrexlem7  15408  resqrtthlem  15414  remsqsqrt  15416  sqrtmul  15419  sqrtdiv  15425  sqrtneg  15427  sqrtmsq  15430  absdiv  15455  absid  15456  absexp  15464  absexpz  15465  absimle  15469  abslt  15475  absle  15476  abssubne0  15477  releabs  15482  recval  15483  abstri  15491  abs2difabs  15495  abs1m  15496  abslem2  15500  absrdbnd  15502  sqreulem  15520  sqreu  15521  amgm2  15530  icodiamlt  15598  bhmafibid1  15628  bhmafibid2  15629  lo1bddrp  15685  o1lo1  15697  rlimrecl  15740  rlimge0  15741  climrecl  15743  climge0  15744  climabs0  15745  reccn2  15757  o1rlimmul  15779  lo1mul2  15789  lo1sub  15791  climle  15800  climsqz  15801  climsqz2  15802  rlimsqz  15810  rlimsqz2  15811  climlec2  15819  isercolllem1  15825  climsup  15830  caucvgrlem  15833  caurcvgr  15834  caucvgrlem2  15835  iseraltlem1  15842  iseraltlem2  15843  iseraltlem3  15844  iseralt  15845  isumrecl  15924  isumge0  15925  fsumless  15956  fsumge1  15957  fsum00  15958  fsumle  15959  fsumlt  15960  fsumabs  15961  o1fsum  15973  seqabs  15974  cvgcmp  15976  cvgcmpce  15978  abscvgcvg  15979  indsum  15988  indsumhash  15989  isumrpcl  16005  isumle  16006  isumless  16007  isumsup  16009  climcndslem1  16011  climcndslem2  16012  climcnds  16013  flo1  16016  supcvg  16018  trireciplem  16024  trirecip  16025  explecnv  16027  geo2sum  16035  geo2lim  16037  geomulcvg  16038  cvgrat  16045  mertenslem1  16046  mertenslem2  16047  fprodabs  16134  fprodle  16156  iprodrecl  16162  bpolydiflem  16213  bpoly4  16218  efcllem  16236  ege2le3  16249  efaddlem  16252  efgt0  16264  eftlub  16270  effsumlt  16272  eflt  16278  eflegeo  16282  resin4p  16299  recos4p  16300  retanhcl  16320  tanhlt1  16321  efeul  16323  ef01bndlem  16345  sin01bnd  16346  cos01bnd  16347  sin01gt0  16351  cos01gt0  16352  sin02gt0  16353  absefi  16357  absef  16358  absefib  16359  efieq1re  16360  eirrlem  16365  rpnnen2lem5  16379  rpnnen2lem8  16382  rpnnen2lem9  16383  rpnnen2lem11  16385  rpnnen2lem12  16386  moddvds  16426  odd2np1  16504  divalglem5  16560  bitsp1o  16596  bitsfzo  16598  bitscmp  16601  sadcaddlem  16620  nn0seqcvgd  16738  sqnprm  16871  isprm5  16876  nonsq  16928  eulerthlem2  16952  prmdiveq  16956  odzdvds  16966  vfermltlALT  16973  pythagtriplem14  16999  pcid  17044  fldivp1  17068  pcfac  17070  pockthlem  17076  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  prmrec  17093  4sqlem5  17113  4sqlem10  17118  mul4sqlem  17124  4sqlem15  17130  4sqlem16  17131  mulgneg  19295  ghmmulg  19435  odmodnn0  19747  mndodconglem  19748  pgpfaclem2  20291  isabvd  21062  abv1z  21074  abvneg  21076  abvrec  21078  abvdiv  21079  abvdom  21080  rege0subm  21722  cnsubrg  21726  gzrngunitlem  21731  regsumfsum  21734  prmirredlem  21771  remulg  21906  rzgrp  21922  bl2in  24712  blhalf  24717  blssps  24736  blss  24737  methaus  24832  nrmmetd  24886  nm2dif  24937  nminvr  24981  nmdvr  24982  nlmmul0or  24995  nrginvrcnlem  25003  nmolb2d  25030  nmoi2  25042  nmoleub  25043  nmo0  25047  nmoeq0  25048  nmoco  25049  nmotri  25051  nmoid  25054  blcvx  25110  xrsxmet  25122  recld2  25127  reconnlem2  25140  opnreen  25144  metdstri  25164  metnrmlem3  25174  icchmeo  25255  icopnfcnv  25256  icopnfhmeo  25257  iccpnfhmeo  25259  xrhmeo  25260  icccvx  25264  cnheiborlem  25268  evth  25273  lebnumii  25280  pcoass  25338  pcorevlem  25340  pcorev2  25342  pi1xfrcnv  25371  nmoleub2lem  25428  nmoleub2lem3  25429  nmoleub3  25433  ncvsm1  25468  ncvspi  25470  ncvs1  25471  cphsqrtcl2  25500  ipcau2  25548  tcphcphlem1  25549  tcphcphlem2  25550  tcphcph  25551  cphipval2  25555  cphipval  25557  iscau3  25592  rrxnm  25705  rrxcph  25706  csbren  25713  trirn  25714  rrxmval  25719  rrxmetlem  25721  rrxmet  25722  rrxdstprj1  25723  ehl1eudis  25734  ehl2eudis  25736  minveclem2  25740  minveclem3b  25742  minveclem4  25746  minveclem6  25748  minveclem7  25749  pjthlem1  25751  ivthlem2  25766  ivthlem3  25767  ivth2  25769  ovolfsval  25784  ovollb2lem  25802  ovolctb  25804  ovolunlem1a  25810  ovolunnul  25814  ovolfiniun  25815  ovoliunlem1  25816  ovoliun2  25820  shft2rab  25822  ovolshftlem1  25823  sca2rab  25826  ovolscalem1  25827  ovolsca  25829  ovolicc1  25830  ovolicc2lem4  25834  ovolicopnf  25838  cmmbl  25848  nulmbl  25849  nulmbl2  25850  unmbl  25851  volinun  25860  volfiniun  25861  voliunlem1  25864  voliunlem3  25866  ioombl1lem3  25874  ioombl1lem4  25875  ovolioo  25882  ioorcl2  25886  uniioovol  25893  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  uniioombllem6  25902  dyadovol  25907  dyaddisjlem  25909  opnmbllem  25915  vitalilem1  25922  vitalilem2  25923  vitalilem3  25924  vitalilem4  25925  ismbf  25942  mbfmulc2lem  25961  mbfmulc2re  25962  mbfmulc2  25977  mbfinf  25979  itg1val2  25998  itg11  26005  i1fmullem  26008  i1fadd  26009  itg1addlem4  26013  itg1addlem5  26014  i1fmulclem  26016  i1fmulc  26017  itg1mulc  26018  itg1sub  26023  itg10a  26024  itg1ge0a  26025  itg1climres  26028  mbfi1fseqlem3  26031  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  mbfi1flimlem  26036  mbfmullem2  26038  itg2const  26054  itg2const2  26055  itg2mulclem  26060  itg2mulc  26061  itg2splitlem  26062  itg2split  26063  itg2monolem1  26064  itg2monolem3  26066  itg2addlem  26072  itgcl  26097  itgcnlem  26103  itgrevallem1  26108  itgposval  26109  iblneg  26116  itgneg  26117  i1fibl  26121  itgitg1  26122  itgconst  26132  ibladd  26134  itgaddlem2  26137  iblabslem  26141  iblabs  26142  iblabsr  26143  iblmulc2  26144  itgmulc2lem2  26146  itgmulc2  26147  itgabs  26148  itgsplit  26149  bddmulibl  26152  bddiblnc  26155  dvcjbr  26262  dvfre  26264  dvexp3  26291  dveflem  26292  dvferm1lem  26297  dvferm2lem  26299  rolle  26303  cmvth  26304  mvth  26305  dvlip  26306  dvlipcn  26307  c1liplem1  26309  c1lip1  26310  dveq0  26313  dv11cn  26314  dvlt0  26318  dvle  26320  dvivthlem1  26321  dvivth  26323  lhop1lem  26326  lhop1  26327  lhop2  26328  lhop  26329  dvcvx  26333  dvfsumle  26334  dvfsumge  26335  dvfsumabs  26336  dvfsumlem1  26339  dvfsumlem2  26340  dvfsumlem4  26342  dvfsumrlimge0  26343  dvfsumrlim2  26345  dvfsum2  26347  ftc1a  26350  ftc1lem4  26352  ftc1lem5  26353  itgpowd  26363  plyeq0lem  26522  coemulhi  26566  plyrecj  26591  plyn0mulidp  26595  plydivlem3  26609  aalioulem2  26653  aalioulem3  26654  aalioulem4  26655  aalioulem5  26656  aalioulem6  26657  aaliou  26658  aaliou2  26660  aaliou2b  26661  aaliou3lem3  26664  aaliou3lem7  26669  aaliou3lem9  26670  taylthlem2  26694  ulmcn  26719  ulmdvlem1  26720  mtest  26724  mtestbdd  26725  itgulm  26728  radcnvlem1  26733  radcnvlem2  26734  radcnvlt1  26738  radcnvle  26740  dvradcnv  26741  pserulm  26742  abelthlem2  26752  abelthlem5  26755  abelthlem7  26758  abelth2  26762  reeff1olem  26766  efcvx  26769  pilem2  26772  pilem3  26773  sincosq2sgn  26821  sincosq3sgn  26822  sincosq4sgn  26823  coseq0negpitopi  26825  tanrpcl  26826  tangtx  26827  tanabsge  26828  sinq12gt0  26829  sinq34lt0t  26831  cosq14gt0  26832  cosq14ge0  26833  pige3ALT  26841  coskpi  26844  cos02pilt1  26847  cosordlem  26851  sinord  26855  tanord1  26858  tanord  26859  tanregt0  26860  efif1olem2  26864  efif1olem4  26866  eff1olem  26869  logrnaddcl  26895  logneg  26909  lognegb  26911  reexplog  26916  relogexp  26917  logfac  26922  efiarg  26928  cosargd  26929  cosarg0d  26930  argregt0  26931  argrege0  26932  argimgt0  26933  logneg2  26936  logmul2  26937  logdiv2  26938  abslogle  26939  tanarg  26940  logdivlti  26941  divlogrlim  26956  logcnlem2  26964  logcnlem3  26965  logcnlem4  26966  logcn  26968  logf1o2  26971  advlog  26975  advlogexp  26976  efopnlem1  26977  logtayllem  26980  logtayl  26981  logccv  26984  logcxp  26990  mulcxp  27006  divcxp  27008  cxpmul  27009  cxproot  27011  cxpmul2z  27012  abscxp  27013  abscxp2  27014  cxplt  27015  cxplea  27017  cxple2  27018  cxple2a  27020  cxplt3  27021  cxpsqrtlem  27023  cxpsqrt  27024  logsqrt  27025  dvcxp2  27062  cxpcn3lem  27068  resqrtcn  27070  cxpaddlelem  27072  cxpaddle  27073  abscxpbnd  27074  root1id  27075  root1eq1  27076  root1cj  27077  cxpeq  27078  loglesqrt  27082  relogbmul  27098  nnlogbexp  27102  logbrec  27103  cosangneg2d  27128  angrtmuld  27129  ang180lem2  27131  lawcoslem1  27136  lawcos  27137  pythag  27138  isosctrlem1  27139  isosctrlem2  27140  isosctrlem3  27141  ssscongptld  27143  chordthmlem  27153  chordthmlem2  27154  chordthmlem3  27155  chordthmlem4  27156  chordthmlem5  27157  heron  27159  asinsinlem  27212  reasinsin  27217  acosrecl  27224  atancj  27231  atanrecl  27232  atanlogaddlem  27234  atanlogsublem  27236  atanbndlem  27246  atans2  27252  ressatans  27255  atantayl  27258  leibpilem2  27262  leibpi  27263  leibpisum  27264  log2tlbnd  27266  log2ublem2  27268  birthdaylem2  27273  birthdaylem3  27274  cxp2limlem  27296  cxp2lim  27297  cxploglim  27298  cxploglim2  27299  divsqrtsumo1  27304  cvxcl  27305  scvxcvx  27306  jensenlem2  27308  jensen  27309  amgmlem  27310  logdiflbnd  27315  emcllem2  27317  emcllem3  27318  emcllem5  27320  emcllem6  27321  emcllem7  27322  harmonicbnd4  27331  fsumharmonic  27332  zetacvg  27335  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem4  27352  lgamgulmlem5  27353  lgamgulmlem6  27354  lgamgulm2  27356  lgambdd  27357  lgamcvg2  27375  gamcvg  27376  gamcvg2lem  27379  regamcl  27381  relgamcl  27382  lgam1  27384  ftalem1  27393  ftalem2  27394  ftalem4  27396  ftalem5  27397  basellem3  27403  basellem4  27404  basellem5  27405  basellem6  27406  basellem7  27407  basellem8  27408  basellem9  27409  efnnfsumcl  27423  chtprm  27473  chpp1  27475  chtdif  27478  efchtdvds  27479  prmorcht  27498  mumullem2  27500  fsumfldivdiaglem  27509  ppiub  27524  chtleppi  27530  chtublem  27531  chtub  27532  pclogsum  27535  vmasum  27536  logfac2  27537  chpval2  27538  chpchtsum  27539  chpub  27540  logfaclbnd  27542  logfacbnd3  27543  logfacrlim  27544  logexprlim  27545  logfacrlim2  27546  mersenne  27547  dchrabs  27580  dchrptlem1  27584  dchrptlem2  27585  bcmax  27598  bcp1ctr  27599  bposlem1  27604  bposlem9  27612  lgsvalmod  27636  lgsdilem  27644  lgsne0  27655  lgsqrlem2  27667  gausslemma2dlem1a  27685  gausslemma2dlem6  27692  lgseisenlem1  27695  lgseisenlem2  27696  lgseisen  27699  lgsquadlem1  27700  lgsquadlem2  27701  mul2sq  27739  2sqlem3  27740  2sqlem8  27746  2sqmod  27756  2sqreulem1  27766  2sqreunnlem1  27769  chebbnd1lem1  27789  chebbnd1lem2  27790  chebbnd1lem3  27791  chtppilimlem1  27793  chtppilimlem2  27794  chtppilim  27795  chto1ub  27796  chto1lb  27798  chpchtlim  27799  chpo1ub  27800  vmadivsum  27802  vmadivsumb  27803  rplogsumlem1  27804  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlema  27808  dchrisumlem1  27809  dchrisumlem2  27810  dchrisumlem3  27811  dchrmusumlema  27813  dchrmusum2  27814  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasum2if  27817  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrvmasumiflem2  27822  dchrisum0flblem1  27828  dchrisum0fno1  27831  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lema  27834  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  dchrmusumlem  27842  dchrvmasumlem  27843  rpvmasum  27846  rplogsum  27847  dirith2  27848  mudivsum  27850  mulogsumlem  27851  mulogsum  27852  logdivsum  27853  mulog2sumlem1  27854  mulog2sumlem2  27855  mulog2sumlem3  27856  vmalogdivsum2  27858  vmalogdivsum  27859  2vmadivsumlem  27860  logsqvma  27862  logsqvma2  27863  log2sumbnd  27864  selberglem1  27865  selberglem2  27866  selberglem3  27867  selberg  27868  selbergb  27869  selberg2lem  27870  selberg2  27871  selberg2b  27872  chpdifbndlem1  27873  logdivbnd  27876  selberg3lem1  27877  selberg3lem2  27878  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrmax  27884  pntrsumo1  27885  pntrsumbnd  27886  pntrsumbnd2  27887  selbergr  27888  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntsval2  27896  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6a  27902  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntibndlem2  27911  pntibndlem3  27912  pntlemb  27917  pntlemg  27918  pntlemh  27919  pntlemn  27920  pntlemr  27922  pntlemj  27923  pntlemf  27925  pntlemk  27926  pntlemo  27927  pntlem3  27929  pntleml  27931  pnt2  27933  pnt  27934  abvcxp  27935  ostth2lem1  27938  qabvexp  27946  padicabv  27950  padicabvcxp  27952  ostth2lem2  27954  ostth2lem3  27955  ostth2lem4  27956  ostth2  27957  ostth3  27958  ttgcontlem1  29455  fveecn  29473  eqeelen  29475  brbtwn2  29476  colinearalglem4  29480  colinearalg  29481  axsegconlem9  29496  axsegconlem10  29497  ax5seglem1  29499  ax5seglem2  29500  ax5seglem3  29502  ax5seglem5  29504  ax5seglem6  29505  ax5seglem9  29508  ax5seg  29509  axbtwnid  29510  axpaschlem  29511  axpasch  29512  axeuclidlem  29533  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  axcontlem8  29542  elntg2  29556  nrt2irr  31067  nvm1  31260  nvpi  31262  nvz0  31263  nvmtri  31266  nvabs  31267  nvge0  31268  nv1  31270  smcnlem  31292  ipval2lem4  31301  ipval2  31302  4ipval2  31303  ipidsq  31305  dipcj  31309  dip0r  31312  ipz  31314  nmoub3i  31368  nmlno0lem  31388  nmblolbii  31394  blocnilem  31399  cncph  31414  ipasslem4  31429  ipasslem5  31430  ipblnfi  31450  minvecolem2  31470  minvecolem4  31475  minvecolem6  31477  minvecolem7  31478  htthlem  31512  normpyc  31741  hhph  31773  bcs2  31777  norm1  31844  norm1exi  31845  pjhthlem1  31986  eigvalcl  32556  eighmorth  32559  nmlnop0iALT  32590  nmbdoplbi  32619  nmcexi  32621  nmcoplbi  32623  nmbdfnlbi  32644  nmcfnlbi  32647  riesz4i  32658  cnlnadjlem2  32663  cnlnadjlem7  32668  nmopcoi  32690  nmopcoadji  32696  branmfn  32700  leopnmid  32733  opsqrlem1  32735  hst1h  32822  hstle  32825  hstoh  32827  sto2i  32832  stadd3i  32843  strlem1  32845  golem1  32866  stcltrlem1  32871  cdj1i  33028  cdj3lem1  33029  cdj3lem3b  33035  cdj3i  33036  sgnval2  33320  re0cj  33328  receqid  33329  pythagreim  33330  lt2addrd  33335  le2halvesd  33341  fzsplit3  33378  bcm1n  33380  expgt0b  33401  fsumiunle  33413  nexple  33417  expevenpos  33419  oexpled  33420  wrdt2ind  33509  psgnfzto1stlem  33654  ccfldsrarelvec  34296  ccfldextdgrr  34297  constrrtll  34356  constrrtlc1  34357  constrrtlc2  34358  constrconj  34370  nn0constr  34386  constrnegcl  34388  constrdircl  34390  iconstr  34391  constrremulcl  34392  constrrecl  34394  constrimcl  34395  constrmulcl  34396  constrreinvcl  34397  constrinvcl  34398  constrresqrtcl  34402  constrabscl  34403  constrsqrtcl  34404  cos9thpiminplylem1  34407  sqsscirc1  34533  sqsscirc2  34534  cnre2csqima  34536  rmulccn  34553  xrge0iifcnv  34558  xrge0iifhom  34562  zrhnm  34592  rezh  34594  esumpcvgval  34703  esumcvgsum  34713  dya2ub  34895  dya2icoseg  34902  omssubadd  34925  eulerpartlemgc  34987  ballotlemsi  35140  signsply0  35173  signsvtp  35205  signsvtn  35206  signsvfpn  35207  signsvfnn  35208  divsqrtid  35216  reprgt  35243  reprinfz1  35244  breprexplemc  35254  circlemethhgt  35265  hgt750lemd  35270  hgt750lemf  35275  hgt750lemg  35276  hgt750lemb  35278  hgt750lema  35279  hgt750leme  35280  tgoldbachgtde  35282  subfacval2  35931  subfaclim  35932  subfacval3  35933  resconn  35990  sinccvglem  36416  circum  36418  climlec3  36478  faclimlem1  36487  faclimlem2  36488  faclimlem3  36489  faclim  36490  iprodfac  36491  faclim2  36492  dnicld1  37318  dnizeq0  37321  dnizphlfeqhlf  37322  dnibndlem2  37325  dnibndlem3  37326  dnibndlem5  37328  dnibndlem6  37329  dnibndlem7  37330  dnibndlem8  37331  dnibndlem9  37332  dnibndlem10  37333  dnibndlem11  37334  dnibndlem12  37335  dnibndlem13  37336  dnibnd  37337  dnicn  37338  knoppcnlem4  37342  knoppcnlem5  37343  knoppcnlem6  37344  knoppcnlem8  37346  knoppcnlem9  37347  knoppcnlem10  37348  knoppcnlem11  37349  unblimceq0  37353  unbdqndv2lem1  37355  unbdqndv2lem2  37356  knoppndvlem1  37358  knoppndvlem6  37363  knoppndvlem8  37365  knoppndvlem9  37366  knoppndvlem10  37367  knoppndvlem11  37368  knoppndvlem12  37369  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem17  37374  knoppndvlem18  37375  knoppndvlem19  37376  knoppndvlem20  37377  knoppndvlem21  37378  irrdifflemf  38226  irrdiff  38227  qdiff  38228  ltflcei  38511  sin2h  38513  cos2h  38514  tan2h  38515  poimirlem29  38547  opnmbllem0  38554  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  mbfposadd  38565  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  ibladdnc  38575  itgaddnclem2  38577  iblabsnclem  38581  iblabsnc  38582  iblmulc2nc  38583  itgmulc2nclem2  38585  itgmulc2nc  38586  itgabsnc  38587  ftc1cnnclem  38589  ftc1cnnc  38590  ftc1anclem1  38591  ftc1anclem2  38592  ftc1anclem3  38593  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  areacirclem1  38606  areacirclem5  38610  areacirc  38611  mettrifi  38671  lmclim2  38672  geomcau  38673  isbnd3  38698  ssbnd  38702  cntotbnd  38710  bfplem1  38736  bfplem2  38737  bfp  38738  rrnmet  38743  rrndstprj1  38744  rrndstprj2  38745  rrncmslem  38746  rrnequiv  38749  rrntotbnd  38750  ismrer1  38752  lcmineqlem18  43076  lcmineqlem19  43077  lcmineqlem20  43078  lcmineqlem21  43079  lcmineqlem22  43080  3lexlogpow5ineq2  43085  3lexlogpow2ineq1  43088  3lexlogpow2ineq2  43089  3lexlogpow5ineq5  43090  dvrelogpow2b  43098  aks4d1p1p2  43100  aks4d1p1p4  43101  dvle2  43102  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p3  43108  aks4d1p5  43110  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8d2  43115  aks4d1p8  43117  posbezout  43130  aks6d1c1  43146  hashscontpow1  43151  aks6d1c3  43153  aks6d1c4  43154  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem3  43167  aks6d1c5lem2  43168  2np3bcnp1  43174  sticksstones6  43181  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem4  43203  bcled  43208  bcle2d  43209  aks6d1c7lem1  43210  aks6d1c7lem2  43211  remulcan2d  43287  readdridaddlidd  43288  readdrcl2d  43312  sumcubes  43350  oexpreposd  43359  expeqidd  43362  rxp112d  43376  rxp11d  43379  readvrec2  43392  readvrec  43393  resuppsinopn  43394  readvcot  43395  resubeulem1  43406  resubeulem2  43407  readdsub  43415  resubsub4  43420  resubidaddlidlem  43425  resubdi  43427  sn-addlid  43435  remul02  43436  remul01  43438  renegneg  43443  readdcan2  43444  renegid2  43445  sn-it0e0  43447  sn-negex12  43448  reixi  43454  remulinvcom  43464  remullid  43465  remulcand  43470  rediveud  43474  redivrec2d  43491  rediv23d  43492  redivdird  43493  sn-0tie0  43495  zaddcomlem  43507  zaddcom  43508  renegmulnnass  43509  mulgt0b1d  43516  mulgt0b2d  43522  mullt0b1d  43527  sn-itrere  43532  sn-retire  43533  cnreeu  43534  frlmvscadiccat  43553  abvexp  43576  dffltz  43650  fltnltalem  43653  fltnlta  43654  negexpidd  43672  3cubeslem1  43674  3cubeslem2  43675  3cubeslem4  43679  eldioph2lem1  43750  lzenom  43760  rencldnfilem  43806  irrapxlem1  43808  irrapxlem2  43809  irrapxlem3  43810  irrapxlem4  43811  irrapxlem5  43812  pellexlem2  43816  pellexlem6  43820  pell1234qrreccl  43840  pell14qrgt0  43845  pell14qrdivcl  43851  pell14qrexpclnn0  43852  pell14qrexpcl  43853  pell14qrdich  43855  pell1qrgaplem  43859  pellfundex  43872  reglogmul  43879  reglogexp  43880  reglogbas  43881  reglog1  43882  pellfund14  43884  rmspecfund  43895  monotoddzzfi  43928  jm2.24nn  43945  jm2.17a  43946  jm2.17b  43947  jm2.17c  43948  jm2.24  43949  acongrep  43966  fzmaxdif  43967  acongeq  43969  modabsdifz  43972  jm2.19lem4  43978  jm2.19  43979  jm2.26lem3  43987  jm3.1lem1  44003  jm3.1lem2  44004  areaquad  44202  sqrtcvallem4  44624  sqrtcval  44626  sqrtcval2  44627  absmulrposd  45144  extoimad  45149  imo72b2lem0  45150  imo72b2lem1  45154  imo72b2  45157  int-addcomd  45158  int-addassocd  45159  int-addsimpd  45160  int-mulcomd  45161  int-mulassocd  45162  int-mulsimpd  45163  int-leftdistd  45164  int-rightdistd  45165  int-sqdefd  45166  int-mul11d  45167  int-mul12d  45168  int-add01d  45169  int-add02d  45170  int-sqgeq0d  45171  int-eqmvtd  45174  cvgdvgrat  45282  radcnvrat  45283  hashnzfzclim  45291  dvconstbi  45303  binomcxplemnn0  45318  binomcxplemnotnn0  45325  isosctrlem1ALT  45901  sineq0ALT  45904  infnsuprnmpt  46231  oddfl  46263  dstregt0  46267  zltlesub  46270  lt3addmuld  46286  fperiodmullem  46288  fperiodmul  46289  lt4addmuld  46291  fzdifsuc2  46295  supxrgere  46314  supxrgelem  46318  suplesup  46320  supsubc  46334  xralrple2  46335  abslt2sqd  46341  xralrple3  46354  reclt0d  46367  ltmulneg  46372  rexabslelem  46397  supminfrnmpt  46424  leneg2d  46427  leneg3d  46436  supminfxr  46443  absimnre  46455  absimlere  46458  iooabslt  46480  iccshift  46499  iooshift  46503  sqrlearg  46534  fmul01  46561  fmul01lt1lem1  46565  fmul01lt1lem2  46566  fprodabs2  46576  climinf  46587  limcrecl  46610  lptre2pt  46619  limcleqr  46623  0ellimcdiv  46628  limclner  46630  climleltrp  46655  climinf2mpt  46693  climinf3  46695  climxrre  46729  climliminflimsupd  46780  liminfltlem  46783  liminflimsupclim  46786  cnrefiisplem  46808  sinaover2ne0  46847  cncfperiod  46858  ioccncflimc  46864  cncficcgt0  46867  icocncflimc  46868  cncfshiftioo  46871  cncfiooicc  46873  fperdvper  46898  dvbdfbdioolem1  46907  dvbdfbdioolem2  46908  dvbdfbdioo  46909  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc1  46912  ioodvbdlimc2lem  46913  ioodvbdlimc2  46914  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  itgcoscmulx  46948  volioc  46951  itgsincmulx  46953  itgiccshift  46959  itgperiod  46960  itgsbtaddcnst  46961  volico  46962  voliooico  46971  voliccico  46978  stoweidlem7  46986  stoweidlem11  46990  stoweidlem13  46992  stoweidlem17  46996  stoweidlem19  46998  stoweidlem20  46999  stoweidlem21  47000  stoweidlem22  47001  stoweidlem23  47002  stoweidlem24  47003  stoweidlem26  47005  stoweidlem32  47011  stoweidlem36  47015  stoweidlem44  47023  stoweidlem47  47026  wallispilem3  47046  wallispi2lem1  47050  stirlinglem1  47053  stirlinglem5  47057  stirlinglem11  47063  stirlinglem12  47064  stirlinglem14  47066  dirkerval2  47073  dirkerre  47074  dirkertrigeqlem2  47078  dirkertrigeq  47080  dirkeritg  47081  dirkercncflem1  47082  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem4  47090  fourierdlem6  47092  fourierdlem7  47093  fourierdlem13  47099  fourierdlem14  47100  fourierdlem16  47102  fourierdlem18  47104  fourierdlem19  47105  fourierdlem21  47107  fourierdlem22  47108  fourierdlem24  47110  fourierdlem26  47112  fourierdlem28  47114  fourierdlem30  47116  fourierdlem35  47121  fourierdlem39  47125  fourierdlem40  47126  fourierdlem41  47127  fourierdlem42  47128  fourierdlem43  47129  fourierdlem44  47130  fourierdlem47  47132  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem51  47136  fourierdlem53  47138  fourierdlem56  47141  fourierdlem57  47142  fourierdlem58  47143  fourierdlem59  47144  fourierdlem60  47145  fourierdlem61  47146  fourierdlem62  47147  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem66  47151  fourierdlem68  47153  fourierdlem70  47155  fourierdlem71  47156  fourierdlem72  47157  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem77  47162  fourierdlem78  47163  fourierdlem79  47164  fourierdlem80  47165  fourierdlem81  47166  fourierdlem83  47168  fourierdlem84  47169  fourierdlem85  47170  fourierdlem87  47172  fourierdlem88  47173  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem92  47177  fourierdlem93  47178  fourierdlem95  47180  fourierdlem97  47182  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem107  47192  fourierdlem109  47194  fourierdlem111  47196  fourierdlem112  47197  fouriercnp  47205  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  etransclem14  47227  etransclem18  47231  etransclem23  47236  etransclem24  47237  etransclem27  47240  etransclem46  47259  etransclem48  47261  qndenserrnbllem  47273  ioorrnopnlem  47283  sge0tsms  47359  sge0cl  47360  sge0split  47388  sge0iunmptlemfi  47392  sge0rpcpnf  47400  sge0isum  47406  sge0ad2en  47410  sge0xaddlem1  47412  sge0xaddlem2  47413  sge0gtfsumgt  47422  sge0seq  47425  meadif  47458  meaiininclem  47465  carageniuncllem1  47500  carageniuncllem2  47501  hoicvr  47527  hoicvrrex  47535  ovnsubaddlem1  47549  hsphoidmvle2  47564  hsphoidmvle  47565  hoidmvval0  47566  hoiprodp1  47567  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoiqssbllem2  47602  hspmbllem1  47605  ovolval2lem  47622  ovolval3  47626  ovolval5lem1  47631  ovnovollem1  47635  ovnovollem2  47636  vonioolem1  47659  vonioo  47661  vonicclem1  47662  vonicc  47664  smfaddlem1  47742  smflimlem4  47753  smfmullem1  47770  smfmullem2  47771  smfmullem3  47772  smfdiv  47776  smfneg  47782  sigaras  47834  sigarms  47835  sigarls  47836  sigarexp  47838  sigarperm  47839  sigarimcd  47841  sigarcol  47843  sharhght  47844  cevathlem2  47847  readdcnnred  48342  resubcnnred  48343  cndivrenred  48345  flmrecm1  48382  fldivmod  48383  ceildivmod  48384  m1mod0mod1  48399  m1modmmod  48403  difmodm1lt  48404  requad01  48688  requad1  48689  requad2  48690  fpprwppr  48806  bgoldbtbndlem2  48873  gpgvtxedg1  49131  ltsubaddb  49595  ltsubsubb  49596  ltsubadd2b  49597  flsubz  49603  logblt1b  49645  dignn0fr  49682  dignn0flhalflem1  49696  dignn0flhalflem2  49697  nn0sumshdiglemA  49700  affinecomb1  49783  affinecomb2  49784  resum2sqorgt0  49790  rrx2pnedifcoorneor  49797  rrx2pnedifcoorneorr  49798  ehl2eudisval0  49806  eenglngeehlnmlem1  49818  eenglngeehlnmlem2  49819  rrx2vlinest  49822  rrx2linest  49823  rrx2linest2  49825  2sphere0  49831  line2ylem  49832  line2  49833  line2xlem  49834  line2x  49835  line2y  49836  itscnhlc0yqe  49840  itschlc0yqe  49841  itsclc0yqsol  49845  itscnhlc0xyqsol  49846  itschlc0xyqsol1  49847  itschlc0xyqsol  49848  itsclc0xyqsolr  49850  itsclinecirc0b  49855  itsclquadb  49857  itsclquadeu  49858  2itscplem1  49859  2itscplem2  49860  2itscplem3  49861  2itscp  49862  itscnhlinecirc02plem1  49863  itscnhlinecirc02plem2  49864  itscnhlinecirc02p  49866  inlinecirc02plem  49867  inlinecirc02p  49868  crosspdotsumlem  50933  crosspdotd  50934  crosspaltd  50935  crossp3d  50936  veronesev1lem  50942  veronesev2lem  50943  veronesev3lem  50944  veronesev4lem  50945  veronesev5lem  50946  veronesev6lem  50947  veroquadgsumlem  50952  amgmwlem  50956  amgmlemALT  50957