Theorem recnd 10385

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

Syntax hints:   → wi 4   ∈ wcel 2166  ℂcc 10250  ℝcr 10251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803  ax-resscn 10309

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812

This theorem is referenced by:  00id  10530  mul02lem1  10531  addid1  10535  cnegex  10536  ltadd1  10819  leadd2  10821  ltsubadd  10822  ltsubadd2  10823  lesubadd  10824  lesubadd2  10825  lesub1  10846  lesub2  10847  ltnegcon1  10853  ltnegcon2  10854  add20  10864  subge0  10865  suble0  10866  lesub0  10869  mulge0  10870  eqord2  10883  lesub3d  10970  possumd  10977  sublt0d  10978  rereccl  11069  redivcl  11070  recgt0  11197  prodgt0  11198  prodge0OLD  11200  ltmul1a  11202  ltdiv1  11217  ltmuldiv  11226  ltrec  11235  recp1lt1  11251  recreclt  11252  ledivp1  11255  supadd  11321  infrenegsup  11336  rimul  11341  cru  11342  avglt1  11596  avglt2  11597  lt2addmuld  11608  div4p1lem1div2  11613  nn0cnd  11680  zcn  11709  zeo  11791  zcnd  11811  eluzmn  11975  eluzelcn  11980  cnref1o  12107  rpcn  12124  rpcnd  12158  ltaddrp2d  12190  mul2lt0rlt0  12216  mul2lt0rgt0  12217  mul2lt0llt0  12218  mul2lt0lgt0  12219  mul2lt0bi  12220  prodge0rd  12221  prodge0ld  12222  qbtwnre  12318  xralrple  12324  xpncan  12369  xmulcom  12384  xmulneg1  12387  xlemul1  12408  icoshftf1o  12586  lincmb01cmp  12608  iccf1o  12609  divfl0  12920  fladdz  12921  flzadd  12922  flhalf  12926  ceim1l  12941  intfracq  12953  fldiv  12954  modvalr  12966  flpmodeq  12968  mod0  12970  modlt  12974  moddiffl  12976  modfrac  12978  flmod  12979  intfrac  12980  modmulnn  12983  modvalp1  12984  modid  12990  modcyc  13000  modadd1  13002  modaddabs  13003  modmuladdnn0  13009  negmod  13010  modadd2mod  13015  modnegd  13020  modadd12d  13021  modsub12d  13022  modmulmodr  13031  modaddmulmod  13032  moddi  13033  modsubdir  13034  modeqmodmin  13035  modirr  13036  addmodlteq  13040  seqf1olem1  13134  serle  13150  expcl2lem  13166  expnegz  13188  expaddzlem  13197  expaddz  13198  expmulz  13200  ltexp2a  13206  leexp2a  13210  leexp2r  13212  exple1  13214  expubnd  13215  sq11  13230  bernneq2  13285  expmulnbnd  13290  discr1  13294  discr  13295  faclbnd  13370  bcp1nk  13397  cshweqrep  13942  remim  14234  reim0b  14236  rereb  14237  mulre  14238  cjreb  14240  recj  14241  reneg  14242  readd  14243  resub  14244  remullem  14245  remul2  14247  rediv  14248  imcj  14249  imneg  14250  imadd  14251  imsub  14252  immul2  14254  imdiv  14255  cjcj  14257  cjadd  14258  ipcnval  14260  cjmulval  14262  cjneg  14264  imval2  14268  cjreim2  14278  sqr0lem  14358  sqrlem5  14364  sqrlem7  14366  resqrtthlem  14372  remsqsqrt  14374  sqrtmul  14377  sqrtdiv  14383  sqrtneg  14385  sqrtmsq  14388  absdiv  14412  absid  14413  absexp  14421  absexpz  14422  absimle  14426  abslt  14431  absle  14432  abssubne0  14433  releabs  14438  recval  14439  abstri  14447  abs2difabs  14451  abs1m  14452  abslem2  14456  absrdbnd  14458  sqreulem  14476  sqreu  14477  amgm2  14486  icodiamlt  14551  lo1bddrp  14633  o1lo1  14645  rlimrecl  14688  rlimge0  14689  climrecl  14691  climge0  14692  climabs0  14693  reccn2  14704  o1rlimmul  14726  lo1mul2  14736  lo1sub  14738  climle  14747  climsqz  14748  climsqz2  14749  rlimsqz  14757  rlimsqz2  14758  climlec2  14766  isercolllem1  14772  climsup  14777  caucvgrlem  14780  caurcvgr  14781  caucvgrlem2  14782  iseraltlem1  14789  iseraltlem2  14790  iseraltlem3  14791  iseralt  14792  isumrecl  14871  isumge0  14872  fsumless  14902  fsumge1  14903  fsum00  14904  fsumle  14905  fsumlt  14906  fsumabs  14907  o1fsum  14919  seqabs  14920  cvgcmp  14922  cvgcmpce  14924  abscvgcvg  14925  isumrpcl  14949  isumle  14950  isumless  14951  isumsup  14953  climcndslem1  14955  climcndslem2  14956  climcnds  14957  flo1  14960  supcvg  14962  trireciplem  14968  trirecip  14969  explecnv  14971  geo2sum  14978  geo2lim  14980  geomulcvg  14981  cvgrat  14988  mertenslem1  14989  mertenslem2  14990  fprodabs  15077  fprodle  15099  iprodrecl  15105  bpolydiflem  15157  bpoly4  15162  efcllem  15180  ege2le3  15192  efaddlem  15195  efgt0  15205  eftlub  15211  effsumlt  15213  eflt  15219  eflegeo  15223  resin4p  15240  recos4p  15241  retanhcl  15261  tanhlt1  15262  efeul  15264  ef01bndlem  15286  sin01bnd  15287  cos01bnd  15288  sin01gt0  15292  cos01gt0  15293  sin02gt0  15294  absefi  15298  absef  15299  absefib  15300  efieq1re  15301  eirrlem  15306  rpnnen2lem5  15321  rpnnen2lem8  15324  rpnnen2lem9  15325  rpnnen2lem11  15327  rpnnen2lem12  15328  moddvds  15368  odd2np1  15439  divalglem5  15494  bitsp1o  15528  bitsfzo  15530  bitscmp  15533  sadcaddlem  15552  nn0seqcvgd  15656  sqnprm  15785  isprm5  15790  nonsq  15838  eulerthlem2  15858  prmdiveq  15862  odzdvds  15871  vfermltlALT  15878  pythagtriplem14  15904  pcid  15948  fldivp1  15972  pcfac  15974  pockthlem  15980  prmreclem3  15993  prmreclem4  15994  prmreclem5  15995  prmrec  15997  4sqlem5  16017  4sqlem10  16022  mul4sqlem  16028  4sqlem15  16034  4sqlem16  16035  mulgneg  17913  ghmmulg  18023  odmodnn0  18310  mndodconglem  18311  pgpfaclem2  18835  isabvd  19176  abv1z  19188  abvneg  19190  abvrec  19192  abvdiv  19193  abvdom  19194  rege0subm  20162  cnsubrg  20166  gzrngunitlem  20171  regsumfsum  20174  prmirredlem  20201  remulg  20314  regsumsupp  20329  rzgrp  20330  bl2in  22575  blhalf  22580  blssps  22599  blss  22600  methaus  22695  nrmmetd  22749  nm2dif  22799  nminvr  22843  nmdvr  22844  nlmmul0or  22857  nrginvrcnlem  22865  nmolb2d  22892  nmoi2  22904  nmoleub  22905  nmo0  22909  nmoeq0  22910  nmoco  22911  nmotri  22913  nmoid  22916  blcvx  22971  xrsxmet  22982  recld2  22987  reconnlem2  23000  opnreen  23004  metdstri  23024  metnrmlem3  23034  icchmeo  23110  icopnfcnv  23111  icopnfhmeo  23112  iccpnfhmeo  23114  xrhmeo  23115  icccvx  23119  cnheiborlem  23123  evth  23128  lebnumii  23135  pcoass  23193  pcorevlem  23195  pcorev2  23197  pi1xfrcnv  23226  nmoleub2lem  23283  nmoleub2lem3  23284  nmoleub3  23288  ncvsm1  23323  ncvspi  23325  ncvs1  23326  cphsqrtcl2  23355  ipcau2  23402  tcphcphlem1  23403  tcphcphlem2  23404  tcphcph  23405  cphipval2  23409  cphipval  23411  iscau3  23446  rrxnm  23559  rrxcph  23560  csbren  23567  trirn  23568  rrxmval  23573  rrxmetlem  23575  rrxmet  23576  rrxdstprj1  23577  ehl1eudis  23588  ehl2eudis  23590  minveclem2  23594  minveclem3b  23596  minveclem4  23600  minveclem6  23602  minveclem7  23603  pjthlem1  23605  ivthlem2  23618  ivthlem3  23619  ivth2  23621  ovolfsval  23636  ovollb2lem  23654  ovolctb  23656  ovolunlem1a  23662  ovolunnul  23666  ovolfiniun  23667  ovoliunlem1  23668  ovoliun2  23672  shft2rab  23674  ovolshftlem1  23675  sca2rab  23678  ovolscalem1  23679  ovolsca  23681  ovolicc1  23682  ovolicc2lem4  23686  ovolicopnf  23690  cmmbl  23700  nulmbl  23701  nulmbl2  23702  unmbl  23703  volinun  23712  volfiniun  23713  voliunlem1  23716  voliunlem3  23718  ioombl1lem3  23726  ioombl1lem4  23727  ovolioo  23734  ioorcl2  23738  uniioovol  23745  uniioombllem3  23751  uniioombllem4  23752  uniioombllem5  23753  uniioombllem6  23754  dyadovol  23759  dyaddisjlem  23761  opnmbllem  23767  vitalilem1  23774  vitalilem2  23775  vitalilem3  23776  vitalilem4  23777  ismbf  23794  mbfmulc2lem  23813  mbfmulc2re  23814  mbfmulc2  23829  mbfinf  23831  itg1val2  23850  itg11  23857  i1fmullem  23860  i1fadd  23861  itg1addlem4  23865  itg1addlem5  23866  i1fmulclem  23868  i1fmulc  23869  itg1mulc  23870  itg1sub  23875  itg10a  23876  itg1ge0a  23877  itg1climres  23880  mbfi1fseqlem3  23883  mbfi1fseqlem4  23884  mbfi1fseqlem5  23885  mbfi1fseqlem6  23886  mbfi1flimlem  23888  mbfmullem2  23890  itg2const  23906  itg2const2  23907  itg2mulclem  23912  itg2mulc  23913  itg2splitlem  23914  itg2split  23915  itg2monolem1  23916  itg2monolem3  23918  itg2addlem  23924  itgcl  23949  itgcnlem  23955  itgrevallem1  23960  itgposval  23961  iblneg  23968  itgneg  23969  i1fibl  23973  itgitg1  23974  itgconst  23984  ibladd  23986  itgaddlem2  23989  iblabslem  23993  iblabs  23994  iblabsr  23995  iblmulc2  23996  itgmulc2lem2  23998  itgmulc2  23999  itgabs  24000  itgsplit  24001  bddmulibl  24004  dvcjbr  24111  dvfre  24113  dvexp3  24140  dveflem  24141  dvferm1lem  24146  dvferm2lem  24148  rolle  24152  cmvth  24153  mvth  24154  dvlip  24155  dvlipcn  24156  c1liplem1  24158  c1lip1  24159  dveq0  24162  dv11cn  24163  dvlt0  24167  dvle  24169  dvivthlem1  24170  dvivth  24172  lhop1lem  24175  lhop1  24176  lhop2  24177  lhop  24178  dvcvx  24182  dvfsumle  24183  dvfsumge  24184  dvfsumabs  24185  dvfsumlem1  24188  dvfsumlem2  24189  dvfsumlem4  24191  dvfsumrlimge0  24192  dvfsumrlim2  24194  dvfsum2  24196  ftc1a  24199  ftc1lem4  24201  ftc1lem5  24202  plyeq0lem  24365  coemulhi  24409  plyrecj  24434  plydivlem3  24449  aalioulem2  24487  aalioulem3  24488  aalioulem4  24489  aalioulem5  24490  aalioulem6  24491  aaliou  24492  aaliou2  24494  aaliou2b  24495  aaliou3lem3  24498  aaliou3lem7  24503  aaliou3lem9  24504  taylthlem2  24527  ulmcn  24552  ulmdvlem1  24553  mtest  24557  mtestbdd  24558  itgulm  24561  radcnvlem1  24566  radcnvlem2  24567  radcnvlt1  24571  radcnvle  24573  dvradcnv  24574  pserulm  24575  abelthlem2  24585  abelthlem5  24588  abelthlem7  24591  abelth2  24595  reeff1olem  24599  efcvx  24602  pilem2  24605  pilem3  24606  pilem3OLD  24607  sincosq2sgn  24651  sincosq3sgn  24652  sincosq4sgn  24653  coseq0negpitopi  24655  tanrpcl  24656  tangtx  24657  tanabsge  24658  sinq12gt0  24659  sinq34lt0t  24661  cosq14gt0  24662  cosq14ge0  24663  pige3  24669  coskpi  24672  cosordlem  24677  sinord  24680  tanord1  24683  tanord  24684  tanregt0  24685  efif1olem2  24689  efif1olem4  24691  eff1olem  24694  logrnaddcl  24720  logneg  24733  lognegb  24735  reexplog  24740  relogexp  24741  logfac  24746  efiarg  24752  cosargd  24753  cosarg0d  24754  argregt0  24755  argrege0  24756  argimgt0  24757  logneg2  24760  logmul2  24761  logdiv2  24762  abslogle  24763  tanarg  24764  logdivlti  24765  divlogrlim  24780  logcnlem2  24788  logcnlem3  24789  logcnlem4  24790  logcn  24792  logf1o2  24795  advlog  24799  advlogexp  24800  efopnlem1  24801  logtayllem  24804  logtayl  24805  logccv  24808  logcxp  24814  mulcxp  24830  divcxp  24832  cxpmul  24833  cxproot  24835  cxpmul2z  24836  abscxp  24837  abscxp2  24838  cxplt  24839  cxplea  24841  cxple2  24842  cxple2a  24844  cxplt3  24845  cxpsqrtlem  24847  cxpsqrt  24848  logsqrt  24849  dvcxp2  24884  cxpcn3lem  24890  resqrtcn  24892  cxpaddlelem  24894  cxpaddle  24895  abscxpbnd  24896  root1id  24897  root1eq1  24898  root1cj  24899  cxpeq  24900  loglesqrt  24901  relogbmul  24917  nnlogbexp  24921  logbrec  24922  cosangneg2d  24947  angrtmuld  24948  ang180lem2  24950  lawcoslem1  24955  lawcos  24956  pythag  24957  isosctrlem1  24958  isosctrlem2  24959  isosctrlem3  24960  ssscongptld  24962  chordthmlem  24972  chordthmlem2  24973  chordthmlem3  24974  chordthmlem4  24975  chordthmlem5  24976  heron  24978  asinsinlem  25031  reasinsin  25036  acosrecl  25043  atancj  25050  atanrecl  25051  atanlogaddlem  25053  atanlogsublem  25055  atanbndlem  25065  atans2  25071  ressatans  25074  atantayl  25077  leibpilem2  25081  leibpi  25082  leibpisum  25083  log2tlbnd  25085  log2ublem2  25087  birthdaylem2  25092  birthdaylem3  25093  cxp2limlem  25115  cxp2lim  25116  cxploglim  25117  cxploglim2  25118  divsqrtsumo1  25123  cvxcl  25124  scvxcvx  25125  jensenlem2  25127  jensen  25128  amgmlem  25129  logdiflbnd  25134  emcllem2  25136  emcllem3  25137  emcllem5  25139  emcllem6  25140  emcllem7  25141  harmonicbnd4  25150  fsumharmonic  25151  zetacvg  25154  lgamgulmlem2  25169  lgamgulmlem3  25170  lgamgulmlem4  25171  lgamgulmlem5  25172  lgamgulmlem6  25173  lgamgulm2  25175  lgambdd  25176  lgamcvg2  25194  gamcvg  25195  gamcvg2lem  25198  regamcl  25200  relgamcl  25201  lgam1  25203  ftalem1  25212  ftalem2  25213  ftalem4  25215  ftalem5  25216  basellem3  25222  basellem4  25223  basellem5  25224  basellem6  25225  basellem7  25226  basellem8  25227  basellem9  25228  efnnfsumcl  25242  chtprm  25292  chpp1  25294  chtdif  25297  efchtdvds  25298  prmorcht  25317  mumullem2  25319  fsumfldivdiaglem  25328  ppiub  25342  chtleppi  25348  chtublem  25349  chtub  25350  pclogsum  25353  vmasum  25354  logfac2  25355  chpval2  25356  chpchtsum  25357  chpub  25358  logfaclbnd  25360  logfacbnd3  25361  logfacrlim  25362  logexprlim  25363  logfacrlim2  25364  mersenne  25365  dchrabs  25398  dchrptlem1  25402  dchrptlem2  25403  bcmax  25416  bcp1ctr  25417  bposlem1  25422  bposlem9  25430  lgsvalmod  25454  lgsdilem  25462  lgsne0  25473  lgsqrlem2  25485  gausslemma2dlem1a  25503  gausslemma2dlem6  25510  lgseisenlem1  25513  lgseisenlem2  25514  lgseisen  25517  lgsquadlem1  25518  lgsquadlem2  25519  mul2sq  25557  2sqlem3  25558  2sqlem8  25564  chebbnd1lem1  25571  chebbnd1lem2  25572  chebbnd1lem3  25573  chtppilimlem1  25575  chtppilimlem2  25576  chtppilim  25577  chto1ub  25578  chto1lb  25580  chpchtlim  25581  chpo1ub  25582  vmadivsum  25584  vmadivsumb  25585  rplogsumlem1  25586  rplogsumlem2  25587  rpvmasumlem  25589  dchrisumlema  25590  dchrisumlem1  25591  dchrisumlem2  25592  dchrisumlem3  25593  dchrmusumlema  25595  dchrmusum2  25596  dchrvmasumlem1  25597  dchrvmasum2lem  25598  dchrvmasum2if  25599  dchrvmasumlem2  25600  dchrvmasumlem3  25601  dchrvmasumiflem1  25603  dchrvmasumiflem2  25604  dchrisum0flblem1  25610  dchrisum0fno1  25613  rpvmasum2  25614  dchrisum0re  25615  dchrisum0lema  25616  dchrisum0lem1b  25617  dchrisum0lem1  25618  dchrisum0lem2a  25619  dchrisum0lem2  25620  dchrisum0lem3  25621  dchrmusumlem  25624  dchrvmasumlem  25625  rpvmasum  25628  rplogsum  25629  dirith2  25630  mudivsum  25632  mulogsumlem  25633  mulogsum  25634  logdivsum  25635  mulog2sumlem1  25636  mulog2sumlem2  25637  mulog2sumlem3  25638  vmalogdivsum2  25640  vmalogdivsum  25641  2vmadivsumlem  25642  logsqvma  25644  logsqvma2  25645  log2sumbnd  25646  selberglem1  25647  selberglem2  25648  selberglem3  25649  selberg  25650  selbergb  25651  selberg2lem  25652  selberg2  25653  selberg2b  25654  chpdifbndlem1  25655  logdivbnd  25658  selberg3lem1  25659  selberg3lem2  25660  selberg3  25661  selberg4lem1  25662  selberg4  25663  pntrmax  25666  pntrsumo1  25667  pntrsumbnd  25668  pntrsumbnd2  25669  selbergr  25670  selberg3r  25671  selberg4r  25672  selberg34r  25673  pntsval2  25678  pntrlog2bndlem1  25679  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  pntrlog2bndlem6a  25684  pntrlog2bndlem6  25685  pntrlog2bnd  25686  pntpbnd1a  25687  pntpbnd1  25688  pntpbnd2  25689  pntibndlem2  25693  pntibndlem3  25694  pntlemb  25699  pntlemg  25700  pntlemh  25701  pntlemn  25702  pntlemr  25704  pntlemj  25705  pntlemf  25707  pntlemk  25708  pntlemo  25709  pntlem3  25711  pntleml  25713  pnt2  25715  pnt  25716  abvcxp  25717  ostth2lem1  25720  qabvexp  25728  padicabv  25732  padicabvcxp  25734  ostth2lem2  25736  ostth2lem3  25737  ostth2lem4  25738  ostth2  25739  ostth3  25740  ttgcontlem1  26184  fveecn  26201  eqeelen  26203  brbtwn2  26204  colinearalglem4  26208  colinearalg  26209  axsegconlem9  26224  axsegconlem10  26225  ax5seglem1  26227  ax5seglem2  26228  ax5seglem3  26230  ax5seglem5  26232  ax5seglem6  26233  ax5seglem9  26236  ax5seg  26237  axbtwnid  26238  axpaschlem  26239  axpasch  26240  axeuclidlem  26261  axcontlem2  26264  axcontlem4  26266  axcontlem7  26269  axcontlem8  26270  elntg2  26284  nvm1  28075  nvpi  28077  nvz0  28078  nvmtri  28081  nvabs  28082  nvge0  28083  nv1  28085  smcnlem  28107  ipval2lem4  28116  ipval2  28117  4ipval2  28118  ipidsq  28120  dipcj  28124  dip0r  28127  ipz  28129  nmoub3i  28183  nmlno0lem  28203  nmblolbii  28209  blocnilem  28214  cncph  28229  ipasslem4  28244  ipasslem5  28245  ipblnfi  28266  minvecolem2  28286  minvecolem4  28291  minvecolem6  28293  minvecolem7  28294  htthlem  28329  normpyc  28558  hhph  28590  bcs2  28594  norm1  28661  norm1exi  28662  pjhthlem1  28805  eigvalcl  29375  eighmorth  29378  nmlnop0iALT  29409  nmbdoplbi  29438  nmcexi  29440  nmcoplbi  29442  nmbdfnlbi  29463  nmcfnlbi  29466  riesz4i  29477  cnlnadjlem2  29482  cnlnadjlem7  29487  nmopcoi  29509  nmopcoadji  29515  branmfn  29519  leopnmid  29552  opsqrlem1  29554  hst1h  29641  hstle  29644  hstoh  29646  sto2i  29651  stadd3i  29662  strlem1  29664  golem1  29685  stcltrlem1  29690  cdj1i  29847  cdj3lem1  29848  cdj3lem3b  29854  cdj3i  29855  lt2addrd  30063  le2halvesd  30067  fzsplit3  30100  bcm1n  30101  fsumiunle  30122  bhmafibid1  30189  bhmafibid2  30190  2sqmod  30193  psgnfzto1stlem  30395  elunitcn  30489  sqsscirc1  30499  sqsscirc2  30500  cnre2csqima  30502  rmulccn  30519  xrge0iifcnv  30524  xrge0iifhom  30528  zrhnm  30558  rezh  30560  nexple  30616  indsum  30628  esumpcvgval  30685  esumcvgsum  30695  dya2ub  30877  dya2icoseg  30884  omssubadd  30907  eulerpartlemgc  30969  ballotlemsi  31122  sgnmul  31150  sgnsub  31152  plymulx0  31171  signsply0  31175  signsvtp  31209  signsvtn  31210  signsvfpn  31211  signsvfnn  31212  divsqrtid  31221  reprgt  31248  reprinfz1  31249  breprexplemc  31259  circlemethhgt  31270  hgt750lemd  31275  hgt750lemf  31280  hgt750lemg  31281  hgt750lemb  31283  hgt750lema  31284  hgt750leme  31285  tgoldbachgtde  31287  subfacval2  31715  subfaclim  31716  subfacval3  31717  resconn  31774  sinccvglem  32110  circum  32112  climlec3  32161  faclimlem1  32171  faclimlem2  32172  faclimlem3  32173  faclim  32174  iprodfac  32175  faclim2  32176  dnicld1  32995  dnizeq0  32998  dnizphlfeqhlf  32999  dnibndlem2  33002  dnibndlem3  33003  dnibndlem5  33005  dnibndlem6  33006  dnibndlem7  33007  dnibndlem8  33008  dnibndlem9  33009  dnibndlem10  33010  dnibndlem11  33011  dnibndlem12  33012  dnibndlem13  33013  dnibnd  33014  dnicn  33015  knoppcnlem4  33019  knoppcnlem5  33020  knoppcnlem6  33021  knoppcnlem8  33023  knoppcnlem9  33024  knoppcnlem10  33025  knoppcnlem11  33026  unblimceq0  33030  unbdqndv2lem1  33032  unbdqndv2lem2  33033  knoppndvlem1  33035  knoppndvlem6  33040  knoppndvlem8  33042  knoppndvlem9  33043  knoppndvlem10  33044  knoppndvlem11  33045  knoppndvlem12  33046  knoppndvlem14  33048  knoppndvlem15  33049  knoppndvlem17  33051  knoppndvlem18  33052  knoppndvlem19  33053  knoppndvlem20  33054  knoppndvlem21  33055  ltflcei  33940  sin2h  33942  cos2h  33943  tan2h  33944  poimirlem29  33982  opnmbllem0  33989  mblfinlem2  33991  mblfinlem3  33992  mblfinlem4  33993  mbfposadd  34000  itg2addnclem  34004  itg2addnclem2  34005  itg2addnclem3  34006  itg2addnc  34007  itg2gt0cn  34008  ibladdnc  34010  itgaddnclem2  34012  iblabsnclem  34016  iblabsnc  34017  iblmulc2nc  34018  itgmulc2nclem2  34020  itgmulc2nc  34021  itgabsnc  34022  bddiblnc  34023  ftc1cnnclem  34026  ftc1cnnc  34027  ftc1anclem1  34028  ftc1anclem2  34029  ftc1anclem3  34030  ftc1anclem4  34031  ftc1anclem5  34032  ftc1anclem6  34033  ftc1anclem7  34034  ftc1anclem8  34035  ftc1anc  34036  areacirclem1  34043  areacirclem5  34047  areacirc  34048  mettrifi  34095  lmclim2  34096  geomcau  34097  isbnd3  34125  ssbnd  34129  cntotbnd  34137  bfplem1  34163  bfplem2  34164  bfp  34165  rrnmet  34170  rrndstprj1  34171  rrndstprj2  34172  rrncmslem  34173  rrnequiv  34176  rrntotbnd  34177  ismrer1  34179  oexpreposd  38068  readdid2addid1d  38078  resubeulem1  38080  resubeulem2  38081  readdsub  38089  resubsub4  38092  resubidaddid1lem  38095  dffltz  38097  eldioph2lem1  38167  lzenom  38177  rencldnfilem  38228  irrapxlem1  38230  irrapxlem2  38231  irrapxlem3  38232  irrapxlem4  38233  irrapxlem5  38234  pellexlem2  38238  pellexlem6  38242  pell1234qrreccl  38262  pell14qrgt0  38267  pell14qrdivcl  38273  pell14qrexpclnn0  38274  pell14qrexpcl  38275  pell14qrdich  38277  pell1qrgaplem  38281  pellfundex  38294  reglogmul  38301  reglogexp  38302  reglogbas  38303  reglog1  38304  pellfund14  38306  rmspecfund  38317  monotoddzzfi  38350  expmordi  38355  jm2.24nn  38369  jm2.17a  38370  jm2.17b  38371  jm2.17c  38372  jm2.24  38373  acongrep  38390  fzmaxdif  38391  acongeq  38393  modabsdifz  38396  jm2.19lem4  38402  jm2.19  38403  jm2.26lem3  38411  jm3.1lem1  38427  jm3.1lem2  38428  itgpowd  38642  areaquad  38644  absmulrposd  39297  extoimad  39304  imo72b2lem0  39305  imo72b2lem1  39311  imo72b2  39315  int-addcomd  39316  int-addassocd  39317  int-addsimpd  39318  int-mulcomd  39319  int-mulassocd  39320  int-mulsimpd  39321  int-leftdistd  39322  int-rightdistd  39323  int-sqdefd  39324  int-mul11d  39325  int-mul12d  39326  int-add01d  39327  int-add02d  39328  int-sqgeq0d  39329  int-eqmvtd  39332  cvgdvgrat  39352  radcnvrat  39353  hashnzfzclim  39361  dvconstbi  39373  binomcxplemnn0  39388  binomcxplemnotnn0  39395  isosctrlem1ALT  39988  sineq0ALT  39991  infnsuprnmpt  40265  oddfl  40288  dstregt0  40292  zltlesub  40296  lt3addmuld  40313  fperiodmullem  40315  fperiodmul  40316  lt4addmuld  40318  fzdifsuc2  40322  supxrgere  40346  supxrgelem  40350  suplesup  40352  supsubc  40366  xralrple2  40367  abslt2sqd  40373  xralrple3  40387  reclt0d  40404  ltmulneg  40410  rexabslelem  40440  supminfrnmpt  40467  leneg2d  40471  leneg3d  40481  supminfxr  40488  absimnre  40501  absimlere  40504  iooabslt  40520  iccshift  40540  iooshift  40544  sqrlearg  40575  fmul01  40607  fmul01lt1lem1  40611  fmul01lt1lem2  40612  fprodabs2  40622  climinf  40633  limcrecl  40656  lptre2pt  40667  limcleqr  40671  0ellimcdiv  40676  limclner  40678  climleltrp  40703  climinf2mpt  40741  climinf3  40743  climxrre  40777  climliminflimsupd  40828  liminfltlem  40831  liminflimsupclim  40834  cnrefiisplem  40850  sinaover2ne0  40874  cncfperiod  40887  ioccncflimc  40893  cncficcgt0  40896  icocncflimc  40897  cncfshiftioo  40900  cncfiooicc  40902  fperdvper  40928  dvbdfbdioolem1  40938  dvbdfbdioolem2  40939  dvbdfbdioo  40940  ioodvbdlimc1lem1  40941  ioodvbdlimc1lem2  40942  ioodvbdlimc1  40943  ioodvbdlimc2lem  40944  ioodvbdlimc2  40945  dvnmul  40953  dvnprodlem1  40956  dvnprodlem2  40957  itgcoscmulx  40979  volioc  40982  itgsincmulx  40984  itgiccshift  40990  itgperiod  40991  itgsbtaddcnst  40992  volico  40994  voliooico  41003  voliccico  41010  stoweidlem7  41018  stoweidlem11  41022  stoweidlem13  41024  stoweidlem17  41028  stoweidlem19  41030  stoweidlem20  41031  stoweidlem21  41032  stoweidlem22  41033  stoweidlem23  41034  stoweidlem24  41035  stoweidlem26  41037  stoweidlem32  41043  stoweidlem36  41047  stoweidlem44  41055  stoweidlem47  41058  wallispilem3  41078  wallispi2lem1  41082  stirlinglem1  41085  stirlinglem5  41089  stirlinglem11  41095  stirlinglem12  41096  stirlinglem14  41098  dirkerval2  41105  dirkerre  41106  dirkertrigeqlem2  41110  dirkertrigeq  41112  dirkeritg  41113  dirkercncflem1  41114  dirkercncflem2  41115  dirkercncflem4  41117  fourierdlem4  41122  fourierdlem6  41124  fourierdlem7  41125  fourierdlem13  41131  fourierdlem14  41132  fourierdlem16  41134  fourierdlem18  41136  fourierdlem19  41137  fourierdlem21  41139  fourierdlem22  41140  fourierdlem24  41142  fourierdlem26  41144  fourierdlem28  41146  fourierdlem30  41148  fourierdlem35  41153  fourierdlem39  41157  fourierdlem40  41158  fourierdlem41  41159  fourierdlem42  41160  fourierdlem43  41161  fourierdlem44  41162  fourierdlem47  41164  fourierdlem48  41165  fourierdlem49  41166  fourierdlem50  41167  fourierdlem51  41168  fourierdlem53  41170  fourierdlem56  41173  fourierdlem57  41174  fourierdlem58  41175  fourierdlem59  41176  fourierdlem60  41177  fourierdlem61  41178  fourierdlem62  41179  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem66  41183  fourierdlem68  41185  fourierdlem70  41187  fourierdlem71  41188  fourierdlem72  41189  fourierdlem73  41190  fourierdlem74  41191  fourierdlem75  41192  fourierdlem76  41193  fourierdlem77  41194  fourierdlem78  41195  fourierdlem79  41196  fourierdlem80  41197  fourierdlem81  41198  fourierdlem83  41200  fourierdlem84  41201  fourierdlem85  41202  fourierdlem87  41204  fourierdlem88  41205  fourierdlem89  41206  fourierdlem90  41207  fourierdlem91  41208  fourierdlem92  41209  fourierdlem93  41210  fourierdlem95  41212  fourierdlem97  41214  fourierdlem101  41218  fourierdlem103  41220  fourierdlem104  41221  fourierdlem107  41224  fourierdlem109  41226  fourierdlem111  41228  fourierdlem112  41229  fouriercnp  41237  sqwvfoura  41239  sqwvfourb  41240  fouriersw  41242  etransclem14  41259  etransclem18  41263  etransclem23  41268  etransclem24  41269  etransclem27  41272  etransclem46  41291  etransclem48  41293  qndenserrnbllem  41305  ioorrnopnlem  41315  sge0tsms  41388  sge0cl  41389  sge0split  41417  sge0iunmptlemfi  41421  sge0rpcpnf  41429  sge0isum  41435  sge0ad2en  41439  sge0xaddlem1  41441  sge0xaddlem2  41442  sge0gtfsumgt  41451  sge0seq  41454  meadif  41487  meaiininclem  41494  carageniuncllem1  41529  carageniuncllem2  41530  hoicvrrex  41564  ovnsubaddlem1  41578  hsphoidmvle2  41593  hsphoidmvle  41594  hoidmvval0  41595  hoiprodp1  41596  hoidmv1lelem1  41599  hoidmv1lelem2  41600  hoidmv1le  41602  hoidmvlelem1  41603  hoidmvlelem2  41604  hoidmvlelem3  41605  hoiqssbllem2  41631  hspmbllem1  41634  ovolval2lem  41651  ovolval3  41655  ovolval5lem1  41660  ovnovollem1  41664  ovnovollem2  41665  vonioolem1  41688  vonioo  41690  vonicclem1  41691  vonicc  41693  smfaddlem1  41765  smflimlem4  41776  smfmullem1  41792  smfmullem2  41793  smfmullem3  41794  smfdiv  41798  smfneg  41804  sigaras  41838  sigarms  41839  sigarls  41840  sigarexp  41842  sigarperm  41843  sigarimcd  41845  sigarcol  41847  sharhght  41848  cevathlem2  41851  m1mod0mod1  42227  bgoldbtbndlem2  42524  ltsubaddb  43151  ltsubsubb  43152  ltsubadd2b  43153  flsubz  43159  fldivmod  43160  m1modmmod  43163  logblt1b  43205  dignn0fr  43242  dignn0flhalflem1  43256  dignn0flhalflem2  43257  nn0sumshdiglemA  43260  affinecomb1  43271  affinecomb2  43272  eenglngeehlnmlem1  43288  eenglngeehlnmlem2  43289  rrx2vlinest  43295  rrx2linest  43296  2sphere0  43302  line2ylem  43303  line2  43304  line2xlem  43305  line2x  43306  line2y  43307  itsclc0lem1  43308  itsclc0lem4  43311  itsclc0lem5  43312  itsclinecirc0  43314  amgmwlem  43444  amgmlemALT  43445