Theorem recnd 9947

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  00id  10090  mul02lem1  10091  addid1  10095  cnegex  10096  ltadd1  10374  leadd2  10376  ltsubadd  10377  ltsubadd2  10378  lesubadd  10379  lesubadd2  10380  lesub1  10401  lesub2  10402  ltnegcon1  10408  ltnegcon2  10409  add20  10419  subge0  10420  suble0  10421  lesub0  10424  mulge0  10425  eqord2  10438  lesub3d  10524  possumd  10531  sublt0d  10532  rereccl  10622  redivcl  10623  recgt0  10746  prodgt0  10747  prodge0  10749  ltmul1a  10751  ltdiv1  10766  ltmuldiv  10775  ltrec  10784  recp1lt1  10800  recreclt  10801  ledivp1  10804  supadd  10868  infrenegsup  10883  rimul  10888  cru  10889  avglt1  11147  avglt2  11148  lt2addmuld  11159  div4p1lem1div2  11164  nn0cnd  11230  zcn  11259  zeo  11339  zcnd  11359  eluzmn  11570  eluzelcn  11575  cnref1o  11703  rpcn  11717  rpcnd  11750  ltaddrp2d  11782  mul2lt0rlt0  11808  mul2lt0rgt0  11809  mul2lt0llt0  11810  mul2lt0lgt0  11811  mul2lt0bi  11812  qbtwnre  11904  xralrple  11910  xpncan  11953  xmulcom  11968  xmulneg1  11971  xlemul1  11992  icoshftf1o  12166  lincmb01cmp  12186  iccf1o  12187  divfl0  12487  fladdz  12488  flzadd  12489  flhalf  12493  ceim1l  12508  intfracq  12520  fldiv  12521  modvalr  12533  flpmodeq  12535  mod0  12537  modlt  12541  moddiffl  12543  modfrac  12545  flmod  12546  intfrac  12547  modmulnn  12550  modvalp1  12551  modid  12557  modcyc  12567  modadd1  12569  modaddabs  12570  modmuladdnn0  12576  negmod  12577  modadd2mod  12582  modnegd  12587  modadd12d  12588  modsub12d  12589  modmulmodr  12598  modaddmulmod  12599  moddi  12600  modsubdir  12601  modeqmodmin  12602  modirr  12603  addmodlteq  12607  seqf1olem1  12702  serle  12718  expcl2lem  12734  expnegz  12756  expaddzlem  12765  expaddz  12766  expmulz  12768  ltexp2a  12774  leexp2a  12778  leexp2r  12780  exple1  12782  expubnd  12783  sq11  12798  bernneq2  12853  expmulnbnd  12858  discr1  12862  discr  12863  faclbnd  12939  bcp1nk  12966  cshweqrep  13418  remim  13705  reim0b  13707  rereb  13708  mulre  13709  cjreb  13711  recj  13712  reneg  13713  readd  13714  resub  13715  remullem  13716  remul2  13718  rediv  13719  imcj  13720  imneg  13721  imadd  13722  imsub  13723  immul2  13725  imdiv  13726  cjcj  13728  cjadd  13729  ipcnval  13731  cjmulval  13733  cjneg  13735  imval2  13739  cjreim2  13749  sqr0lem  13829  sqrlem5  13835  sqrlem7  13837  resqrtthlem  13843  remsqsqrt  13845  sqrtmul  13848  sqrtdiv  13854  sqrtneg  13856  sqrtmsq  13859  absdiv  13883  absid  13884  absexp  13892  absexpz  13893  absimle  13897  abslt  13902  absle  13903  abssubne0  13904  releabs  13909  recval  13910  abstri  13918  abs2difabs  13922  abs1m  13923  abslem2  13927  absrdbnd  13929  sqreulem  13947  sqreu  13948  amgm2  13957  icodiamlt  14022  lo1bddrp  14104  o1lo1  14116  rlimrecl  14159  rlimge0  14160  climrecl  14162  climge0  14163  climabs0  14164  reccn2  14175  o1rlimmul  14197  lo1mul2  14207  lo1sub  14209  climle  14218  climsqz  14219  climsqz2  14220  rlimsqz  14228  rlimsqz2  14229  climlec2  14237  isercolllem1  14243  climsup  14248  caucvgrlem  14251  caurcvgr  14252  caucvgrlem2  14253  iseraltlem1  14260  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  isumrecl  14338  isumge0  14339  fsumless  14369  fsumge1  14370  fsum00  14371  fsumle  14372  fsumlt  14373  fsumabs  14374  o1fsum  14386  seqabs  14387  cvgcmp  14389  cvgcmpce  14391  abscvgcvg  14392  isumrpcl  14414  isumle  14415  isumless  14416  isumsup  14418  climcndslem1  14420  climcndslem2  14421  climcnds  14422  flo1  14425  supcvg  14427  trireciplem  14433  trirecip  14434  explecnv  14436  geo2sum  14443  geo2lim  14445  geomulcvg  14446  cvgrat  14454  mertenslem1  14455  mertenslem2  14456  fprodabs  14543  fprodle  14566  iprodrecl  14572  bpolydiflem  14624  bpoly4  14629  efcllem  14647  ege2le3  14659  efaddlem  14662  efgt0  14672  eftlub  14678  effsumlt  14680  eflt  14686  eflegeo  14690  resin4p  14707  recos4p  14708  retanhcl  14728  tanhlt1  14729  efeul  14731  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  absefi  14765  absef  14766  absefib  14767  efieq1re  14768  eirrlem  14771  rpnnen2lem5  14786  rpnnen2lem8  14789  rpnnen2lem9  14790  rpnnen2lem11  14792  rpnnen2lem12  14793  moddvds  14829  odd2np1  14903  divalglem5  14958  bitsp1o  14993  bitsfzo  14995  bitscmp  14998  sadcaddlem  15017  nn0seqcvgd  15121  sqnprm  15252  isprm5  15257  nonsq  15305  eulerthlem2  15325  prmdiveq  15329  odzdvds  15338  vfermltlALT  15345  pythagtriplem14  15371  pcid  15415  fldivp1  15439  pcfac  15441  pockthlem  15447  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  prmrec  15464  4sqlem5  15484  4sqlem10  15489  mul4sqlem  15495  4sqlem15  15501  4sqlem16  15502  mulgneg  17383  ghmmulg  17495  odmodnn0  17782  mndodconglem  17783  pgpfaclem2  18304  isabvd  18643  abv1z  18655  abvneg  18657  abvrec  18659  abvdiv  18660  abvdom  18661  rege0subm  19621  cnsubrg  19625  gzrngunitlem  19630  regsumfsum  19633  prmirredlem  19660  remulg  19772  regsumsupp  19787  bl2in  22015  blhalf  22020  blssps  22039  blss  22040  methaus  22135  nrmmetd  22189  nm2dif  22239  nminvr  22283  nmdvr  22284  nlmmul0or  22297  nrginvrcnlem  22305  nmolb2d  22332  nmoi2  22344  nmoleub  22345  nmo0  22349  nmoeq0  22350  nmoco  22351  nmotri  22353  nmoid  22356  blcvx  22409  xrsxmet  22420  recld2  22425  reconnlem2  22438  opnreen  22442  metdstri  22462  metnrmlem3  22472  icchmeo  22548  icopnfcnv  22549  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  icccvx  22557  cnheiborlem  22561  evth  22566  lebnumii  22573  pcoass  22632  pcorevlem  22634  pcorev2  22636  pi1xfrcnv  22665  nmoleub2lem  22722  nmoleub2lem3  22723  nmoleub3  22727  ncvsm1  22762  ncvspi  22764  ncvs1  22765  cphsqrtcl2  22794  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  tchcph  22844  cphipval2  22848  cphipval  22850  iscau3  22884  rrxnm  22987  rrxcph  22988  csbren  22990  trirn  22991  rrxmval  22996  rrxmetlem  22998  rrxmet  22999  rrxdstprj1  23000  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  minveclem7  23014  pjthlem1  23016  ivthlem2  23028  ivthlem3  23029  ivth2  23031  ovolfsval  23046  ovollb2lem  23063  ovolctb  23065  ovolunlem1a  23071  ovolunnul  23075  ovolfiniun  23076  ovoliunlem1  23077  ovoliun2  23081  shft2rab  23083  ovolshftlem1  23084  sca2rab  23087  ovolscalem1  23088  ovolsca  23090  ovolicc1  23091  ovolicc2lem4  23095  ovolicopnf  23099  cmmbl  23109  nulmbl  23110  nulmbl2  23111  unmbl  23112  volinun  23121  volfiniun  23122  voliunlem1  23125  voliunlem3  23127  ioombl1lem3  23135  ioombl1lem4  23136  ovolioo  23143  ioorcl2  23146  uniioovol  23153  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombllem6  23162  dyadovol  23167  dyaddisjlem  23169  opnmbllem  23175  vitalilem1  23182  vitalilem1OLD  23183  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  ismbf  23203  mbfmulc2lem  23220  mbfmulc2re  23221  mbfmulc2  23236  mbfinf  23238  itg1val2  23257  itg11  23264  i1fmullem  23267  i1fadd  23268  itg1addlem4  23272  itg1addlem5  23273  i1fmulclem  23275  i1fmulc  23276  itg1mulc  23277  itg1sub  23282  itg10a  23283  itg1ge0a  23284  itg1climres  23287  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfmullem2  23297  itg2const  23313  itg2const2  23314  itg2mulclem  23319  itg2mulc  23320  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2monolem3  23325  itg2addlem  23331  itgcl  23356  itgcnlem  23362  itgrevallem1  23367  itgposval  23368  iblneg  23375  itgneg  23376  i1fibl  23380  itgitg1  23381  itgconst  23391  ibladd  23393  itgaddlem2  23396  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2lem2  23405  itgmulc2  23406  itgabs  23407  itgsplit  23408  bddmulibl  23411  dvcjbr  23518  dvfre  23520  dvexp3  23545  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  c1liplem1  23563  c1lip1  23564  dveq0  23567  dv11cn  23568  dvlt0  23572  dvle  23574  dvivthlem1  23575  dvivth  23577  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem4  23596  dvfsumrlimge0  23597  dvfsumrlim2  23599  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  ftc1lem5  23607  plyeq0lem  23770  coemulhi  23814  plyrecj  23839  plydivlem3  23854  aalioulem2  23892  aalioulem3  23893  aalioulem4  23894  aalioulem5  23895  aalioulem6  23896  aaliou  23897  aaliou2  23899  aaliou2b  23900  aaliou3lem3  23903  aaliou3lem7  23908  aaliou3lem9  23909  taylthlem2  23932  ulmcn  23957  ulmdvlem1  23958  mtest  23962  mtestbdd  23963  itgulm  23966  radcnvlem1  23971  radcnvlem2  23972  radcnvlt1  23976  radcnvle  23978  dvradcnv  23979  pserulm  23980  abelthlem2  23990  abelthlem5  23993  abelthlem7  23996  abelth2  24000  reeff1olem  24004  efcvx  24007  pilem2  24010  pilem3  24011  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  coseq0negpitopi  24059  tanrpcl  24060  tangtx  24061  tanabsge  24062  sinq12gt0  24063  sinq34lt0t  24065  cosq14gt0  24066  cosq14ge0  24067  pige3  24073  coskpi  24076  cosordlem  24081  sinord  24084  tanord1  24087  tanord  24088  tanregt0  24089  efif1olem2  24093  efif1olem4  24095  eff1olem  24098  rzgrp  24104  logrnaddcl  24125  logneg  24138  lognegb  24140  reexplog  24145  relogexp  24146  logfac  24151  efiarg  24157  cosargd  24158  cosarg0d  24159  argregt0  24160  argrege0  24161  argimgt0  24162  logneg2  24165  logmul2  24166  logdiv2  24167  abslogle  24168  tanarg  24169  logdivlti  24170  divlogrlim  24181  logcnlem2  24189  logcnlem3  24190  logcnlem4  24191  logcn  24193  logf1o2  24196  advlog  24200  advlogexp  24201  efopnlem1  24202  logtayllem  24205  logtayl  24206  logccv  24209  logcxp  24215  mulcxp  24231  divcxp  24233  cxpmul  24234  cxproot  24236  cxpmul2z  24237  abscxp  24238  abscxp2  24239  cxplt  24240  cxplea  24242  cxple2  24243  cxple2a  24245  cxplt3  24246  cxpsqrtlem  24248  cxpsqrt  24249  logsqrt  24250  dvcxp2  24282  cxpcn3lem  24288  resqrtcn  24290  cxpaddlelem  24292  cxpaddle  24293  abscxpbnd  24294  root1id  24295  root1eq1  24296  root1cj  24297  cxpeq  24298  loglesqrt  24299  relogbmul  24315  nnlogbexp  24319  logbrec  24320  cosangneg2d  24337  angrtmuld  24338  ang180lem2  24340  lawcoslem1  24345  lawcos  24346  pythag  24347  isosctrlem1  24348  isosctrlem2  24349  isosctrlem3  24350  ssscongptld  24352  chordthmlem  24359  chordthmlem2  24360  chordthmlem3  24361  chordthmlem4  24362  chordthmlem5  24363  heron  24365  asinsinlem  24418  reasinsin  24423  acosrecl  24430  atancj  24437  atanrecl  24438  atanlogaddlem  24440  atanlogsublem  24442  atanbndlem  24452  atans2  24458  ressatans  24461  atantayl  24464  leibpilem2  24468  leibpi  24469  leibpisum  24470  log2tlbnd  24472  log2ublem2  24474  birthdaylem2  24479  birthdaylem3  24480  cxp2limlem  24502  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  divsqrtsumo1  24510  cvxcl  24511  scvxcvx  24512  jensenlem2  24514  jensen  24515  amgmlem  24516  logdiflbnd  24521  emcllem2  24523  emcllem3  24524  emcllem5  24526  emcllem6  24527  emcllem7  24528  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgambdd  24563  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  regamcl  24587  relgamcl  24588  lgam1  24590  ftalem1  24599  ftalem2  24600  ftalem4  24602  ftalem5  24603  basellem3  24609  basellem4  24610  basellem5  24611  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  efnnfsumcl  24629  chtprm  24679  chpp1  24681  chtdif  24684  efchtdvds  24685  prmorcht  24704  mumullem2  24706  fsumfldivdiaglem  24715  ppiub  24729  chtleppi  24735  chtublem  24736  chtub  24737  pclogsum  24740  vmasum  24741  logfac2  24742  chpval2  24743  chpchtsum  24744  chpub  24745  logfaclbnd  24747  logfacbnd3  24748  logfacrlim  24749  logexprlim  24750  logfacrlim2  24751  mersenne  24752  dchrabs  24785  dchrptlem1  24789  dchrptlem2  24790  bcmax  24803  bcp1ctr  24804  bposlem1  24809  bposlem9  24817  lgsvalmod  24841  lgsdilem  24849  lgsne0  24860  lgsqrlem2  24872  gausslemma2dlem1a  24890  gausslemma2dlem6  24897  lgseisenlem1  24900  lgseisenlem2  24901  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  mul2sq  24944  2sqlem3  24945  2sqlem8  24951  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chto1ub  24965  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  vmadivsum  24971  vmadivsumb  24972  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlema  24977  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasum2if  24986  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  dchrisum0flblem1  24997  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrmusumlem  25011  dchrvmasumlem  25012  rpvmasum  25015  rplogsum  25016  dirith2  25017  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  logdivsum  25022  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma  25031  logsqvma2  25032  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  selberglem3  25036  selberg  25037  selbergb  25038  selberg2lem  25039  selberg2  25040  selberg2b  25041  chpdifbndlem1  25042  logdivbnd  25045  selberg3lem1  25046  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrmax  25053  pntrsumo1  25054  pntrsumbnd  25055  pntrsumbnd2  25056  selbergr  25057  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntsval2  25065  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6a  25071  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntibndlem3  25081  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemn  25089  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlem3  25098  pntleml  25100  pnt2  25102  pnt  25103  abvcxp  25104  ostth2lem1  25107  qabvexp  25115  padicabv  25119  padicabvcxp  25121  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  ttgcontlem1  25565  fveecn  25582  eqeelen  25584  brbtwn2  25585  colinearalglem4  25589  colinearalg  25590  axsegconlem9  25605  axsegconlem10  25606  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem6  25614  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axpaschlem  25620  axpasch  25621  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  eupap1  26503  nvm1  26904  nvpi  26906  nvz0  26907  nvmtri  26910  nvabs  26911  nvge0  26912  nv1  26914  smcnlem  26936  ipval2lem4  26945  ipval2  26946  4ipval2  26947  ipidsq  26949  dipcj  26953  dip0r  26956  ipz  26958  nmoub3i  27012  nmlno0lem  27032  nmblolbii  27038  blocnilem  27043  cncph  27058  ipasslem4  27073  ipasslem5  27074  ipblnfi  27095  minvecolem2  27115  minvecolem4  27120  minvecolem6  27122  minvecolem7  27123  htthlem  27158  normpyc  27387  hhph  27419  bcs2  27423  norm1  27490  norm1exi  27491  pjhthlem1  27634  eigvalcl  28204  eighmorth  28207  nmlnop0iALT  28238  nmbdoplbi  28267  nmcexi  28269  nmcoplbi  28271  nmbdfnlbi  28292  nmcfnlbi  28295  riesz4i  28306  cnlnadjlem2  28311  cnlnadjlem7  28316  nmopcoi  28338  nmopcoadji  28344  branmfn  28348  leopnmid  28381  opsqrlem1  28383  hst1h  28470  hstle  28473  hstoh  28475  sto2i  28480  stadd3i  28491  strlem1  28493  golem1  28514  stcltrlem1  28519  cdj1i  28676  cdj3lem1  28677  cdj3lem3b  28683  cdj3i  28684  lt2addrd  28903  le2halvesd  28910  fzsplit3  28940  bcm1n  28941  bhmafibid1  28975  bhmafibid2  28976  2sqmod  28979  psgnfzto1stlem  29181  elunitcn  29272  sqsscirc1  29282  sqsscirc2  29283  cnre2csqima  29285  rmulccn  29302  xrge0iifcnv  29307  xrge0iifhom  29311  zrhnm  29341  rezh  29343  nexple  29399  indsum  29412  esumpcvgval  29467  esumcvgsum  29477  dya2ub  29659  dya2icoseg  29666  omssubadd  29689  eulerpartlemgc  29751  ballotlemsi  29903  sgnmul  29931  sgnsub  29933  plymulx0  29950  signsply0  29954  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  subfacval2  30423  subfaclim  30424  subfacval3  30425  rescon  30482  sinccvglem  30820  circum  30822  climlec3  30872  faclimlem1  30882  faclimlem2  30883  faclimlem3  30884  faclim  30885  iprodfac  30886  faclim2  30887  dnicld1  31632  dnizeq0  31635  dnizphlfeqhlf  31636  dnibndlem2  31639  dnibndlem3  31640  dnibndlem5  31642  dnibndlem6  31643  dnibndlem7  31644  dnibndlem8  31645  dnibndlem9  31646  dnibndlem10  31647  dnibndlem11  31648  dnibndlem12  31649  dnibndlem13  31650  dnibnd  31651  dnicn  31652  knoppcnlem4  31656  knoppcnlem5  31657  knoppcnlem6  31658  knoppcnlem8  31660  knoppcnlem9  31661  knoppcnlem10  31662  knoppcnlem11  31663  unblimceq0  31668  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem1  31673  knoppndvlem6  31678  knoppndvlem8  31680  knoppndvlem9  31681  knoppndvlem10  31682  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem20  31692  knoppndvlem21  31693  ltflcei  32567  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem29  32608  opnmbllem0  32615  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  mbfposadd  32627  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ibladdnc  32637  itgaddnclem2  32639  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nclem2  32647  itgmulc2nc  32648  itgabsnc  32649  bddiblnc  32650  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem1  32655  ftc1anclem2  32656  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem1  32670  areacirclem5  32674  areacirc  32675  mettrifi  32723  lmclim2  32724  geomcau  32725  isbnd3  32753  ssbnd  32757  cntotbnd  32765  bfplem1  32791  bfplem2  32792  bfp  32793  rrnmet  32798  rrndstprj1  32799  rrndstprj2  32800  rrncmslem  32801  rrnequiv  32804  rrntotbnd  32805  ismrer1  32807  eldioph2lem1  36341  lzenom  36351  rencldnfilem  36402  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell1234qrreccl  36436  pell14qrgt0  36441  pell14qrdivcl  36447  pell14qrexpclnn0  36448  pell14qrexpcl  36449  pell14qrdich  36451  pell1qrgaplem  36455  pellfundex  36468  reglogmul  36475  reglogexp  36476  reglogbas  36477  reglog1  36478  pellfund14  36480  rmspecsqrtnqOLD  36489  rmspecfund  36492  monotoddzzfi  36525  expmordi  36530  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  jm2.24  36548  acongrep  36565  fzmaxdif  36566  acongeq  36568  modabsdifz  36571  jm2.19lem4  36577  jm2.19  36578  jm2.26lem3  36586  jm3.1lem1  36602  jm3.1lem2  36603  itgpowd  36819  areaquad  36821  absmulrposd  37477  extoimad  37486  imo72b2lem0  37487  imo72b2lem1  37493  imo72b2  37497  int-addcomd  37498  int-addassocd  37499  int-addsimpd  37500  int-mulcomd  37501  int-mulassocd  37502  int-mulsimpd  37503  int-leftdistd  37504  int-rightdistd  37505  int-sqdefd  37506  int-mul11d  37507  int-mul12d  37508  int-add01d  37509  int-add02d  37510  int-sqgeq0d  37511  int-eqmvtd  37514  cvgdvgrat  37534  radcnvrat  37535  hashnzfzclim  37543  dvconstbi  37555  binomcxplemnn0  37570  binomcxplemnotnn0  37577  isosctrlem1ALT  38192  sineq0ALT  38195  oddfl  38430  dstregt0  38434  zltlesub  38438  lt3addmuld  38456  fperiodmullem  38458  fperiodmul  38459  lt4addmuld  38461  fzdifsuc2  38466  supxrgere  38490  supxrgelem  38494  suplesup  38496  supsubc  38510  xralrple2  38511  abslt2sqd  38517  xralrple3  38531  reclt0d  38548  ltmulneg  38556  iooabslt  38568  iccshift  38591  iooshift  38595  sqrlearg  38627  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodabs2  38662  climinf  38673  limcrecl  38696  lptre2pt  38707  limcleqr  38711  0ellimcdiv  38716  limclner  38718  climleltrp  38743  sinaover2ne0  38751  cncfperiod  38764  ioccncflimc  38771  cncficcgt0  38774  icocncflimc  38775  cncfshiftioo  38778  cncfiooicc  38780  fperdvper  38808  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  itgcoscmulx  38861  volioc  38864  itgsincmulx  38866  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  volico  38876  voliooico  38885  voliccico  38892  stoweidlem7  38900  stoweidlem11  38904  stoweidlem13  38906  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem21  38914  stoweidlem22  38915  stoweidlem23  38916  stoweidlem24  38917  stoweidlem26  38919  stoweidlem32  38925  stoweidlem36  38929  stoweidlem44  38937  stoweidlem47  38940  wallispilem3  38960  wallispi2lem1  38964  stirlinglem1  38967  stirlinglem5  38971  stirlinglem11  38977  stirlinglem12  38978  stirlinglem14  38980  dirkerval2  38987  dirkerre  38988  dirkertrigeqlem2  38992  dirkertrigeq  38994  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem6  39006  fourierdlem7  39007  fourierdlem13  39013  fourierdlem14  39014  fourierdlem16  39016  fourierdlem18  39018  fourierdlem19  39019  fourierdlem21  39021  fourierdlem22  39022  fourierdlem24  39024  fourierdlem26  39026  fourierdlem28  39028  fourierdlem30  39030  fourierdlem35  39035  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem43  39043  fourierdlem44  39044  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem53  39052  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem70  39069  fourierdlem71  39070  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem77  39076  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem87  39086  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem109  39108  fourierdlem111  39110  fourierdlem112  39111  fouriercnp  39119  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem14  39141  etransclem18  39145  etransclem23  39150  etransclem24  39151  etransclem27  39154  etransclem46  39173  etransclem48  39175  qndenserrnbllem  39190  ioorrnopnlem  39200  sge0tsms  39273  sge0cl  39274  sge0split  39302  sge0iunmptlemfi  39306  sge0rpcpnf  39314  sge0isum  39320  sge0ad2en  39324  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0gtfsumgt  39336  sge0seq  39339  meadif  39372  meaiininclem  39376  carageniuncllem1  39411  carageniuncllem2  39412  hoicvrrex  39446  ovnsubaddlem1  39460  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvval0  39477  hoiprodp1  39478  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoiqssbllem2  39513  hspmbllem1  39516  ovolval2lem  39533  ovolval3  39537  ovolval5lem1  39542  ovnovollem1  39546  ovnovollem2  39547  vonioolem1  39571  vonioo  39573  vonicclem1  39574  vonicc  39576  smfaddlem1  39649  smflimlem4  39660  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  smfdiv  39682  sigaras  39693  sigarms  39694  sigarls  39695  sigarexp  39697  sigarperm  39698  sigarimcd  39700  sigarcol  39702  sharhght  39703  cevathlem2  39706  m1mod0mod1  39949  bgoldbtbndlem2  40222  ltsubaddb  42098  ltsubsubb  42099  ltsubadd2b  42100  flsubz  42106  fldivmod  42107  m1modmmod  42110  logblt1b  42156  dignn0fr  42193  dignn0flhalflem1  42207  dignn0flhalflem2  42208  nn0sumshdiglemA  42211  amgmwlem  42357  amgmlemALT  42358