Theorem recnd 11248

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11109  ℝcr 11110

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 2148  ax-resscn 11168

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

This theorem is used by:  00id  11396  mul02lem1  11397  addrid  11401  cnegex  11402  ltadd1  11692  leadd2  11694  ltsubadd  11695  ltsubadd2  11696  lesubadd  11697  lesubadd2  11698  lesub1  11719  lesub2  11720  ltnegcon1  11726  ltnegcon2  11727  add20  11737  subge0  11738  suble0  11739  lesub0  11742  mulge0  11743  eqord2  11756  lesub3d  11843  possumd  11850  sublt0d  11851  rereccl  11944  redivcl  11945  recgt0  12072  prodgt0  12073  ltmul1a  12075  ltdiv1  12090  ltmuldiv  12099  ltrec  12108  recp1lt1  12124  recreclt  12125  ledivp1  12128  supadd  12194  infrenegsup  12209  rimul  12220  cru  12221  avglt1  12493  avglt2  12494  lt2addmuld  12505  div4p1lem1div2  12510  nn0cnd  12578  zcn  12607  zeo  12693  zcnd  12712  eluzmn  12880  eluzelcn  12885  cnref1o  13020  rpcn  13038  rpcnd  13073  ltaddrp2d  13105  mul2lt0rlt0  13131  mul2lt0rgt0  13132  mul2lt0llt0  13133  mul2lt0lgt0  13134  mul2lt0bi  13135  prodge0rd  13136  prodge0ld  13137  qbtwnre  13236  xralrple  13242  xpncan  13288  xmulcom  13303  xmulneg1  13306  xlemul1  13327  elunitcn  13506  icoshftf1o  13512  lincmb01cmp  13533  iccf1o  13534  divfl0  13870  fladdz  13871  flzadd  13872  flhalf  13876  ceim1l  13893  intfracq  13905  fldiv  13906  modvalr  13918  flpmodeq  13920  mod0  13922  modlt  13926  moddiffl  13928  modfrac  13930  flmod  13931  intfrac  13932  modmulnn  13935  modvalp1  13936  modid  13942  modcyc  13952  modadd1  13954  modaddb  13955  modaddabs  13957  modmuladdnn0  13964  negmod  13965  modadd2mod  13970  modnegd  13975  modadd12d  13976  modsub12d  13977  modmulmodr  13986  modaddmulmod  13987  moddi  13988  modsubdir  13989  modeqmodmin  13990  modirr  13991  addmodlteq  13995  seqf1olem1  14090  serle  14106  expcl2lem  14122  expnegz  14145  expaddzlem  14154  expaddz  14155  expmulz  14157  sq11  14180  ltexp2a  14215  expmordi  14216  leexp2a  14221  leexp2r  14223  exple1  14226  expubnd  14227  bernneq2  14279  expmulnbnd  14284  discr1  14288  discr  14289  faclbnd  14339  bcp1nk  14366  cshweqrep  14877  sgnsub  15162  sgnmul  15163  remim  15187  reim0b  15189  rereb  15190  mulre  15191  cjreb  15193  recj  15194  reneg  15195  readd  15196  resub  15197  remullem  15198  remul2  15200  rediv  15201  imcj  15202  imneg  15203  imadd  15204  imsub  15205  immul2  15207  imdiv  15208  cjcj  15210  cjadd  15211  ipcnval  15213  cjmulval  15215  cjneg  15217  imval2  15221  cjreim2  15231  01sqrexlem5  15316  01sqrexlem7  15318  resqrtthlem  15324  remsqsqrt  15326  sqrtmul  15329  sqrtdiv  15335  sqrtneg  15337  sqrtmsq  15340  absdiv  15365  absid  15366  absexp  15374  absexpz  15375  absimle  15379  abslt  15385  absle  15386  abssubne0  15387  releabs  15392  recval  15393  abstri  15401  abs2difabs  15405  abs1m  15406  abslem2  15410  absrdbnd  15412  sqreulem  15430  sqreu  15431  amgm2  15440  icodiamlt  15508  bhmafibid1  15538  bhmafibid2  15539  lo1bddrp  15595  o1lo1  15607  rlimrecl  15650  rlimge0  15651  climrecl  15653  climge0  15654  climabs0  15655  reccn2  15667  o1rlimmul  15689  lo1mul2  15699  lo1sub  15701  climle  15710  climsqz  15711  climsqz2  15712  rlimsqz  15720  rlimsqz2  15721  climlec2  15729  isercolllem1  15735  climsup  15740  caucvgrlem  15743  caurcvgr  15744  caucvgrlem2  15745  iseraltlem1  15752  iseraltlem2  15753  iseraltlem3  15754  iseralt  15755  isumrecl  15834  isumge0  15835  fsumless  15866  fsumge1  15867  fsum00  15868  fsumle  15869  fsumlt  15870  fsumabs  15871  o1fsum  15883  seqabs  15884  cvgcmp  15886  cvgcmpce  15888  abscvgcvg  15889  indsum  15898  indsumhash  15899  isumrpcl  15915  isumle  15916  isumless  15917  isumsup  15919  climcndslem1  15921  climcndslem2  15922  climcnds  15923  flo1  15926  supcvg  15928  trireciplem  15934  trirecip  15935  explecnv  15937  geo2sum  15945  geo2lim  15947  geomulcvg  15948  cvgrat  15955  mertenslem1  15956  mertenslem2  15957  fprodabs  16046  fprodle  16068  iprodrecl  16074  bpolydiflem  16125  bpoly4  16130  efcllem  16148  ege2le3  16161  efaddlem  16164  efgt0  16176  eftlub  16182  effsumlt  16184  eflt  16190  eflegeo  16194  resin4p  16211  recos4p  16212  retanhcl  16232  tanhlt1  16233  efeul  16235  ef01bndlem  16257  sin01bnd  16258  cos01bnd  16259  sin01gt0  16263  cos01gt0  16264  sin02gt0  16265  absefi  16269  absef  16270  absefib  16271  efieq1re  16272  eirrlem  16277  rpnnen2lem5  16291  rpnnen2lem8  16294  rpnnen2lem9  16295  rpnnen2lem11  16297  rpnnen2lem12  16298  moddvds  16338  odd2np1  16416  divalglem5  16472  bitsp1o  16508  bitsfzo  16510  bitscmp  16513  sadcaddlem  16532  nn0seqcvgd  16645  sqnprm  16778  isprm5  16783  nonsq  16835  eulerthlem2  16858  prmdiveq  16862  odzdvds  16872  vfermltlALT  16879  pythagtriplem14  16905  pcid  16950  fldivp1  16974  pcfac  16976  pockthlem  16982  prmreclem3  16995  prmreclem4  16996  prmreclem5  16997  prmrec  16999  4sqlem5  17019  4sqlem10  17024  mul4sqlem  17030  4sqlem15  17036  4sqlem16  17037  mulgneg  19181  ghmmulg  19321  odmodnn0  19633  mndodconglem  19634  pgpfaclem2  20177  isabvd  20944  abv1z  20956  abvneg  20958  abvrec  20960  abvdiv  20961  abvdom  20962  rege0subm  21602  cnsubrg  21606  gzrngunitlem  21611  regsumfsum  21614  prmirredlem  21651  remulg  21786  rzgrp  21802  bl2in  24586  blhalf  24591  blssps  24610  blss  24611  methaus  24706  nrmmetd  24760  nm2dif  24811  nminvr  24855  nmdvr  24856  nlmmul0or  24869  nrginvrcnlem  24877  nmolb2d  24904  nmoi2  24916  nmoleub  24917  nmo0  24921  nmoeq0  24922  nmoco  24923  nmotri  24925  nmoid  24928  blcvx  24984  xrsxmet  24996  recld2  25001  reconnlem2  25014  opnreen  25018  metdstri  25038  metnrmlem3  25048  icchmeo  25129  icopnfcnv  25130  icopnfhmeo  25131  iccpnfhmeo  25133  xrhmeo  25134  icccvx  25138  cnheiborlem  25142  evth  25147  lebnumii  25154  pcoass  25212  pcorevlem  25214  pcorev2  25216  pi1xfrcnv  25245  nmoleub2lem  25302  nmoleub2lem3  25303  nmoleub3  25307  ncvsm1  25342  ncvspi  25344  ncvs1  25345  cphsqrtcl2  25374  ipcau2  25422  tcphcphlem1  25423  tcphcphlem2  25424  tcphcph  25425  cphipval2  25429  cphipval  25431  iscau3  25466  rrxnm  25579  rrxcph  25580  csbren  25587  trirn  25588  rrxmval  25593  rrxmetlem  25595  rrxmet  25596  rrxdstprj1  25597  ehl1eudis  25608  ehl2eudis  25610  minveclem2  25614  minveclem3b  25616  minveclem4  25620  minveclem6  25622  minveclem7  25623  pjthlem1  25625  ivthlem2  25640  ivthlem3  25641  ivth2  25643  ovolfsval  25658  ovollb2lem  25676  ovolctb  25678  ovolunlem1a  25684  ovolunnul  25688  ovolfiniun  25689  ovoliunlem1  25690  ovoliun2  25694  shft2rab  25696  ovolshftlem1  25697  sca2rab  25700  ovolscalem1  25701  ovolsca  25703  ovolicc1  25704  ovolicc2lem4  25708  ovolicopnf  25712  cmmbl  25722  nulmbl  25723  nulmbl2  25724  unmbl  25725  volinun  25734  volfiniun  25735  voliunlem1  25738  voliunlem3  25740  ioombl1lem3  25748  ioombl1lem4  25749  ovolioo  25756  ioorcl2  25760  uniioovol  25767  uniioombllem3  25773  uniioombllem4  25774  uniioombllem5  25775  uniioombllem6  25776  dyadovol  25781  dyaddisjlem  25783  opnmbllem  25789  vitalilem1  25796  vitalilem2  25797  vitalilem3  25798  vitalilem4  25799  ismbf  25816  mbfmulc2lem  25835  mbfmulc2re  25836  mbfmulc2  25851  mbfinf  25853  itg1val2  25872  itg11  25879  i1fmullem  25882  i1fadd  25883  itg1addlem4  25887  itg1addlem5  25888  i1fmulclem  25890  i1fmulc  25891  itg1mulc  25892  itg1sub  25897  itg10a  25898  itg1ge0a  25899  itg1climres  25902  mbfi1fseqlem3  25905  mbfi1fseqlem4  25906  mbfi1fseqlem5  25907  mbfi1fseqlem6  25908  mbfi1flimlem  25910  mbfmullem2  25912  itg2const  25928  itg2const2  25929  itg2mulclem  25934  itg2mulc  25935  itg2splitlem  25936  itg2split  25937  itg2monolem1  25938  itg2monolem3  25940  itg2addlem  25946  itgcl  25972  itgcnlem  25978  itgrevallem1  25983  itgposval  25984  iblneg  25991  itgneg  25992  i1fibl  25996  itgitg1  25997  itgconst  26007  ibladd  26009  itgaddlem2  26012  iblabslem  26016  iblabs  26017  iblabsr  26018  iblmulc2  26019  itgmulc2lem2  26021  itgmulc2  26022  itgabs  26023  itgsplit  26024  bddmulibl  26027  bddiblnc  26030  dvcjbr  26137  dvfre  26139  dvexp3  26166  dveflem  26167  dvferm1lem  26172  dvferm2lem  26174  rolle  26178  cmvth  26179  mvth  26180  dvlip  26181  dvlipcn  26182  c1liplem1  26184  c1lip1  26185  dveq0  26188  dv11cn  26189  dvlt0  26193  dvle  26195  dvivthlem1  26196  dvivth  26198  lhop1lem  26201  lhop1  26202  lhop2  26203  lhop  26204  dvcvx  26208  dvfsumle  26209  dvfsumge  26210  dvfsumabs  26211  dvfsumlem1  26214  dvfsumlem2  26215  dvfsumlem4  26217  dvfsumrlimge0  26218  dvfsumrlim2  26220  dvfsum2  26222  ftc1a  26225  ftc1lem4  26227  ftc1lem5  26228  itgpowd  26238  plyeq0lem  26396  coemulhi  26440  plyrecj  26467  plyn0mulidp  26471  plydivlem3  26485  aalioulem2  26525  aalioulem3  26526  aalioulem4  26527  aalioulem5  26528  aalioulem6  26529  aaliou  26530  aaliou2  26532  aaliou2b  26533  aaliou3lem3  26536  aaliou3lem7  26541  aaliou3lem9  26542  taylthlem2  26566  ulmcn  26591  ulmdvlem1  26592  mtest  26596  mtestbdd  26597  itgulm  26600  radcnvlem1  26605  radcnvlem2  26606  radcnvlt1  26610  radcnvle  26612  dvradcnv  26613  pserulm  26614  abelthlem2  26624  abelthlem5  26627  abelthlem7  26630  abelth2  26634  reeff1olem  26638  efcvx  26641  pilem2  26644  pilem3  26645  sincosq2sgn  26693  sincosq3sgn  26694  sincosq4sgn  26695  coseq0negpitopi  26697  tanrpcl  26698  tangtx  26699  tanabsge  26700  sinq12gt0  26701  sinq34lt0t  26703  cosq14gt0  26704  cosq14ge0  26705  pige3ALT  26714  coskpi  26717  cos02pilt1  26720  cosordlem  26724  sinord  26728  tanord1  26731  tanord  26732  tanregt0  26733  efif1olem2  26737  efif1olem4  26739  eff1olem  26742  logrnaddcl  26768  logneg  26782  lognegb  26784  reexplog  26789  relogexp  26790  logfac  26795  efiarg  26801  cosargd  26802  cosarg0d  26803  argregt0  26804  argrege0  26805  argimgt0  26806  logneg2  26809  logmul2  26810  logdiv2  26811  abslogle  26812  tanarg  26813  logdivlti  26814  divlogrlim  26829  logcnlem2  26837  logcnlem3  26838  logcnlem4  26839  logcn  26841  logf1o2  26844  advlog  26848  advlogexp  26849  efopnlem1  26850  logtayllem  26853  logtayl  26854  logccv  26857  logcxp  26863  mulcxp  26879  divcxp  26881  cxpmul  26882  cxproot  26884  cxpmul2z  26885  abscxp  26886  abscxp2  26887  cxplt  26888  cxplea  26890  cxple2  26891  cxple2a  26893  cxplt3  26894  cxpsqrtlem  26896  cxpsqrt  26897  logsqrt  26898  dvcxp2  26935  cxpcn3lem  26941  resqrtcn  26943  cxpaddlelem  26945  cxpaddle  26946  abscxpbnd  26947  root1id  26948  root1eq1  26949  root1cj  26950  cxpeq  26951  loglesqrt  26955  relogbmul  26971  nnlogbexp  26975  logbrec  26976  cosangneg2d  27001  angrtmuld  27002  ang180lem2  27004  lawcoslem1  27009  lawcos  27010  pythag  27011  isosctrlem1  27012  isosctrlem2  27013  isosctrlem3  27014  ssscongptld  27016  chordthmlem  27026  chordthmlem2  27027  chordthmlem3  27028  chordthmlem4  27029  chordthmlem5  27030  heron  27032  asinsinlem  27085  reasinsin  27090  acosrecl  27097  atancj  27104  atanrecl  27105  atanlogaddlem  27107  atanlogsublem  27109  atanbndlem  27119  atans2  27125  ressatans  27128  atantayl  27131  leibpilem2  27135  leibpi  27136  leibpisum  27137  log2tlbnd  27139  log2ublem2  27141  birthdaylem2  27146  birthdaylem3  27147  cxp2limlem  27169  cxp2lim  27170  cxploglim  27171  cxploglim2  27172  divsqrtsumo1  27177  cvxcl  27178  scvxcvx  27179  jensenlem2  27181  jensen  27182  amgmlem  27183  logdiflbnd  27188  emcllem2  27190  emcllem3  27191  emcllem5  27193  emcllem6  27194  emcllem7  27195  harmonicbnd4  27204  fsumharmonic  27205  zetacvg  27208  lgamgulmlem2  27223  lgamgulmlem3  27224  lgamgulmlem4  27225  lgamgulmlem5  27226  lgamgulmlem6  27227  lgamgulm2  27229  lgambdd  27230  lgamcvg2  27248  gamcvg  27249  gamcvg2lem  27252  regamcl  27254  relgamcl  27255  lgam1  27257  ftalem1  27266  ftalem2  27267  ftalem4  27269  ftalem5  27270  basellem3  27276  basellem4  27277  basellem5  27278  basellem6  27279  basellem7  27280  basellem8  27281  basellem9  27282  efnnfsumcl  27296  chtprm  27346  chpp1  27348  chtdif  27351  efchtdvds  27352  prmorcht  27371  mumullem2  27373  fsumfldivdiaglem  27382  ppiub  27397  chtleppi  27403  chtublem  27404  chtub  27405  pclogsum  27408  vmasum  27409  logfac2  27410  chpval2  27411  chpchtsum  27412  chpub  27413  logfaclbnd  27415  logfacbnd3  27416  logfacrlim  27417  logexprlim  27418  logfacrlim2  27419  mersenne  27420  dchrabs  27453  dchrptlem1  27457  dchrptlem2  27458  bcmax  27471  bcp1ctr  27472  bposlem1  27477  bposlem9  27485  lgsvalmod  27509  lgsdilem  27517  lgsne0  27528  lgsqrlem2  27540  gausslemma2dlem1a  27558  gausslemma2dlem6  27565  lgseisenlem1  27568  lgseisenlem2  27569  lgseisen  27572  lgsquadlem1  27573  lgsquadlem2  27574  mul2sq  27612  2sqlem3  27613  2sqlem8  27619  2sqmod  27629  2sqreulem1  27639  2sqreunnlem1  27642  chebbnd1lem1  27662  chebbnd1lem2  27663  chebbnd1lem3  27664  chtppilimlem1  27666  chtppilimlem2  27667  chtppilim  27668  chto1ub  27669  chto1lb  27671  chpchtlim  27672  chpo1ub  27673  vmadivsum  27675  vmadivsumb  27676  rplogsumlem1  27677  rplogsumlem2  27678  rpvmasumlem  27680  dchrisumlema  27681  dchrisumlem1  27682  dchrisumlem2  27683  dchrisumlem3  27684  dchrmusumlema  27686  dchrmusum2  27687  dchrvmasumlem1  27688  dchrvmasum2lem  27689  dchrvmasum2if  27690  dchrvmasumlem2  27691  dchrvmasumlem3  27692  dchrvmasumiflem1  27694  dchrvmasumiflem2  27695  dchrisum0flblem1  27701  dchrisum0fno1  27704  rpvmasum2  27705  dchrisum0re  27706  dchrisum0lema  27707  dchrisum0lem1b  27708  dchrisum0lem1  27709  dchrisum0lem2a  27710  dchrisum0lem2  27711  dchrisum0lem3  27712  dchrmusumlem  27715  dchrvmasumlem  27716  rpvmasum  27719  rplogsum  27720  dirith2  27721  mudivsum  27723  mulogsumlem  27724  mulogsum  27725  logdivsum  27726  mulog2sumlem1  27727  mulog2sumlem2  27728  mulog2sumlem3  27729  vmalogdivsum2  27731  vmalogdivsum  27732  2vmadivsumlem  27733  logsqvma  27735  logsqvma2  27736  log2sumbnd  27737  selberglem1  27738  selberglem2  27739  selberglem3  27740  selberg  27741  selbergb  27742  selberg2lem  27743  selberg2  27744  selberg2b  27745  chpdifbndlem1  27746  logdivbnd  27749  selberg3lem1  27750  selberg3lem2  27751  selberg3  27752  selberg4lem1  27753  selberg4  27754  pntrmax  27757  pntrsumo1  27758  pntrsumbnd  27759  pntrsumbnd2  27760  selbergr  27761  selberg3r  27762  selberg4r  27763  selberg34r  27764  pntsval2  27769  pntrlog2bndlem1  27770  pntrlog2bndlem2  27771  pntrlog2bndlem3  27772  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  pntrlog2bndlem6a  27775  pntrlog2bndlem6  27776  pntrlog2bnd  27777  pntpbnd1a  27778  pntpbnd1  27779  pntpbnd2  27780  pntibndlem2  27784  pntibndlem3  27785  pntlemb  27790  pntlemg  27791  pntlemh  27792  pntlemn  27793  pntlemr  27795  pntlemj  27796  pntlemf  27798  pntlemk  27799  pntlemo  27800  pntlem3  27802  pntleml  27804  pnt2  27806  pnt  27807  abvcxp  27808  ostth2lem1  27811  qabvexp  27819  padicabv  27823  padicabvcxp  27825  ostth2lem2  27827  ostth2lem3  27828  ostth2lem4  27829  ostth2  27830  ostth3  27831  ttgcontlem1  29263  fveecn  29281  eqeelen  29283  brbtwn2  29284  colinearalglem4  29288  colinearalg  29289  axsegconlem9  29304  axsegconlem10  29305  ax5seglem1  29307  ax5seglem2  29308  ax5seglem3  29310  ax5seglem5  29312  ax5seglem6  29313  ax5seglem9  29316  ax5seg  29317  axbtwnid  29318  axpaschlem  29319  axpasch  29320  axeuclidlem  29341  axcontlem2  29344  axcontlem4  29346  axcontlem7  29349  axcontlem8  29350  elntg2  29364  nrt2irr  30853  nvm1  31046  nvpi  31048  nvz0  31049  nvmtri  31052  nvabs  31053  nvge0  31054  nv1  31056  smcnlem  31078  ipval2lem4  31087  ipval2  31088  4ipval2  31089  ipidsq  31091  dipcj  31095  dip0r  31098  ipz  31100  nmoub3i  31154  nmlno0lem  31174  nmblolbii  31180  blocnilem  31185  cncph  31200  ipasslem4  31215  ipasslem5  31216  ipblnfi  31236  minvecolem2  31256  minvecolem4  31261  minvecolem6  31263  minvecolem7  31264  htthlem  31298  normpyc  31527  hhph  31559  bcs2  31563  norm1  31630  norm1exi  31631  pjhthlem1  31772  eigvalcl  32342  eighmorth  32345  nmlnop0iALT  32376  nmbdoplbi  32405  nmcexi  32407  nmcoplbi  32409  nmbdfnlbi  32430  nmcfnlbi  32433  riesz4i  32444  cnlnadjlem2  32449  cnlnadjlem7  32454  nmopcoi  32476  nmopcoadji  32482  branmfn  32486  leopnmid  32519  opsqrlem1  32521  hst1h  32608  hstle  32611  hstoh  32613  sto2i  32618  stadd3i  32629  strlem1  32631  golem1  32652  stcltrlem1  32657  cdj1i  32814  cdj3lem1  32815  cdj3lem3b  32821  cdj3i  32822  sgnval2  33109  re0cj  33117  receqid  33118  pythagreim  33119  lt2addrd  33124  le2halvesd  33130  fzsplit3  33167  bcm1n  33169  expgt0b  33190  fsumiunle  33202  nexple  33206  expevenpos  33208  oexpled  33209  wrdt2ind  33298  psgnfzto1stlem  33443  ccfldsrarelvec  34084  ccfldextdgrr  34085  constrrtll  34144  constrrtlc1  34145  constrrtlc2  34146  constrconj  34158  nn0constr  34174  constrnegcl  34176  constrdircl  34178  iconstr  34179  constrremulcl  34180  constrrecl  34182  constrimcl  34183  constrmulcl  34184  constrreinvcl  34185  constrinvcl  34186  constrresqrtcl  34190  constrabscl  34191  constrsqrtcl  34192  cos9thpiminplylem1  34195  sqsscirc1  34321  sqsscirc2  34322  cnre2csqima  34324  rmulccn  34341  xrge0iifcnv  34346  xrge0iifhom  34350  zrhnm  34380  rezh  34382  esumpcvgval  34491  esumcvgsum  34501  dya2ub  34684  dya2icoseg  34691  omssubadd  34714  eulerpartlemgc  34776  ballotlemsi  34929  signsply0  34962  signsvtp  34994  signsvtn  34995  signsvfpn  34996  signsvfnn  34997  divsqrtid  35005  reprgt  35032  reprinfz1  35033  breprexplemc  35043  circlemethhgt  35054  hgt750lemd  35059  hgt750lemf  35064  hgt750lemg  35065  hgt750lemb  35067  hgt750lema  35068  hgt750leme  35069  tgoldbachgtde  35071  subfacval2  35692  subfaclim  35693  subfacval3  35694  resconn  35751  sinccvglem  36177  circum  36179  climlec3  36239  faclimlem1  36248  faclimlem2  36249  faclimlem3  36250  faclim  36251  iprodfac  36252  faclim2  36253  dnicld1  37094  dnizeq0  37097  dnizphlfeqhlf  37098  dnibndlem2  37101  dnibndlem3  37102  dnibndlem5  37104  dnibndlem6  37105  dnibndlem7  37106  dnibndlem8  37107  dnibndlem9  37108  dnibndlem10  37109  dnibndlem11  37110  dnibndlem12  37111  dnibndlem13  37112  dnibnd  37113  dnicn  37114  knoppcnlem4  37118  knoppcnlem5  37119  knoppcnlem6  37120  knoppcnlem8  37122  knoppcnlem9  37123  knoppcnlem10  37124  knoppcnlem11  37125  unblimceq0  37129  unbdqndv2lem1  37131  unbdqndv2lem2  37132  knoppndvlem1  37134  knoppndvlem6  37139  knoppndvlem8  37141  knoppndvlem9  37142  knoppndvlem10  37143  knoppndvlem11  37144  knoppndvlem12  37145  knoppndvlem14  37147  knoppndvlem15  37148  knoppndvlem17  37150  knoppndvlem18  37151  knoppndvlem19  37152  knoppndvlem20  37153  knoppndvlem21  37154  irrdifflemf  38002  irrdiff  38003  qdiff  38004  ltflcei  38292  sin2h  38294  cos2h  38295  tan2h  38296  poimirlem29  38333  opnmbllem0  38340  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  mbfposadd  38351  itg2addnclem  38355  itg2addnclem2  38356  itg2addnclem3  38357  itg2addnc  38358  itg2gt0cn  38359  ibladdnc  38361  itgaddnclem2  38363  iblabsnclem  38367  iblabsnc  38368  iblmulc2nc  38369  itgmulc2nclem2  38371  itgmulc2nc  38372  itgabsnc  38373  ftc1cnnclem  38375  ftc1cnnc  38376  ftc1anclem1  38377  ftc1anclem2  38378  ftc1anclem3  38379  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  areacirclem1  38392  areacirclem5  38396  areacirc  38397  mettrifi  38441  lmclim2  38442  geomcau  38443  isbnd3  38468  ssbnd  38472  cntotbnd  38480  bfplem1  38506  bfplem2  38507  bfp  38508  rrnmet  38513  rrndstprj1  38514  rrndstprj2  38515  rrncmslem  38516  rrnequiv  38519  rrntotbnd  38520  ismrer1  38522  lcmineqlem18  42846  lcmineqlem19  42847  lcmineqlem20  42848  lcmineqlem21  42849  lcmineqlem22  42850  3lexlogpow5ineq2  42855  3lexlogpow2ineq1  42858  3lexlogpow2ineq2  42859  3lexlogpow5ineq5  42860  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1p4  42871  dvle2  42872  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p3  42878  aks4d1p5  42880  aks4d1p6  42881  aks4d1p7d1  42882  aks4d1p7  42883  aks4d1p8d2  42885  aks4d1p8  42887  posbezout  42900  aks6d1c1  42916  hashscontpow1  42921  aks6d1c3  42923  aks6d1c4  42924  aks6d1c2lem4  42927  aks6d1c2  42930  aks6d1c5lem3  42937  aks6d1c5lem2  42938  2np3bcnp1  42944  sticksstones6  42951  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem4  42973  bcled  42978  bcle2d  42979  aks6d1c7lem1  42980  aks6d1c7lem2  42981  remulcan2d  43057  readdridaddlidd  43058  readdrcl2d  43067  sumcubes  43107  oexpreposd  43116  expeqidd  43119  rxp112d  43139  rxp11d  43142  readvrec2  43155  readvrec  43156  resuppsinopn  43157  readvcot  43158  resubeulem1  43169  resubeulem2  43170  readdsub  43178  resubsub4  43183  resubidaddlidlem  43188  resubdi  43190  sn-addlid  43198  remul02  43199  remul01  43201  renegneg  43206  readdcan2  43207  renegid2  43208  sn-it0e0  43210  sn-negex12  43211  reixi  43217  remulinvcom  43227  remullid  43228  remulcand  43233  rediveud  43237  redivrec2d  43254  rediv23d  43255  redivdird  43256  sn-0tie0  43258  zaddcomlem  43270  zaddcom  43271  renegmulnnass  43272  mulgt0b1d  43279  mulgt0b2d  43285  mullt0b1d  43290  sn-itrere  43295  sn-retire  43296  cnreeu  43297  frlmvscadiccat  43313  abvexp  43333  dffltz  43399  fltnltalem  43427  fltnlta  43428  negexpidd  43446  3cubeslem1  43448  3cubeslem2  43449  3cubeslem4  43453  eldioph2lem1  43524  lzenom  43534  rencldnfilem  43580  irrapxlem1  43582  irrapxlem2  43583  irrapxlem3  43584  irrapxlem4  43585  irrapxlem5  43586  pellexlem2  43590  pellexlem6  43594  pell1234qrreccl  43614  pell14qrgt0  43619  pell14qrdivcl  43625  pell14qrexpclnn0  43626  pell14qrexpcl  43627  pell14qrdich  43629  pell1qrgaplem  43633  pellfundex  43646  reglogmul  43653  reglogexp  43654  reglogbas  43655  reglog1  43656  pellfund14  43658  rmspecfund  43669  monotoddzzfi  43702  jm2.24nn  43719  jm2.17a  43720  jm2.17b  43721  jm2.17c  43722  jm2.24  43723  acongrep  43740  fzmaxdif  43741  acongeq  43743  modabsdifz  43746  jm2.19lem4  43752  jm2.19  43753  jm2.26lem3  43761  jm3.1lem1  43777  jm3.1lem2  43778  areaquad  43976  sqrtcvallem4  44398  sqrtcval  44400  sqrtcval2  44401  absmulrposd  44918  extoimad  44923  imo72b2lem0  44924  imo72b2lem1  44928  imo72b2  44931  int-addcomd  44932  int-addassocd  44933  int-addsimpd  44934  int-mulcomd  44935  int-mulassocd  44936  int-mulsimpd  44937  int-leftdistd  44938  int-rightdistd  44939  int-sqdefd  44940  int-mul11d  44941  int-mul12d  44942  int-add01d  44943  int-add02d  44944  int-sqgeq0d  44945  int-eqmvtd  44948  cvgdvgrat  45056  radcnvrat  45057  hashnzfzclim  45065  dvconstbi  45077  binomcxplemnn0  45092  binomcxplemnotnn0  45099  isosctrlem1ALT  45675  sineq0ALT  45678  infnsuprnmpt  45998  oddfl  46030  dstregt0  46034  zltlesub  46037  lt3addmuld  46053  fperiodmullem  46055  fperiodmul  46056  lt4addmuld  46058  fzdifsuc2  46062  supxrgere  46082  supxrgelem  46086  suplesup  46088  supsubc  46102  xralrple2  46103  abslt2sqd  46109  xralrple3  46122  reclt0d  46135  ltmulneg  46140  rexabslelem  46165  supminfrnmpt  46192  leneg2d  46195  leneg3d  46204  supminfxr  46211  absimnre  46223  absimlere  46226  iooabslt  46248  iccshift  46267  iooshift  46271  sqrlearg  46302  fmul01  46329  fmul01lt1lem1  46333  fmul01lt1lem2  46334  fprodabs2  46344  climinf  46355  limcrecl  46378  lptre2pt  46387  limcleqr  46391  0ellimcdiv  46396  limclner  46398  climleltrp  46423  climinf2mpt  46461  climinf3  46463  climxrre  46497  climliminflimsupd  46548  liminfltlem  46551  liminflimsupclim  46554  cnrefiisplem  46576  sinaover2ne0  46615  cncfperiod  46626  ioccncflimc  46632  cncficcgt0  46635  icocncflimc  46636  cncfshiftioo  46639  cncfiooicc  46641  fperdvper  46666  dvbdfbdioolem1  46675  dvbdfbdioolem2  46676  dvbdfbdioo  46677  ioodvbdlimc1lem1  46678  ioodvbdlimc1lem2  46679  ioodvbdlimc1  46680  ioodvbdlimc2lem  46681  ioodvbdlimc2  46682  dvnmul  46690  dvnprodlem1  46693  dvnprodlem2  46694  itgcoscmulx  46716  volioc  46719  itgsincmulx  46721  itgiccshift  46727  itgperiod  46728  itgsbtaddcnst  46729  volico  46730  voliooico  46739  voliccico  46746  stoweidlem7  46754  stoweidlem11  46758  stoweidlem13  46760  stoweidlem17  46764  stoweidlem19  46766  stoweidlem20  46767  stoweidlem21  46768  stoweidlem22  46769  stoweidlem23  46770  stoweidlem24  46771  stoweidlem26  46773  stoweidlem32  46779  stoweidlem36  46783  stoweidlem44  46791  stoweidlem47  46794  wallispilem3  46814  wallispi2lem1  46818  stirlinglem1  46821  stirlinglem5  46825  stirlinglem11  46831  stirlinglem12  46832  stirlinglem14  46834  dirkerval2  46841  dirkerre  46842  dirkertrigeqlem2  46846  dirkertrigeq  46848  dirkeritg  46849  dirkercncflem1  46850  dirkercncflem2  46851  dirkercncflem4  46853  fourierdlem4  46858  fourierdlem6  46860  fourierdlem7  46861  fourierdlem13  46867  fourierdlem14  46868  fourierdlem16  46870  fourierdlem18  46872  fourierdlem19  46873  fourierdlem21  46875  fourierdlem22  46876  fourierdlem24  46878  fourierdlem26  46880  fourierdlem28  46882  fourierdlem30  46884  fourierdlem35  46889  fourierdlem39  46893  fourierdlem40  46894  fourierdlem41  46895  fourierdlem42  46896  fourierdlem43  46897  fourierdlem44  46898  fourierdlem47  46900  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem51  46904  fourierdlem53  46906  fourierdlem56  46909  fourierdlem57  46910  fourierdlem58  46911  fourierdlem59  46912  fourierdlem60  46913  fourierdlem61  46914  fourierdlem62  46915  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem66  46919  fourierdlem68  46921  fourierdlem70  46923  fourierdlem71  46924  fourierdlem72  46925  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem77  46930  fourierdlem78  46931  fourierdlem79  46932  fourierdlem80  46933  fourierdlem81  46934  fourierdlem83  46936  fourierdlem84  46937  fourierdlem85  46938  fourierdlem87  46940  fourierdlem88  46941  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem92  46945  fourierdlem93  46946  fourierdlem95  46948  fourierdlem97  46950  fourierdlem101  46954  fourierdlem103  46956  fourierdlem104  46957  fourierdlem107  46960  fourierdlem109  46962  fourierdlem111  46964  fourierdlem112  46965  fouriercnp  46973  sqwvfoura  46975  sqwvfourb  46976  fouriersw  46978  etransclem14  46995  etransclem18  46999  etransclem23  47004  etransclem24  47005  etransclem27  47008  etransclem46  47027  etransclem48  47029  qndenserrnbllem  47041  ioorrnopnlem  47051  sge0tsms  47127  sge0cl  47128  sge0split  47156  sge0iunmptlemfi  47160  sge0rpcpnf  47168  sge0isum  47174  sge0ad2en  47178  sge0xaddlem1  47180  sge0xaddlem2  47181  sge0gtfsumgt  47190  sge0seq  47193  meadif  47226  meaiininclem  47233  carageniuncllem1  47268  carageniuncllem2  47269  hoicvr  47295  hoicvrrex  47303  ovnsubaddlem1  47317  hsphoidmvle2  47332  hsphoidmvle  47333  hoidmvval0  47334  hoiprodp1  47335  hoidmv1lelem1  47338  hoidmv1lelem2  47339  hoidmv1le  47341  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem3  47344  hoiqssbllem2  47370  hspmbllem1  47373  ovolval2lem  47390  ovolval3  47394  ovolval5lem1  47399  ovnovollem1  47403  ovnovollem2  47404  vonioolem1  47427  vonioo  47429  vonicclem1  47430  vonicc  47432  smfaddlem1  47510  smflimlem4  47521  smfmullem1  47538  smfmullem2  47539  smfmullem3  47540  smfdiv  47544  smfneg  47550  sigaras  47602  sigarms  47603  sigarls  47604  sigarexp  47606  sigarperm  47607  sigarimcd  47609  sigarcol  47611  sharhght  47612  cevathlem2  47615  readdcnnred  48073  resubcnnred  48074  cndivrenred  48076  flmrecm1  48113  fldivmod  48114  ceildivmod  48115  m1mod0mod1  48130  m1modmmod  48134  difmodm1lt  48135  requad01  48419  requad1  48420  requad2  48421  fpprwppr  48537  bgoldbtbndlem2  48604  gpgvtxedg1  48862  ltsubaddb  49327  ltsubsubb  49328  ltsubadd2b  49329  flsubz  49335  logblt1b  49377  dignn0fr  49414  dignn0flhalflem1  49428  dignn0flhalflem2  49429  nn0sumshdiglemA  49432  affinecomb1  49515  affinecomb2  49516  resum2sqorgt0  49522  rrx2pnedifcoorneor  49529  rrx2pnedifcoorneorr  49530  ehl2eudisval0  49538  eenglngeehlnmlem1  49550  eenglngeehlnmlem2  49551  rrx2vlinest  49554  rrx2linest  49555  rrx2linest2  49557  2sphere0  49563  line2ylem  49564  line2  49565  line2xlem  49566  line2x  49567  line2y  49568  itscnhlc0yqe  49572  itschlc0yqe  49573  itsclc0yqsol  49577  itscnhlc0xyqsol  49578  itschlc0xyqsol1  49579  itschlc0xyqsol  49580  itsclc0xyqsolr  49582  itsclinecirc0b  49587  itsclquadb  49589  itsclquadeu  49590  2itscplem1  49591  2itscplem2  49592  2itscplem3  49593  2itscp  49594  itscnhlinecirc02plem1  49595  itscnhlinecirc02plem2  49596  itscnhlinecirc02p  49598  inlinecirc02plem  49599  inlinecirc02p  49600  crosspalti  50681  crossp3i  50682  amgmwlem  50683  amgmlemALT  50684