Theorem recnd 10363

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

Syntax hints:   → wi 4   ∈ wcel 2157  ℂcc 10229  ℝcr 10230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795  ax-resscn 10288

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794

This theorem is referenced by:  00id  10506  mul02lem1  10507  addid1  10511  cnegex  10512  ltadd1  10790  leadd2  10792  ltsubadd  10793  ltsubadd2  10794  lesubadd  10795  lesubadd2  10796  lesub1  10817  lesub2  10818  ltnegcon1  10824  ltnegcon2  10825  add20  10835  subge0  10836  suble0  10837  lesub0  10840  mulge0  10841  eqord2  10854  lesub3d  10940  possumd  10947  sublt0d  10948  rereccl  11038  redivcl  11039  recgt0  11162  prodgt0  11163  prodge0OLD  11165  ltmul1a  11167  ltdiv1  11182  ltmuldiv  11191  ltrec  11200  recp1lt1  11216  recreclt  11217  ledivp1  11220  supadd  11286  infrenegsup  11301  rimul  11306  cru  11307  avglt1  11557  avglt2  11558  lt2addmuld  11569  div4p1lem1div2  11574  nn0cnd  11639  zcn  11668  zeo  11749  zcnd  11769  eluzmn  11931  eluzelcn  11936  cnref1o  12061  rpcn  12075  rpcnd  12108  ltaddrp2d  12140  mul2lt0rlt0  12166  mul2lt0rgt0  12167  mul2lt0llt0  12168  mul2lt0lgt0  12169  mul2lt0bi  12170  prodge0rd  12171  prodge0ld  12172  qbtwnre  12268  xralrple  12274  xpncan  12319  xmulcom  12334  xmulneg1  12337  xlemul1  12358  icoshftf1o  12536  lincmb01cmp  12558  iccf1o  12559  divfl0  12869  fladdz  12870  flzadd  12871  flhalf  12875  ceim1l  12890  intfracq  12902  fldiv  12903  modvalr  12915  flpmodeq  12917  mod0  12919  modlt  12923  moddiffl  12925  modfrac  12927  flmod  12928  intfrac  12929  modmulnn  12932  modvalp1  12933  modid  12939  modcyc  12949  modadd1  12951  modaddabs  12952  modmuladdnn0  12958  negmod  12959  modadd2mod  12964  modnegd  12969  modadd12d  12970  modsub12d  12971  modmulmodr  12980  modaddmulmod  12981  moddi  12982  modsubdir  12983  modeqmodmin  12984  modirr  12985  addmodlteq  12989  seqf1olem1  13083  serle  13099  expcl2lem  13115  expnegz  13137  expaddzlem  13146  expaddz  13147  expmulz  13149  ltexp2a  13155  leexp2a  13159  leexp2r  13161  exple1  13163  expubnd  13164  sq11  13179  bernneq2  13234  expmulnbnd  13239  discr1  13243  discr  13244  faclbnd  13317  bcp1nk  13344  cshweqrep  13811  remim  14100  reim0b  14102  rereb  14103  mulre  14104  cjreb  14106  recj  14107  reneg  14108  readd  14109  resub  14110  remullem  14111  remul2  14113  rediv  14114  imcj  14115  imneg  14116  imadd  14117  imsub  14118  immul2  14120  imdiv  14121  cjcj  14123  cjadd  14124  ipcnval  14126  cjmulval  14128  cjneg  14130  imval2  14134  cjreim2  14144  sqr0lem  14224  sqrlem5  14230  sqrlem7  14232  resqrtthlem  14238  remsqsqrt  14240  sqrtmul  14243  sqrtdiv  14249  sqrtneg  14251  sqrtmsq  14254  absdiv  14278  absid  14279  absexp  14287  absexpz  14288  absimle  14292  abslt  14297  absle  14298  abssubne0  14299  releabs  14304  recval  14305  abstri  14313  abs2difabs  14317  abs1m  14318  abslem2  14322  absrdbnd  14324  sqreulem  14342  sqreu  14343  amgm2  14352  icodiamlt  14417  lo1bddrp  14499  o1lo1  14511  rlimrecl  14554  rlimge0  14555  climrecl  14557  climge0  14558  climabs0  14559  reccn2  14570  o1rlimmul  14592  lo1mul2  14602  lo1sub  14604  climle  14613  climsqz  14614  climsqz2  14615  rlimsqz  14623  rlimsqz2  14624  climlec2  14632  isercolllem1  14638  climsup  14643  caucvgrlem  14646  caurcvgr  14647  caucvgrlem2  14648  iseraltlem1  14655  iseraltlem2  14656  iseraltlem3  14657  iseralt  14658  isumrecl  14739  isumge0  14740  fsumless  14770  fsumge1  14771  fsum00  14772  fsumle  14773  fsumlt  14774  fsumabs  14775  o1fsum  14787  seqabs  14788  cvgcmp  14790  cvgcmpce  14792  abscvgcvg  14793  isumrpcl  14817  isumle  14818  isumless  14819  isumsup  14821  climcndslem1  14823  climcndslem2  14824  climcnds  14825  flo1  14828  supcvg  14830  trireciplem  14836  trirecip  14837  explecnv  14839  geo2sum  14846  geo2lim  14848  geomulcvg  14849  cvgrat  14856  mertenslem1  14857  mertenslem2  14858  fprodabs  14945  fprodle  14967  iprodrecl  14973  bpolydiflem  15025  bpoly4  15030  efcllem  15048  ege2le3  15060  efaddlem  15063  efgt0  15073  eftlub  15079  effsumlt  15081  eflt  15087  eflegeo  15091  resin4p  15108  recos4p  15109  retanhcl  15129  tanhlt1  15130  efeul  15132  ef01bndlem  15154  sin01bnd  15155  cos01bnd  15156  sin01gt0  15160  cos01gt0  15161  sin02gt0  15162  absefi  15166  absef  15167  absefib  15168  efieq1re  15169  eirrlem  15172  rpnnen2lem5  15187  rpnnen2lem8  15190  rpnnen2lem9  15191  rpnnen2lem11  15193  rpnnen2lem12  15194  moddvds  15234  odd2np1  15305  divalglem5  15360  bitsp1o  15394  bitsfzo  15396  bitscmp  15399  sadcaddlem  15418  nn0seqcvgd  15522  sqnprm  15651  isprm5  15656  nonsq  15704  eulerthlem2  15724  prmdiveq  15728  odzdvds  15737  vfermltlALT  15744  pythagtriplem14  15770  pcid  15814  fldivp1  15838  pcfac  15840  pockthlem  15846  prmreclem3  15859  prmreclem4  15860  prmreclem5  15861  prmrec  15863  4sqlem5  15883  4sqlem10  15888  mul4sqlem  15894  4sqlem15  15900  4sqlem16  15901  mulgneg  17784  ghmmulg  17894  odmodnn0  18180  mndodconglem  18181  pgpfaclem2  18703  isabvd  19044  abv1z  19056  abvneg  19058  abvrec  19060  abvdiv  19061  abvdom  19062  rege0subm  20030  cnsubrg  20034  gzrngunitlem  20039  regsumfsum  20042  prmirredlem  20069  remulg  20182  regsumsupp  20197  rzgrp  20198  bl2in  22439  blhalf  22444  blssps  22463  blss  22464  methaus  22559  nrmmetd  22613  nm2dif  22663  nminvr  22707  nmdvr  22708  nlmmul0or  22721  nrginvrcnlem  22729  nmolb2d  22756  nmoi2  22768  nmoleub  22769  nmo0  22773  nmoeq0  22774  nmoco  22775  nmotri  22777  nmoid  22780  blcvx  22835  xrsxmet  22846  recld2  22851  reconnlem2  22864  opnreen  22868  metdstri  22888  metnrmlem3  22898  icchmeo  22974  icopnfcnv  22975  icopnfhmeo  22976  iccpnfhmeo  22978  xrhmeo  22979  icccvx  22983  cnheiborlem  22987  evth  22992  lebnumii  22999  pcoass  23057  pcorevlem  23059  pcorev2  23061  pi1xfrcnv  23090  nmoleub2lem  23147  nmoleub2lem3  23148  nmoleub3  23152  ncvsm1  23187  ncvspi  23189  ncvs1  23190  cphsqrtcl2  23219  ipcau2  23266  tchcphlem1  23267  tchcphlem2  23268  tchcph  23269  cphipval2  23273  cphipval  23275  iscau3  23310  rrxnm  23414  rrxcph  23415  csbren  23417  trirn  23418  rrxmval  23423  rrxmetlem  23425  rrxmet  23426  rrxdstprj1  23427  minveclem2  23432  minveclem3b  23434  minveclem4  23438  minveclem6  23440  minveclem7  23441  pjthlem1  23443  ivthlem2  23456  ivthlem3  23457  ivth2  23459  ovolfsval  23474  ovollb2lem  23492  ovolctb  23494  ovolunlem1a  23500  ovolunnul  23504  ovolfiniun  23505  ovoliunlem1  23506  ovoliun2  23510  shft2rab  23512  ovolshftlem1  23513  sca2rab  23516  ovolscalem1  23517  ovolsca  23519  ovolicc1  23520  ovolicc2lem4  23524  ovolicopnf  23528  cmmbl  23538  nulmbl  23539  nulmbl2  23540  unmbl  23541  volinun  23550  volfiniun  23551  voliunlem1  23554  voliunlem3  23556  ioombl1lem3  23564  ioombl1lem4  23565  ovolioo  23572  ioorcl2  23576  uniioovol  23583  uniioombllem3  23589  uniioombllem4  23590  uniioombllem5  23591  uniioombllem6  23592  dyadovol  23597  dyaddisjlem  23599  opnmbllem  23605  vitalilem1  23612  vitalilem2  23613  vitalilem3  23614  vitalilem4  23615  ismbf  23632  mbfmulc2lem  23651  mbfmulc2re  23652  mbfmulc2  23667  mbfinf  23669  itg1val2  23688  itg11  23695  i1fmullem  23698  i1fadd  23699  itg1addlem4  23703  itg1addlem5  23704  i1fmulclem  23706  i1fmulc  23707  itg1mulc  23708  itg1sub  23713  itg10a  23714  itg1ge0a  23715  itg1climres  23718  mbfi1fseqlem3  23721  mbfi1fseqlem4  23722  mbfi1fseqlem5  23723  mbfi1fseqlem6  23724  mbfi1flimlem  23726  mbfmullem2  23728  itg2const  23744  itg2const2  23745  itg2mulclem  23750  itg2mulc  23751  itg2splitlem  23752  itg2split  23753  itg2monolem1  23754  itg2monolem3  23756  itg2addlem  23762  itgcl  23787  itgcnlem  23793  itgrevallem1  23798  itgposval  23799  iblneg  23806  itgneg  23807  i1fibl  23811  itgitg1  23812  itgconst  23822  ibladd  23824  itgaddlem2  23827  iblabslem  23831  iblabs  23832  iblabsr  23833  iblmulc2  23834  itgmulc2lem2  23836  itgmulc2  23837  itgabs  23838  itgsplit  23839  bddmulibl  23842  dvcjbr  23949  dvfre  23951  dvexp3  23978  dveflem  23979  dvferm1lem  23984  dvferm2lem  23986  rolle  23990  cmvth  23991  mvth  23992  dvlip  23993  dvlipcn  23994  c1liplem1  23996  c1lip1  23997  dveq0  24000  dv11cn  24001  dvlt0  24005  dvle  24007  dvivthlem1  24008  dvivth  24010  lhop1lem  24013  lhop1  24014  lhop2  24015  lhop  24016  dvcvx  24020  dvfsumle  24021  dvfsumge  24022  dvfsumabs  24023  dvfsumlem1  24026  dvfsumlem2  24027  dvfsumlem4  24029  dvfsumrlimge0  24030  dvfsumrlim2  24032  dvfsum2  24034  ftc1a  24037  ftc1lem4  24039  ftc1lem5  24040  plyeq0lem  24203  coemulhi  24247  plyrecj  24272  plydivlem3  24287  aalioulem2  24325  aalioulem3  24326  aalioulem4  24327  aalioulem5  24328  aalioulem6  24329  aaliou  24330  aaliou2  24332  aaliou2b  24333  aaliou3lem3  24336  aaliou3lem7  24341  aaliou3lem9  24342  taylthlem2  24365  ulmcn  24390  ulmdvlem1  24391  mtest  24395  mtestbdd  24396  itgulm  24399  radcnvlem1  24404  radcnvlem2  24405  radcnvlt1  24409  radcnvle  24411  dvradcnv  24412  pserulm  24413  abelthlem2  24423  abelthlem5  24426  abelthlem7  24429  abelth2  24433  reeff1olem  24437  efcvx  24440  pilem2  24443  pilem3  24444  pilem3OLD  24445  sincosq2sgn  24489  sincosq3sgn  24490  sincosq4sgn  24491  coseq0negpitopi  24493  tanrpcl  24494  tangtx  24495  tanabsge  24496  sinq12gt0  24497  sinq34lt0t  24499  cosq14gt0  24500  cosq14ge0  24501  pige3  24507  coskpi  24510  cosordlem  24515  sinord  24518  tanord1  24521  tanord  24522  tanregt0  24523  efif1olem2  24527  efif1olem4  24529  eff1olem  24532  logrnaddcl  24558  logneg  24571  lognegb  24573  reexplog  24578  relogexp  24579  logfac  24584  efiarg  24590  cosargd  24591  cosarg0d  24592  argregt0  24593  argrege0  24594  argimgt0  24595  logneg2  24598  logmul2  24599  logdiv2  24600  abslogle  24601  tanarg  24602  logdivlti  24603  divlogrlim  24618  logcnlem2  24626  logcnlem3  24627  logcnlem4  24628  logcn  24630  logf1o2  24633  advlog  24637  advlogexp  24638  efopnlem1  24639  logtayllem  24642  logtayl  24643  logccv  24646  logcxp  24652  mulcxp  24668  divcxp  24670  cxpmul  24671  cxproot  24673  cxpmul2z  24674  abscxp  24675  abscxp2  24676  cxplt  24677  cxplea  24679  cxple2  24680  cxple2a  24682  cxplt3  24683  cxpsqrtlem  24685  cxpsqrt  24686  logsqrt  24687  dvcxp2  24719  cxpcn3lem  24725  resqrtcn  24727  cxpaddlelem  24729  cxpaddle  24730  abscxpbnd  24731  root1id  24732  root1eq1  24733  root1cj  24734  cxpeq  24735  loglesqrt  24736  relogbmul  24752  nnlogbexp  24756  logbrec  24757  cosangneg2d  24774  angrtmuld  24775  ang180lem2  24777  lawcoslem1  24782  lawcos  24783  pythag  24784  isosctrlem1  24785  isosctrlem2  24786  isosctrlem3  24787  ssscongptld  24789  chordthmlem  24796  chordthmlem2  24797  chordthmlem3  24798  chordthmlem4  24799  chordthmlem5  24800  heron  24802  asinsinlem  24855  reasinsin  24860  acosrecl  24867  atancj  24874  atanrecl  24875  atanlogaddlem  24877  atanlogsublem  24879  atanbndlem  24889  atans2  24895  ressatans  24898  atantayl  24901  leibpilem2  24905  leibpi  24906  leibpisum  24907  log2tlbnd  24909  log2ublem2  24911  birthdaylem2  24916  birthdaylem3  24917  cxp2limlem  24939  cxp2lim  24940  cxploglim  24941  cxploglim2  24942  divsqrtsumo1  24947  cvxcl  24948  scvxcvx  24949  jensenlem2  24951  jensen  24952  amgmlem  24953  logdiflbnd  24958  emcllem2  24960  emcllem3  24961  emcllem5  24963  emcllem6  24964  emcllem7  24965  harmonicbnd4  24974  fsumharmonic  24975  zetacvg  24978  lgamgulmlem2  24993  lgamgulmlem3  24994  lgamgulmlem4  24995  lgamgulmlem5  24996  lgamgulmlem6  24997  lgamgulm2  24999  lgambdd  25000  lgamcvg2  25018  gamcvg  25019  gamcvg2lem  25022  regamcl  25024  relgamcl  25025  lgam1  25027  ftalem1  25036  ftalem2  25037  ftalem4  25039  ftalem5  25040  basellem3  25046  basellem4  25047  basellem5  25048  basellem6  25049  basellem7  25050  basellem8  25051  basellem9  25052  efnnfsumcl  25066  chtprm  25116  chpp1  25118  chtdif  25121  efchtdvds  25122  prmorcht  25141  mumullem2  25143  fsumfldivdiaglem  25152  ppiub  25166  chtleppi  25172  chtublem  25173  chtub  25174  pclogsum  25177  vmasum  25178  logfac2  25179  chpval2  25180  chpchtsum  25181  chpub  25182  logfaclbnd  25184  logfacbnd3  25185  logfacrlim  25186  logexprlim  25187  logfacrlim2  25188  mersenne  25189  dchrabs  25222  dchrptlem1  25226  dchrptlem2  25227  bcmax  25240  bcp1ctr  25241  bposlem1  25246  bposlem9  25254  lgsvalmod  25278  lgsdilem  25286  lgsne0  25297  lgsqrlem2  25309  gausslemma2dlem1a  25327  gausslemma2dlem6  25334  lgseisenlem1  25337  lgseisenlem2  25338  lgseisen  25341  lgsquadlem1  25342  lgsquadlem2  25343  mul2sq  25381  2sqlem3  25382  2sqlem8  25388  chebbnd1lem1  25395  chebbnd1lem2  25396  chebbnd1lem3  25397  chtppilimlem1  25399  chtppilimlem2  25400  chtppilim  25401  chto1ub  25402  chto1lb  25404  chpchtlim  25405  chpo1ub  25406  vmadivsum  25408  vmadivsumb  25409  rplogsumlem1  25410  rplogsumlem2  25411  rpvmasumlem  25413  dchrisumlema  25414  dchrisumlem1  25415  dchrisumlem2  25416  dchrisumlem3  25417  dchrmusumlema  25419  dchrmusum2  25420  dchrvmasumlem1  25421  dchrvmasum2lem  25422  dchrvmasum2if  25423  dchrvmasumlem2  25424  dchrvmasumlem3  25425  dchrvmasumiflem1  25427  dchrvmasumiflem2  25428  dchrisum0flblem1  25434  dchrisum0fno1  25437  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lema  25440  dchrisum0lem1b  25441  dchrisum0lem1  25442  dchrisum0lem2a  25443  dchrisum0lem2  25444  dchrisum0lem3  25445  dchrmusumlem  25448  dchrvmasumlem  25449  rpvmasum  25452  rplogsum  25453  dirith2  25454  mudivsum  25456  mulogsumlem  25457  mulogsum  25458  logdivsum  25459  mulog2sumlem1  25460  mulog2sumlem2  25461  mulog2sumlem3  25462  vmalogdivsum2  25464  vmalogdivsum  25465  2vmadivsumlem  25466  logsqvma  25468  logsqvma2  25469  log2sumbnd  25470  selberglem1  25471  selberglem2  25472  selberglem3  25473  selberg  25474  selbergb  25475  selberg2lem  25476  selberg2  25477  selberg2b  25478  chpdifbndlem1  25479  logdivbnd  25482  selberg3lem1  25483  selberg3lem2  25484  selberg3  25485  selberg4lem1  25486  selberg4  25487  pntrmax  25490  pntrsumo1  25491  pntrsumbnd  25492  pntrsumbnd2  25493  selbergr  25494  selberg3r  25495  selberg4r  25496  selberg34r  25497  pntsval2  25502  pntrlog2bndlem1  25503  pntrlog2bndlem2  25504  pntrlog2bndlem3  25505  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  pntrlog2bndlem6a  25508  pntrlog2bndlem6  25509  pntrlog2bnd  25510  pntpbnd1a  25511  pntpbnd1  25512  pntpbnd2  25513  pntibndlem2  25517  pntibndlem3  25518  pntlemb  25523  pntlemg  25524  pntlemh  25525  pntlemn  25526  pntlemr  25528  pntlemj  25529  pntlemf  25531  pntlemk  25532  pntlemo  25533  pntlem3  25535  pntleml  25537  pnt2  25539  pnt  25540  abvcxp  25541  ostth2lem1  25544  qabvexp  25552  padicabv  25556  padicabvcxp  25558  ostth2lem2  25560  ostth2lem3  25561  ostth2lem4  25562  ostth2  25563  ostth3  25564  ttgcontlem1  26002  fveecn  26019  eqeelen  26021  brbtwn2  26022  colinearalglem4  26026  colinearalg  26027  axsegconlem9  26042  axsegconlem10  26043  ax5seglem1  26045  ax5seglem2  26046  ax5seglem3  26048  ax5seglem5  26050  ax5seglem6  26051  ax5seglem9  26054  ax5seg  26055  axbtwnid  26056  axpaschlem  26057  axpasch  26058  axeuclidlem  26079  axcontlem2  26082  axcontlem4  26084  axcontlem7  26087  axcontlem8  26088  nvm1  27871  nvpi  27873  nvz0  27874  nvmtri  27877  nvabs  27878  nvge0  27879  nv1  27881  smcnlem  27903  ipval2lem4  27912  ipval2  27913  4ipval2  27914  ipidsq  27916  dipcj  27920  dip0r  27923  ipz  27925  nmoub3i  27979  nmlno0lem  27999  nmblolbii  28005  blocnilem  28010  cncph  28025  ipasslem4  28040  ipasslem5  28041  ipblnfi  28062  minvecolem2  28082  minvecolem4  28087  minvecolem6  28089  minvecolem7  28090  htthlem  28125  normpyc  28354  hhph  28386  bcs2  28390  norm1  28457  norm1exi  28458  pjhthlem1  28601  eigvalcl  29171  eighmorth  29174  nmlnop0iALT  29205  nmbdoplbi  29234  nmcexi  29236  nmcoplbi  29238  nmbdfnlbi  29259  nmcfnlbi  29262  riesz4i  29273  cnlnadjlem2  29278  cnlnadjlem7  29283  nmopcoi  29305  nmopcoadji  29311  branmfn  29315  leopnmid  29348  opsqrlem1  29350  hst1h  29437  hstle  29440  hstoh  29442  sto2i  29447  stadd3i  29458  strlem1  29460  golem1  29481  stcltrlem1  29486  cdj1i  29643  cdj3lem1  29644  cdj3lem3b  29650  cdj3i  29651  lt2addrd  29866  le2halvesd  29870  fzsplit3  29903  bcm1n  29904  fsumiunle  29925  bhmafibid1  29992  bhmafibid2  29993  2sqmod  29996  psgnfzto1stlem  30198  elunitcn  30292  sqsscirc1  30302  sqsscirc2  30303  cnre2csqima  30305  rmulccn  30322  xrge0iifcnv  30327  xrge0iifhom  30331  zrhnm  30361  rezh  30363  nexple  30419  indsum  30431  esumpcvgval  30488  esumcvgsum  30498  dya2ub  30680  dya2icoseg  30687  omssubadd  30710  eulerpartlemgc  30772  ballotlemsi  30924  sgnmul  30952  sgnsub  30954  plymulx0  30972  signsply0  30976  signsvtp  31008  signsvtn  31009  signsvfpn  31010  signsvfnn  31011  divsqrtid  31020  reprgt  31047  reprinfz1  31048  breprexplemc  31058  circlemethhgt  31069  hgt750lemd  31074  hgt750lemf  31079  hgt750lemg  31080  hgt750lemb  31082  hgt750lema  31083  hgt750leme  31084  tgoldbachgtde  31086  subfacval2  31514  subfaclim  31515  subfacval3  31516  resconn  31573  sinccvglem  31910  circum  31912  climlec3  31963  faclimlem1  31973  faclimlem2  31974  faclimlem3  31975  faclim  31976  iprodfac  31977  faclim2  31978  dnicld1  32801  dnizeq0  32804  dnizphlfeqhlf  32805  dnibndlem2  32808  dnibndlem3  32809  dnibndlem5  32811  dnibndlem6  32812  dnibndlem7  32813  dnibndlem8  32814  dnibndlem9  32815  dnibndlem10  32816  dnibndlem11  32817  dnibndlem12  32818  dnibndlem13  32819  dnibnd  32820  dnicn  32821  knoppcnlem4  32825  knoppcnlem5  32826  knoppcnlem6  32827  knoppcnlem8  32829  knoppcnlem9  32830  knoppcnlem10  32831  knoppcnlem11  32832  unblimceq0  32837  unbdqndv2lem1  32839  unbdqndv2lem2  32840  knoppndvlem1  32842  knoppndvlem6  32847  knoppndvlem8  32849  knoppndvlem9  32850  knoppndvlem10  32851  knoppndvlem11  32852  knoppndvlem12  32853  knoppndvlem14  32855  knoppndvlem15  32856  knoppndvlem17  32858  knoppndvlem18  32859  knoppndvlem19  32860  knoppndvlem20  32861  knoppndvlem21  32862  ltflcei  33729  sin2h  33731  cos2h  33732  tan2h  33733  poimirlem29  33770  opnmbllem0  33777  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  mbfposadd  33788  itg2addnclem  33792  itg2addnclem2  33793  itg2addnclem3  33794  itg2addnc  33795  itg2gt0cn  33796  ibladdnc  33798  itgaddnclem2  33800  iblabsnclem  33804  iblabsnc  33805  iblmulc2nc  33806  itgmulc2nclem2  33808  itgmulc2nc  33809  itgabsnc  33810  bddiblnc  33811  ftc1cnnclem  33814  ftc1cnnc  33815  ftc1anclem1  33816  ftc1anclem2  33817  ftc1anclem3  33818  ftc1anclem4  33819  ftc1anclem5  33820  ftc1anclem6  33821  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  areacirclem1  33831  areacirclem5  33835  areacirc  33836  mettrifi  33883  lmclim2  33884  geomcau  33885  isbnd3  33913  ssbnd  33917  cntotbnd  33925  bfplem1  33951  bfplem2  33952  bfp  33953  rrnmet  33958  rrndstprj1  33959  rrndstprj2  33960  rrncmslem  33961  rrnequiv  33964  rrntotbnd  33965  ismrer1  33967  eldioph2lem1  37843  lzenom  37853  rencldnfilem  37904  irrapxlem1  37906  irrapxlem2  37907  irrapxlem3  37908  irrapxlem4  37909  irrapxlem5  37910  pellexlem2  37914  pellexlem6  37918  pell1234qrreccl  37938  pell14qrgt0  37943  pell14qrdivcl  37949  pell14qrexpclnn0  37950  pell14qrexpcl  37951  pell14qrdich  37953  pell1qrgaplem  37957  pellfundex  37970  reglogmul  37977  reglogexp  37978  reglogbas  37979  reglog1  37980  pellfund14  37982  rmspecfund  37993  monotoddzzfi  38026  expmordi  38031  jm2.24nn  38045  jm2.17a  38046  jm2.17b  38047  jm2.17c  38048  jm2.24  38049  acongrep  38066  fzmaxdif  38067  acongeq  38069  modabsdifz  38072  jm2.19lem4  38078  jm2.19  38079  jm2.26lem3  38087  jm3.1lem1  38103  jm3.1lem2  38104  itgpowd  38318  areaquad  38320  absmulrposd  38975  extoimad  38982  imo72b2lem0  38983  imo72b2lem1  38989  imo72b2  38993  int-addcomd  38994  int-addassocd  38995  int-addsimpd  38996  int-mulcomd  38997  int-mulassocd  38998  int-mulsimpd  38999  int-leftdistd  39000  int-rightdistd  39001  int-sqdefd  39002  int-mul11d  39003  int-mul12d  39004  int-add01d  39005  int-add02d  39006  int-sqgeq0d  39007  int-eqmvtd  39010  cvgdvgrat  39030  radcnvrat  39031  hashnzfzclim  39039  dvconstbi  39051  binomcxplemnn0  39066  binomcxplemnotnn0  39073  isosctrlem1ALT  39682  sineq0ALT  39685  infnsuprnmpt  39966  oddfl  39989  dstregt0  39993  zltlesub  39997  lt3addmuld  40014  fperiodmullem  40016  fperiodmul  40017  lt4addmuld  40019  fzdifsuc2  40023  supxrgere  40047  supxrgelem  40051  suplesup  40053  supsubc  40067  xralrple2  40068  abslt2sqd  40074  xralrple3  40088  reclt0d  40105  ltmulneg  40112  rexabslelem  40142  supminfrnmpt  40169  leneg2d  40173  leneg3d  40184  supminfxr  40191  absimnre  40204  absimlere  40207  iooabslt  40223  iccshift  40243  iooshift  40247  sqrlearg  40278  fmul01  40310  fmul01lt1lem1  40314  fmul01lt1lem2  40315  fprodabs2  40325  climinf  40336  limcrecl  40359  lptre2pt  40370  limcleqr  40374  0ellimcdiv  40379  limclner  40381  climleltrp  40406  climinf2mpt  40444  climinf3  40446  climxrre  40480  climliminflimsupd  40531  liminfltlem  40534  liminflimsupclim  40537  cnrefiisplem  40553  sinaover2ne0  40577  cncfperiod  40590  ioccncflimc  40596  cncficcgt0  40599  icocncflimc  40600  cncfshiftioo  40603  cncfiooicc  40605  fperdvper  40631  dvbdfbdioolem1  40641  dvbdfbdioolem2  40642  dvbdfbdioo  40643  ioodvbdlimc1lem1  40644  ioodvbdlimc1lem2  40645  ioodvbdlimc1  40646  ioodvbdlimc2lem  40647  ioodvbdlimc2  40648  dvnmul  40656  dvnprodlem1  40659  dvnprodlem2  40660  itgcoscmulx  40682  volioc  40685  itgsincmulx  40687  itgiccshift  40693  itgperiod  40694  itgsbtaddcnst  40695  volico  40697  voliooico  40706  voliccico  40713  stoweidlem7  40721  stoweidlem11  40725  stoweidlem13  40727  stoweidlem17  40731  stoweidlem19  40733  stoweidlem20  40734  stoweidlem21  40735  stoweidlem22  40736  stoweidlem23  40737  stoweidlem24  40738  stoweidlem26  40740  stoweidlem32  40746  stoweidlem36  40750  stoweidlem44  40758  stoweidlem47  40761  wallispilem3  40781  wallispi2lem1  40785  stirlinglem1  40788  stirlinglem5  40792  stirlinglem11  40798  stirlinglem12  40799  stirlinglem14  40801  dirkerval2  40808  dirkerre  40809  dirkertrigeqlem2  40813  dirkertrigeq  40815  dirkeritg  40816  dirkercncflem1  40817  dirkercncflem2  40818  dirkercncflem4  40820  fourierdlem4  40825  fourierdlem6  40827  fourierdlem7  40828  fourierdlem13  40834  fourierdlem14  40835  fourierdlem16  40837  fourierdlem18  40839  fourierdlem19  40840  fourierdlem21  40842  fourierdlem22  40843  fourierdlem24  40845  fourierdlem26  40847  fourierdlem28  40849  fourierdlem30  40851  fourierdlem35  40856  fourierdlem39  40860  fourierdlem40  40861  fourierdlem41  40862  fourierdlem42  40863  fourierdlem43  40864  fourierdlem44  40865  fourierdlem47  40867  fourierdlem48  40868  fourierdlem49  40869  fourierdlem50  40870  fourierdlem51  40871  fourierdlem53  40873  fourierdlem56  40876  fourierdlem57  40877  fourierdlem58  40878  fourierdlem59  40879  fourierdlem60  40880  fourierdlem61  40881  fourierdlem62  40882  fourierdlem63  40883  fourierdlem64  40884  fourierdlem65  40885  fourierdlem66  40886  fourierdlem68  40888  fourierdlem70  40890  fourierdlem71  40891  fourierdlem72  40892  fourierdlem73  40893  fourierdlem74  40894  fourierdlem75  40895  fourierdlem76  40896  fourierdlem77  40897  fourierdlem78  40898  fourierdlem79  40899  fourierdlem80  40900  fourierdlem81  40901  fourierdlem83  40903  fourierdlem84  40904  fourierdlem85  40905  fourierdlem87  40907  fourierdlem88  40908  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem92  40912  fourierdlem93  40913  fourierdlem95  40915  fourierdlem97  40917  fourierdlem101  40921  fourierdlem103  40923  fourierdlem104  40924  fourierdlem107  40927  fourierdlem109  40929  fourierdlem111  40931  fourierdlem112  40932  fouriercnp  40940  sqwvfoura  40942  sqwvfourb  40943  fouriersw  40945  etransclem14  40962  etransclem18  40966  etransclem23  40971  etransclem24  40972  etransclem27  40975  etransclem46  40994  etransclem48  40996  qndenserrnbllem  41011  ioorrnopnlem  41021  sge0tsms  41094  sge0cl  41095  sge0split  41123  sge0iunmptlemfi  41127  sge0rpcpnf  41135  sge0isum  41141  sge0ad2en  41145  sge0xaddlem1  41147  sge0xaddlem2  41148  sge0gtfsumgt  41157  sge0seq  41160  meadif  41193  meaiininclem  41200  carageniuncllem1  41235  carageniuncllem2  41236  hoicvrrex  41270  ovnsubaddlem1  41284  hsphoidmvle2  41299  hsphoidmvle  41300  hoidmvval0  41301  hoiprodp1  41302  hoidmv1lelem1  41305  hoidmv1lelem2  41306  hoidmv1le  41308  hoidmvlelem1  41309  hoidmvlelem2  41310  hoidmvlelem3  41311  hoiqssbllem2  41337  hspmbllem1  41340  ovolval2lem  41357  ovolval3  41361  ovolval5lem1  41366  ovnovollem1  41370  ovnovollem2  41371  vonioolem1  41394  vonioo  41396  vonicclem1  41397  vonicc  41399  smfaddlem1  41471  smflimlem4  41482  smfmullem1  41498  smfmullem2  41499  smfmullem3  41500  smfdiv  41504  smfneg  41510  sigaras  41544  sigarms  41545  sigarls  41546  sigarexp  41548  sigarperm  41549  sigarimcd  41551  sigarcol  41553  sharhght  41554  cevathlem2  41557  m1mod0mod1  41932  bgoldbtbndlem2  42287  ltsubaddb  42890  ltsubsubb  42891  ltsubadd2b  42892  flsubz  42898  fldivmod  42899  m1modmmod  42902  logblt1b  42944  dignn0fr  42981  dignn0flhalflem1  42995  dignn0flhalflem2  42996  nn0sumshdiglemA  42999  amgmwlem  43137  amgmlemALT  43138