Theorem recnd 11261

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

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

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 11181

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

This theorem is used by:  00id  11409  mul02lem1  11410  addrid  11414  cnegex  11415  ltadd1  11705  leadd2  11707  ltsubadd  11708  ltsubadd2  11709  lesubadd  11710  lesubadd2  11711  lesub1  11732  lesub2  11733  ltnegcon1  11739  ltnegcon2  11740  add20  11750  subge0  11751  suble0  11752  lesub0  11755  mulge0  11756  eqord2  11769  lesub3d  11856  possumd  11863  sublt0d  11864  rereccl  11957  redivcl  11958  recgt0  12085  prodgt0  12086  ltmul1a  12088  ltdiv1  12103  ltmuldiv  12112  ltrec  12121  recp1lt1  12137  recreclt  12138  ledivp1  12141  supadd  12207  infrenegsup  12222  rimul  12233  cru  12234  avglt1  12506  avglt2  12507  lt2addmuld  12518  div4p1lem1div2  12523  nn0cnd  12591  zcn  12620  zeo  12707  zcnd  12726  eluzmn  12894  eluzelcn  12899  cnref1o  13035  rpcn  13053  rpcnd  13088  ltaddrp2d  13120  mul2lt0rlt0  13146  mul2lt0rgt0  13147  mul2lt0llt0  13148  mul2lt0lgt0  13149  mul2lt0bi  13150  prodge0rd  13151  prodge0ld  13152  qbtwnre  13251  xralrple  13257  xpncan  13303  xmulcom  13318  xmulneg1  13321  xlemul1  13342  elunitcn  13521  icoshftf1o  13527  lincmb01cmp  13548  iccf1o  13549  divfl0  13885  fladdz  13886  flzadd  13887  flhalf  13891  ceim1l  13908  intfracq  13920  fldiv  13921  modvalr  13933  flpmodeq  13935  mod0  13937  modlt  13941  moddiffl  13943  modfrac  13945  flmod  13946  intfrac  13947  modmulnn  13950  modvalp1  13951  modid  13957  modcyc  13967  modadd1  13969  modaddb  13970  modaddabs  13972  modmuladdnn0  13979  negmod  13980  modadd2mod  13985  modnegd  13990  modadd12d  13991  modsub12d  13992  modmulmodr  14001  modaddmulmod  14002  moddi  14003  modsubdir  14004  modeqmodmin  14005  modirr  14006  addmodlteq  14010  seqf1olem1  14105  serle  14121  expcl2lem  14137  expnegz  14160  expaddzlem  14169  expaddz  14170  expmulz  14172  sq11  14195  ltexp2a  14230  expmordi  14231  leexp2a  14236  leexp2r  14238  exple1  14241  expubnd  14242  bernneq2  14294  expmulnbnd  14299  discr1  14303  discr  14304  faclbnd  14354  bcp1nk  14381  cshweqrep  14892  sgnsub  15179  sgnmul  15180  remim  15204  reim0b  15206  rereb  15207  mulre  15208  cjreb  15210  recj  15211  reneg  15212  readd  15213  resub  15214  remullem  15215  remul2  15217  rediv  15218  imcj  15219  imneg  15220  imadd  15221  imsub  15222  immul2  15224  imdiv  15225  cjcj  15227  cjadd  15228  ipcnval  15230  cjmulval  15232  cjneg  15234  imval2  15238  cjreim2  15248  01sqrexlem5  15333  01sqrexlem7  15335  resqrtthlem  15341  remsqsqrt  15343  sqrtmul  15346  sqrtdiv  15352  sqrtneg  15354  sqrtmsq  15357  absdiv  15382  absid  15383  absexp  15391  absexpz  15392  absimle  15396  abslt  15402  absle  15403  abssubne0  15404  releabs  15409  recval  15410  abstri  15418  abs2difabs  15422  abs1m  15423  abslem2  15427  absrdbnd  15429  sqreulem  15447  sqreu  15448  amgm2  15457  icodiamlt  15525  bhmafibid1  15555  bhmafibid2  15556  lo1bddrp  15612  o1lo1  15624  rlimrecl  15667  rlimge0  15668  climrecl  15670  climge0  15671  climabs0  15672  reccn2  15684  o1rlimmul  15706  lo1mul2  15716  lo1sub  15718  climle  15727  climsqz  15728  climsqz2  15729  rlimsqz  15737  rlimsqz2  15738  climlec2  15746  isercolllem1  15752  climsup  15757  caucvgrlem  15760  caurcvgr  15761  caucvgrlem2  15762  iseraltlem1  15769  iseraltlem2  15770  iseraltlem3  15771  iseralt  15772  isumrecl  15851  isumge0  15852  fsumless  15883  fsumge1  15884  fsum00  15885  fsumle  15886  fsumlt  15887  fsumabs  15888  o1fsum  15900  seqabs  15901  cvgcmp  15903  cvgcmpce  15905  abscvgcvg  15906  indsum  15915  indsumhash  15916  isumrpcl  15932  isumle  15933  isumless  15934  isumsup  15936  climcndslem1  15938  climcndslem2  15939  climcnds  15940  flo1  15943  supcvg  15945  trireciplem  15951  trirecip  15952  explecnv  15954  geo2sum  15962  geo2lim  15964  geomulcvg  15965  cvgrat  15972  mertenslem1  15973  mertenslem2  15974  fprodabs  16061  fprodle  16083  iprodrecl  16089  bpolydiflem  16140  bpoly4  16145  efcllem  16163  ege2le3  16176  efaddlem  16179  efgt0  16191  eftlub  16197  effsumlt  16199  eflt  16205  eflegeo  16209  resin4p  16226  recos4p  16227  retanhcl  16247  tanhlt1  16248  efeul  16250  ef01bndlem  16272  sin01bnd  16273  cos01bnd  16274  sin01gt0  16278  cos01gt0  16279  sin02gt0  16280  absefi  16284  absef  16285  absefib  16286  efieq1re  16287  eirrlem  16292  rpnnen2lem5  16306  rpnnen2lem8  16309  rpnnen2lem9  16310  rpnnen2lem11  16312  rpnnen2lem12  16313  moddvds  16353  odd2np1  16431  divalglem5  16487  bitsp1o  16523  bitsfzo  16525  bitscmp  16528  sadcaddlem  16547  nn0seqcvgd  16660  sqnprm  16793  isprm5  16798  nonsq  16850  eulerthlem2  16873  prmdiveq  16877  odzdvds  16887  vfermltlALT  16894  pythagtriplem14  16920  pcid  16965  fldivp1  16989  pcfac  16991  pockthlem  16997  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  prmrec  17014  4sqlem5  17034  4sqlem10  17039  mul4sqlem  17045  4sqlem15  17051  4sqlem16  17052  mulgneg  19215  ghmmulg  19355  odmodnn0  19667  mndodconglem  19668  pgpfaclem2  20211  isabvd  20978  abv1z  20990  abvneg  20992  abvrec  20994  abvdiv  20995  abvdom  20996  rege0subm  21636  cnsubrg  21640  gzrngunitlem  21645  regsumfsum  21648  prmirredlem  21685  remulg  21820  rzgrp  21836  bl2in  24626  blhalf  24631  blssps  24650  blss  24651  methaus  24746  nrmmetd  24800  nm2dif  24851  nminvr  24895  nmdvr  24896  nlmmul0or  24909  nrginvrcnlem  24917  nmolb2d  24944  nmoi2  24956  nmoleub  24957  nmo0  24961  nmoeq0  24962  nmoco  24963  nmotri  24965  nmoid  24968  blcvx  25024  xrsxmet  25036  recld2  25041  reconnlem2  25054  opnreen  25058  metdstri  25078  metnrmlem3  25088  icchmeo  25169  icopnfcnv  25170  icopnfhmeo  25171  iccpnfhmeo  25173  xrhmeo  25174  icccvx  25178  cnheiborlem  25182  evth  25187  lebnumii  25194  pcoass  25252  pcorevlem  25254  pcorev2  25256  pi1xfrcnv  25285  nmoleub2lem  25342  nmoleub2lem3  25343  nmoleub3  25347  ncvsm1  25382  ncvspi  25384  ncvs1  25385  cphsqrtcl2  25414  ipcau2  25462  tcphcphlem1  25463  tcphcphlem2  25464  tcphcph  25465  cphipval2  25469  cphipval  25471  iscau3  25506  rrxnm  25619  rrxcph  25620  csbren  25627  trirn  25628  rrxmval  25633  rrxmetlem  25635  rrxmet  25636  rrxdstprj1  25637  ehl1eudis  25648  ehl2eudis  25650  minveclem2  25654  minveclem3b  25656  minveclem4  25660  minveclem6  25662  minveclem7  25663  pjthlem1  25665  ivthlem2  25680  ivthlem3  25681  ivth2  25683  ovolfsval  25698  ovollb2lem  25716  ovolctb  25718  ovolunlem1a  25724  ovolunnul  25728  ovolfiniun  25729  ovoliunlem1  25730  ovoliun2  25734  shft2rab  25736  ovolshftlem1  25737  sca2rab  25740  ovolscalem1  25741  ovolsca  25743  ovolicc1  25744  ovolicc2lem4  25748  ovolicopnf  25752  cmmbl  25762  nulmbl  25763  nulmbl2  25764  unmbl  25765  volinun  25774  volfiniun  25775  voliunlem1  25778  voliunlem3  25780  ioombl1lem3  25788  ioombl1lem4  25789  ovolioo  25796  ioorcl2  25800  uniioovol  25807  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  uniioombllem6  25816  dyadovol  25821  dyaddisjlem  25823  opnmbllem  25829  vitalilem1  25836  vitalilem2  25837  vitalilem3  25838  vitalilem4  25839  ismbf  25856  mbfmulc2lem  25875  mbfmulc2re  25876  mbfmulc2  25891  mbfinf  25893  itg1val2  25912  itg11  25919  i1fmullem  25922  i1fadd  25923  itg1addlem4  25927  itg1addlem5  25928  i1fmulclem  25930  i1fmulc  25931  itg1mulc  25932  itg1sub  25937  itg10a  25938  itg1ge0a  25939  itg1climres  25942  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  mbfi1flimlem  25950  mbfmullem2  25952  itg2const  25968  itg2const2  25969  itg2mulclem  25974  itg2mulc  25975  itg2splitlem  25976  itg2split  25977  itg2monolem1  25978  itg2monolem3  25980  itg2addlem  25986  itgcl  26011  itgcnlem  26017  itgrevallem1  26022  itgposval  26023  iblneg  26030  itgneg  26031  i1fibl  26035  itgitg1  26036  itgconst  26046  ibladd  26048  itgaddlem2  26051  iblabslem  26055  iblabs  26056  iblabsr  26057  iblmulc2  26058  itgmulc2lem2  26060  itgmulc2  26061  itgabs  26062  itgsplit  26063  bddmulibl  26066  bddiblnc  26069  dvcjbr  26176  dvfre  26178  dvexp3  26205  dveflem  26206  dvferm1lem  26211  dvferm2lem  26213  rolle  26217  cmvth  26218  mvth  26219  dvlip  26220  dvlipcn  26221  c1liplem1  26223  c1lip1  26224  dveq0  26227  dv11cn  26228  dvlt0  26232  dvle  26234  dvivthlem1  26235  dvivth  26237  lhop1lem  26240  lhop1  26241  lhop2  26242  lhop  26243  dvcvx  26247  dvfsumle  26248  dvfsumge  26249  dvfsumabs  26250  dvfsumlem1  26253  dvfsumlem2  26254  dvfsumlem4  26256  dvfsumrlimge0  26257  dvfsumrlim2  26259  dvfsum2  26261  ftc1a  26264  ftc1lem4  26266  ftc1lem5  26267  itgpowd  26277  plyeq0lem  26436  coemulhi  26480  plyrecj  26507  plyn0mulidp  26511  plydivlem3  26525  aalioulem2  26569  aalioulem3  26570  aalioulem4  26571  aalioulem5  26572  aalioulem6  26573  aaliou  26574  aaliou2  26576  aaliou2b  26577  aaliou3lem3  26580  aaliou3lem7  26585  aaliou3lem9  26586  taylthlem2  26610  ulmcn  26635  ulmdvlem1  26636  mtest  26640  mtestbdd  26641  itgulm  26644  radcnvlem1  26649  radcnvlem2  26650  radcnvlt1  26654  radcnvle  26656  dvradcnv  26657  pserulm  26658  abelthlem2  26668  abelthlem5  26671  abelthlem7  26674  abelth2  26678  reeff1olem  26682  efcvx  26685  pilem2  26688  pilem3  26689  sincosq2sgn  26737  sincosq3sgn  26738  sincosq4sgn  26739  coseq0negpitopi  26741  tanrpcl  26742  tangtx  26743  tanabsge  26744  sinq12gt0  26745  sinq34lt0t  26747  cosq14gt0  26748  cosq14ge0  26749  pige3ALT  26757  coskpi  26760  cos02pilt1  26763  cosordlem  26767  sinord  26771  tanord1  26774  tanord  26775  tanregt0  26776  efif1olem2  26780  efif1olem4  26782  eff1olem  26785  logrnaddcl  26811  logneg  26825  lognegb  26827  reexplog  26832  relogexp  26833  logfac  26838  efiarg  26844  cosargd  26845  cosarg0d  26846  argregt0  26847  argrege0  26848  argimgt0  26849  logneg2  26852  logmul2  26853  logdiv2  26854  abslogle  26855  tanarg  26856  logdivlti  26857  divlogrlim  26872  logcnlem2  26880  logcnlem3  26881  logcnlem4  26882  logcn  26884  logf1o2  26887  advlog  26891  advlogexp  26892  efopnlem1  26893  logtayllem  26896  logtayl  26897  logccv  26900  logcxp  26906  mulcxp  26922  divcxp  26924  cxpmul  26925  cxproot  26927  cxpmul2z  26928  abscxp  26929  abscxp2  26930  cxplt  26931  cxplea  26933  cxple2  26934  cxple2a  26936  cxplt3  26937  cxpsqrtlem  26939  cxpsqrt  26940  logsqrt  26941  dvcxp2  26978  cxpcn3lem  26984  resqrtcn  26986  cxpaddlelem  26988  cxpaddle  26989  abscxpbnd  26990  root1id  26991  root1eq1  26992  root1cj  26993  cxpeq  26994  loglesqrt  26998  relogbmul  27014  nnlogbexp  27018  logbrec  27019  cosangneg2d  27044  angrtmuld  27045  ang180lem2  27047  lawcoslem1  27052  lawcos  27053  pythag  27054  isosctrlem1  27055  isosctrlem2  27056  isosctrlem3  27057  ssscongptld  27059  chordthmlem  27069  chordthmlem2  27070  chordthmlem3  27071  chordthmlem4  27072  chordthmlem5  27073  heron  27075  asinsinlem  27128  reasinsin  27133  acosrecl  27140  atancj  27147  atanrecl  27148  atanlogaddlem  27150  atanlogsublem  27152  atanbndlem  27162  atans2  27168  ressatans  27171  atantayl  27174  leibpilem2  27178  leibpi  27179  leibpisum  27180  log2tlbnd  27182  log2ublem2  27184  birthdaylem2  27189  birthdaylem3  27190  cxp2limlem  27212  cxp2lim  27213  cxploglim  27214  cxploglim2  27215  divsqrtsumo1  27220  cvxcl  27221  scvxcvx  27222  jensenlem2  27224  jensen  27225  amgmlem  27226  logdiflbnd  27231  emcllem2  27233  emcllem3  27234  emcllem5  27236  emcllem6  27237  emcllem7  27238  harmonicbnd4  27247  fsumharmonic  27248  zetacvg  27251  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem4  27268  lgamgulmlem5  27269  lgamgulmlem6  27270  lgamgulm2  27272  lgambdd  27273  lgamcvg2  27291  gamcvg  27292  gamcvg2lem  27295  regamcl  27297  relgamcl  27298  lgam1  27300  ftalem1  27309  ftalem2  27310  ftalem4  27312  ftalem5  27313  basellem3  27319  basellem4  27320  basellem5  27321  basellem6  27322  basellem7  27323  basellem8  27324  basellem9  27325  efnnfsumcl  27339  chtprm  27389  chpp1  27391  chtdif  27394  efchtdvds  27395  prmorcht  27414  mumullem2  27416  fsumfldivdiaglem  27425  ppiub  27440  chtleppi  27446  chtublem  27447  chtub  27448  pclogsum  27451  vmasum  27452  logfac2  27453  chpval2  27454  chpchtsum  27455  chpub  27456  logfaclbnd  27458  logfacbnd3  27459  logfacrlim  27460  logexprlim  27461  logfacrlim2  27462  mersenne  27463  dchrabs  27496  dchrptlem1  27500  dchrptlem2  27501  bcmax  27514  bcp1ctr  27515  bposlem1  27520  bposlem9  27528  lgsvalmod  27552  lgsdilem  27560  lgsne0  27571  lgsqrlem2  27583  gausslemma2dlem1a  27601  gausslemma2dlem6  27608  lgseisenlem1  27611  lgseisenlem2  27612  lgseisen  27615  lgsquadlem1  27616  lgsquadlem2  27617  mul2sq  27655  2sqlem3  27656  2sqlem8  27662  2sqmod  27672  2sqreulem1  27682  2sqreunnlem1  27685  chebbnd1lem1  27705  chebbnd1lem2  27706  chebbnd1lem3  27707  chtppilimlem1  27709  chtppilimlem2  27710  chtppilim  27711  chto1ub  27712  chto1lb  27714  chpchtlim  27715  chpo1ub  27716  vmadivsum  27718  vmadivsumb  27719  rplogsumlem1  27720  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlema  27724  dchrisumlem1  27725  dchrisumlem2  27726  dchrisumlem3  27727  dchrmusumlema  27729  dchrmusum2  27730  dchrvmasumlem1  27731  dchrvmasum2lem  27732  dchrvmasum2if  27733  dchrvmasumlem2  27734  dchrvmasumlem3  27735  dchrvmasumiflem1  27737  dchrvmasumiflem2  27738  dchrisum0flblem1  27744  dchrisum0fno1  27747  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lema  27750  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  dchrmusumlem  27758  dchrvmasumlem  27759  rpvmasum  27762  rplogsum  27763  dirith2  27764  mudivsum  27766  mulogsumlem  27767  mulogsum  27768  logdivsum  27769  mulog2sumlem1  27770  mulog2sumlem2  27771  mulog2sumlem3  27772  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  logsqvma  27778  logsqvma2  27779  log2sumbnd  27780  selberglem1  27781  selberglem2  27782  selberglem3  27783  selberg  27784  selbergb  27785  selberg2lem  27786  selberg2  27787  selberg2b  27788  chpdifbndlem1  27789  logdivbnd  27792  selberg3lem1  27793  selberg3lem2  27794  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrmax  27800  pntrsumo1  27801  pntrsumbnd  27802  pntrsumbnd2  27803  selbergr  27804  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntsval2  27812  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6a  27818  pntrlog2bndlem6  27819  pntrlog2bnd  27820  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntibndlem2  27827  pntibndlem3  27828  pntlemb  27833  pntlemg  27834  pntlemh  27835  pntlemn  27836  pntlemr  27838  pntlemj  27839  pntlemf  27841  pntlemk  27842  pntlemo  27843  pntlem3  27845  pntleml  27847  pnt2  27849  pnt  27850  abvcxp  27851  ostth2lem1  27854  qabvexp  27862  padicabv  27866  padicabvcxp  27868  ostth2lem2  27870  ostth2lem3  27871  ostth2lem4  27872  ostth2  27873  ostth3  27874  ttgcontlem1  29341  fveecn  29359  eqeelen  29361  brbtwn2  29362  colinearalglem4  29366  colinearalg  29367  axsegconlem9  29382  axsegconlem10  29383  ax5seglem1  29385  ax5seglem2  29386  ax5seglem3  29388  ax5seglem5  29390  ax5seglem6  29391  ax5seglem9  29394  ax5seg  29395  axbtwnid  29396  axpaschlem  29397  axpasch  29398  axeuclidlem  29419  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  axcontlem8  29428  elntg2  29442  nrt2irr  30953  nvm1  31146  nvpi  31148  nvz0  31149  nvmtri  31152  nvabs  31153  nvge0  31154  nv1  31156  smcnlem  31178  ipval2lem4  31187  ipval2  31188  4ipval2  31189  ipidsq  31191  dipcj  31195  dip0r  31198  ipz  31200  nmoub3i  31254  nmlno0lem  31274  nmblolbii  31280  blocnilem  31285  cncph  31300  ipasslem4  31315  ipasslem5  31316  ipblnfi  31336  minvecolem2  31356  minvecolem4  31361  minvecolem6  31363  minvecolem7  31364  htthlem  31398  normpyc  31627  hhph  31659  bcs2  31663  norm1  31730  norm1exi  31731  pjhthlem1  31872  eigvalcl  32442  eighmorth  32445  nmlnop0iALT  32476  nmbdoplbi  32505  nmcexi  32507  nmcoplbi  32509  nmbdfnlbi  32530  nmcfnlbi  32533  riesz4i  32544  cnlnadjlem2  32549  cnlnadjlem7  32554  nmopcoi  32576  nmopcoadji  32582  branmfn  32586  leopnmid  32619  opsqrlem1  32621  hst1h  32708  hstle  32711  hstoh  32713  sto2i  32718  stadd3i  32729  strlem1  32731  golem1  32752  stcltrlem1  32757  cdj1i  32914  cdj3lem1  32915  cdj3lem3b  32921  cdj3i  32922  sgnval2  33206  re0cj  33214  receqid  33215  pythagreim  33216  lt2addrd  33221  le2halvesd  33227  fzsplit3  33264  bcm1n  33266  expgt0b  33287  fsumiunle  33299  nexple  33303  expevenpos  33305  oexpled  33306  wrdt2ind  33395  psgnfzto1stlem  33540  ccfldsrarelvec  34181  ccfldextdgrr  34182  constrrtll  34241  constrrtlc1  34242  constrrtlc2  34243  constrconj  34255  nn0constr  34271  constrnegcl  34273  constrdircl  34275  iconstr  34276  constrremulcl  34277  constrrecl  34279  constrimcl  34280  constrmulcl  34281  constrreinvcl  34282  constrinvcl  34283  constrresqrtcl  34287  constrabscl  34288  constrsqrtcl  34289  cos9thpiminplylem1  34292  sqsscirc1  34418  sqsscirc2  34419  cnre2csqima  34421  rmulccn  34438  xrge0iifcnv  34443  xrge0iifhom  34447  zrhnm  34477  rezh  34479  esumpcvgval  34588  esumcvgsum  34598  dya2ub  34781  dya2icoseg  34788  omssubadd  34811  eulerpartlemgc  34873  ballotlemsi  35026  signsply0  35059  signsvtp  35091  signsvtn  35092  signsvfpn  35093  signsvfnn  35094  divsqrtid  35102  reprgt  35129  reprinfz1  35130  breprexplemc  35140  circlemethhgt  35151  hgt750lemd  35156  hgt750lemf  35161  hgt750lemg  35162  hgt750lemb  35164  hgt750lema  35165  hgt750leme  35166  tgoldbachgtde  35168  subfacval2  35766  subfaclim  35767  subfacval3  35768  resconn  35825  sinccvglem  36251  circum  36253  climlec3  36313  faclimlem1  36322  faclimlem2  36323  faclimlem3  36324  faclim  36325  iprodfac  36326  faclim2  36327  dnicld1  37169  dnizeq0  37172  dnizphlfeqhlf  37173  dnibndlem2  37176  dnibndlem3  37177  dnibndlem5  37179  dnibndlem6  37180  dnibndlem7  37181  dnibndlem8  37182  dnibndlem9  37183  dnibndlem10  37184  dnibndlem11  37185  dnibndlem12  37186  dnibndlem13  37187  dnibnd  37188  dnicn  37189  knoppcnlem4  37193  knoppcnlem5  37194  knoppcnlem6  37195  knoppcnlem8  37197  knoppcnlem9  37198  knoppcnlem10  37199  knoppcnlem11  37200  unblimceq0  37204  unbdqndv2lem1  37206  unbdqndv2lem2  37207  knoppndvlem1  37209  knoppndvlem6  37214  knoppndvlem8  37216  knoppndvlem9  37217  knoppndvlem10  37218  knoppndvlem11  37219  knoppndvlem12  37220  knoppndvlem14  37222  knoppndvlem15  37223  knoppndvlem17  37225  knoppndvlem18  37226  knoppndvlem19  37227  knoppndvlem20  37228  knoppndvlem21  37229  irrdifflemf  38077  irrdiff  38078  qdiff  38079  ltflcei  38362  sin2h  38364  cos2h  38365  tan2h  38366  poimirlem29  38398  opnmbllem0  38405  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  mbfposadd  38416  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  ibladdnc  38426  itgaddnclem2  38428  iblabsnclem  38432  iblabsnc  38433  iblmulc2nc  38434  itgmulc2nclem2  38436  itgmulc2nc  38437  itgabsnc  38438  ftc1cnnclem  38440  ftc1cnnc  38441  ftc1anclem1  38442  ftc1anclem2  38443  ftc1anclem3  38444  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  areacirclem1  38457  areacirclem5  38461  areacirc  38462  mettrifi  38507  lmclim2  38508  geomcau  38509  isbnd3  38534  ssbnd  38538  cntotbnd  38546  bfplem1  38572  bfplem2  38573  bfp  38574  rrnmet  38579  rrndstprj1  38580  rrndstprj2  38581  rrncmslem  38582  rrnequiv  38585  rrntotbnd  38586  ismrer1  38588  lcmineqlem18  42912  lcmineqlem19  42913  lcmineqlem20  42914  lcmineqlem21  42915  lcmineqlem22  42916  3lexlogpow5ineq2  42921  3lexlogpow2ineq1  42924  3lexlogpow2ineq2  42925  3lexlogpow5ineq5  42926  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p4  42937  dvle2  42938  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8d2  42951  aks4d1p8  42953  posbezout  42966  aks6d1c1  42982  hashscontpow1  42987  aks6d1c3  42989  aks6d1c4  42990  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem3  43003  aks6d1c5lem2  43004  2np3bcnp1  43010  sticksstones6  43017  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem4  43039  bcled  43044  bcle2d  43045  aks6d1c7lem1  43046  aks6d1c7lem2  43047  remulcan2d  43123  readdridaddlidd  43124  readdrcl2d  43148  sumcubes  43188  oexpreposd  43197  expeqidd  43200  rxp112d  43220  rxp11d  43223  readvrec2  43236  readvrec  43237  resuppsinopn  43238  readvcot  43239  resubeulem1  43250  resubeulem2  43251  readdsub  43259  resubsub4  43264  resubidaddlidlem  43269  resubdi  43271  sn-addlid  43279  remul02  43280  remul01  43282  renegneg  43287  readdcan2  43288  renegid2  43289  sn-it0e0  43291  sn-negex12  43292  reixi  43298  remulinvcom  43308  remullid  43309  remulcand  43314  rediveud  43318  redivrec2d  43335  rediv23d  43336  redivdird  43337  sn-0tie0  43339  zaddcomlem  43351  zaddcom  43352  renegmulnnass  43353  mulgt0b1d  43360  mulgt0b2d  43366  mullt0b1d  43371  sn-itrere  43376  sn-retire  43377  cnreeu  43378  frlmvscadiccat  43394  abvexp  43414  dffltz  43480  fltnltalem  43508  fltnlta  43509  negexpidd  43527  3cubeslem1  43529  3cubeslem2  43530  3cubeslem4  43534  eldioph2lem1  43605  lzenom  43615  rencldnfilem  43661  irrapxlem1  43663  irrapxlem2  43664  irrapxlem3  43665  irrapxlem4  43666  irrapxlem5  43667  pellexlem2  43671  pellexlem6  43675  pell1234qrreccl  43695  pell14qrgt0  43700  pell14qrdivcl  43706  pell14qrexpclnn0  43707  pell14qrexpcl  43708  pell14qrdich  43710  pell1qrgaplem  43714  pellfundex  43727  reglogmul  43734  reglogexp  43735  reglogbas  43736  reglog1  43737  pellfund14  43739  rmspecfund  43750  monotoddzzfi  43783  jm2.24nn  43800  jm2.17a  43801  jm2.17b  43802  jm2.17c  43803  jm2.24  43804  acongrep  43821  fzmaxdif  43822  acongeq  43824  modabsdifz  43827  jm2.19lem4  43833  jm2.19  43834  jm2.26lem3  43842  jm3.1lem1  43858  jm3.1lem2  43859  areaquad  44057  sqrtcvallem4  44479  sqrtcval  44481  sqrtcval2  44482  absmulrposd  44999  extoimad  45004  imo72b2lem0  45005  imo72b2lem1  45009  imo72b2  45012  int-addcomd  45013  int-addassocd  45014  int-addsimpd  45015  int-mulcomd  45016  int-mulassocd  45017  int-mulsimpd  45018  int-leftdistd  45019  int-rightdistd  45020  int-sqdefd  45021  int-mul11d  45022  int-mul12d  45023  int-add01d  45024  int-add02d  45025  int-sqgeq0d  45026  int-eqmvtd  45029  cvgdvgrat  45137  radcnvrat  45138  hashnzfzclim  45146  dvconstbi  45158  binomcxplemnn0  45173  binomcxplemnotnn0  45180  isosctrlem1ALT  45756  sineq0ALT  45759  infnsuprnmpt  46079  oddfl  46111  dstregt0  46115  zltlesub  46118  lt3addmuld  46134  fperiodmullem  46136  fperiodmul  46137  lt4addmuld  46139  fzdifsuc2  46143  supxrgere  46163  supxrgelem  46167  suplesup  46169  supsubc  46183  xralrple2  46184  abslt2sqd  46190  xralrple3  46203  reclt0d  46216  ltmulneg  46221  rexabslelem  46246  supminfrnmpt  46273  leneg2d  46276  leneg3d  46285  supminfxr  46292  absimnre  46304  absimlere  46307  iooabslt  46329  iccshift  46348  iooshift  46352  sqrlearg  46383  fmul01  46410  fmul01lt1lem1  46414  fmul01lt1lem2  46415  fprodabs2  46425  climinf  46436  limcrecl  46459  lptre2pt  46468  limcleqr  46472  0ellimcdiv  46477  limclner  46479  climleltrp  46504  climinf2mpt  46542  climinf3  46544  climxrre  46578  climliminflimsupd  46629  liminfltlem  46632  liminflimsupclim  46635  cnrefiisplem  46657  sinaover2ne0  46696  cncfperiod  46707  ioccncflimc  46713  cncficcgt0  46716  icocncflimc  46717  cncfshiftioo  46720  cncfiooicc  46722  fperdvper  46747  dvbdfbdioolem1  46756  dvbdfbdioolem2  46757  dvbdfbdioo  46758  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc1  46761  ioodvbdlimc2lem  46762  ioodvbdlimc2  46763  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  itgcoscmulx  46797  volioc  46800  itgsincmulx  46802  itgiccshift  46808  itgperiod  46809  itgsbtaddcnst  46810  volico  46811  voliooico  46820  voliccico  46827  stoweidlem7  46835  stoweidlem11  46839  stoweidlem13  46841  stoweidlem17  46845  stoweidlem19  46847  stoweidlem20  46848  stoweidlem21  46849  stoweidlem22  46850  stoweidlem23  46851  stoweidlem24  46852  stoweidlem26  46854  stoweidlem32  46860  stoweidlem36  46864  stoweidlem44  46872  stoweidlem47  46875  wallispilem3  46895  wallispi2lem1  46899  stirlinglem1  46902  stirlinglem5  46906  stirlinglem11  46912  stirlinglem12  46913  stirlinglem14  46915  dirkerval2  46922  dirkerre  46923  dirkertrigeqlem2  46927  dirkertrigeq  46929  dirkeritg  46930  dirkercncflem1  46931  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem4  46939  fourierdlem6  46941  fourierdlem7  46942  fourierdlem13  46948  fourierdlem14  46949  fourierdlem16  46951  fourierdlem18  46953  fourierdlem19  46954  fourierdlem21  46956  fourierdlem22  46957  fourierdlem24  46959  fourierdlem26  46961  fourierdlem28  46963  fourierdlem30  46965  fourierdlem35  46970  fourierdlem39  46974  fourierdlem40  46975  fourierdlem41  46976  fourierdlem42  46977  fourierdlem43  46978  fourierdlem44  46979  fourierdlem47  46981  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem51  46985  fourierdlem53  46987  fourierdlem56  46990  fourierdlem57  46991  fourierdlem58  46992  fourierdlem59  46993  fourierdlem60  46994  fourierdlem61  46995  fourierdlem62  46996  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem66  47000  fourierdlem68  47002  fourierdlem70  47004  fourierdlem71  47005  fourierdlem72  47006  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem77  47011  fourierdlem78  47012  fourierdlem79  47013  fourierdlem80  47014  fourierdlem81  47015  fourierdlem83  47017  fourierdlem84  47018  fourierdlem85  47019  fourierdlem87  47021  fourierdlem88  47022  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem93  47027  fourierdlem95  47029  fourierdlem97  47031  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem107  47041  fourierdlem109  47043  fourierdlem111  47045  fourierdlem112  47046  fouriercnp  47054  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem14  47076  etransclem18  47080  etransclem23  47085  etransclem24  47086  etransclem27  47089  etransclem46  47108  etransclem48  47110  qndenserrnbllem  47122  ioorrnopnlem  47132  sge0tsms  47208  sge0cl  47209  sge0split  47237  sge0iunmptlemfi  47241  sge0rpcpnf  47249  sge0isum  47255  sge0ad2en  47259  sge0xaddlem1  47261  sge0xaddlem2  47262  sge0gtfsumgt  47271  sge0seq  47274  meadif  47307  meaiininclem  47314  carageniuncllem1  47349  carageniuncllem2  47350  hoicvr  47376  hoicvrrex  47384  ovnsubaddlem1  47398  hsphoidmvle2  47413  hsphoidmvle  47414  hoidmvval0  47415  hoiprodp1  47416  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoiqssbllem2  47451  hspmbllem1  47454  ovolval2lem  47471  ovolval3  47475  ovolval5lem1  47480  ovnovollem1  47484  ovnovollem2  47485  vonioolem1  47508  vonioo  47510  vonicclem1  47511  vonicc  47513  smfaddlem1  47591  smflimlem4  47602  smfmullem1  47619  smfmullem2  47620  smfmullem3  47621  smfdiv  47625  smfneg  47631  sigaras  47683  sigarms  47684  sigarls  47685  sigarexp  47687  sigarperm  47688  sigarimcd  47690  sigarcol  47692  sharhght  47693  cevathlem2  47696  readdcnnred  48191  resubcnnred  48192  cndivrenred  48194  flmrecm1  48231  fldivmod  48232  ceildivmod  48233  m1mod0mod1  48248  m1modmmod  48252  difmodm1lt  48253  requad01  48537  requad1  48538  requad2  48539  fpprwppr  48655  bgoldbtbndlem2  48722  gpgvtxedg1  48980  ltsubaddb  49444  ltsubsubb  49445  ltsubadd2b  49446  flsubz  49452  logblt1b  49494  dignn0fr  49531  dignn0flhalflem1  49545  dignn0flhalflem2  49546  nn0sumshdiglemA  49549  affinecomb1  49632  affinecomb2  49633  resum2sqorgt0  49639  rrx2pnedifcoorneor  49646  rrx2pnedifcoorneorr  49647  ehl2eudisval0  49655  eenglngeehlnmlem1  49667  eenglngeehlnmlem2  49668  rrx2vlinest  49671  rrx2linest  49672  rrx2linest2  49674  2sphere0  49680  line2ylem  49681  line2  49682  line2xlem  49683  line2x  49684  line2y  49685  itscnhlc0yqe  49689  itschlc0yqe  49690  itsclc0yqsol  49694  itscnhlc0xyqsol  49695  itschlc0xyqsol1  49696  itschlc0xyqsol  49697  itsclc0xyqsolr  49699  itsclinecirc0b  49704  itsclquadb  49706  itsclquadeu  49707  2itscplem1  49708  2itscplem2  49709  2itscplem3  49710  2itscp  49711  itscnhlinecirc02plem1  49712  itscnhlinecirc02plem2  49713  itscnhlinecirc02p  49715  inlinecirc02plem  49716  inlinecirc02p  49717  crosspdotsumlem  50797  crosspdotd  50798  crosspaltd  50799  crossp3d  50800  veronesev1lem  50806  veronesev2lem  50807  veronesev3lem  50808  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811  veroquadgsumlem  50816  amgmwlem  50820  amgmlemALT  50821