Theorem recnd 10068

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
recnd	|- ( ph -> A e. CC )

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		recn 10026	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 17	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   RRcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  00id  10211  mul02lem1  10212  addid1  10216  cnegex  10217  ltadd1  10495  leadd2  10497  ltsubadd  10498  ltsubadd2  10499  lesubadd  10500  lesubadd2  10501  lesub1  10522  lesub2  10523  ltnegcon1  10529  ltnegcon2  10530  add20  10540  subge0  10541  suble0  10542  lesub0  10545  mulge0  10546  eqord2  10559  lesub3d  10645  possumd  10652  sublt0d  10653  rereccl  10743  redivcl  10744  recgt0  10867  prodgt0  10868  prodge0  10870  ltmul1a  10872  ltdiv1  10887  ltmuldiv  10896  ltrec  10905  recp1lt1  10921  recreclt  10922  ledivp1  10925  supadd  10991  infrenegsup  11006  rimul  11011  cru  11012  avglt1  11270  avglt2  11271  lt2addmuld  11282  div4p1lem1div2  11287  nn0cnd  11353  zcn  11382  zeo  11463  zcnd  11483  eluzmn  11694  eluzelcn  11699  cnref1o  11827  rpcn  11841  rpcnd  11874  ltaddrp2d  11906  mul2lt0rlt0  11932  mul2lt0rgt0  11933  mul2lt0llt0  11934  mul2lt0lgt0  11935  mul2lt0bi  11936  qbtwnre  12030  xralrple  12036  xpncan  12081  xmulcom  12096  xmulneg1  12099  xlemul1  12120  icoshftf1o  12295  lincmb01cmp  12315  iccf1o  12316  divfl0  12625  fladdz  12626  flzadd  12627  flhalf  12631  ceim1l  12646  intfracq  12658  fldiv  12659  modvalr  12671  flpmodeq  12673  mod0  12675  modlt  12679  moddiffl  12681  modfrac  12683  flmod  12684  intfrac  12685  modmulnn  12688  modvalp1  12689  modid  12695  modcyc  12705  modadd1  12707  modaddabs  12708  modmuladdnn0  12714  negmod  12715  modadd2mod  12720  modnegd  12725  modadd12d  12726  modsub12d  12727  modmulmodr  12736  modaddmulmod  12737  moddi  12738  modsubdir  12739  modeqmodmin  12740  modirr  12741  addmodlteq  12745  seqf1olem1  12840  serle  12856  expcl2lem  12872  expnegz  12894  expaddzlem  12903  expaddz  12904  expmulz  12906  ltexp2a  12912  leexp2a  12916  leexp2r  12918  exple1  12920  expubnd  12921  sq11  12936  bernneq2  12991  expmulnbnd  12996  discr1  13000  discr  13001  faclbnd  13077  bcp1nk  13104  cshweqrep  13567  remim  13857  reim0b  13859  rereb  13860  mulre  13861  cjreb  13863  recj  13864  reneg  13865  readd  13866  resub  13867  remullem  13868  remul2  13870  rediv  13871  imcj  13872  imneg  13873  imadd  13874  imsub  13875  immul2  13877  imdiv  13878  cjcj  13880  cjadd  13881  ipcnval  13883  cjmulval  13885  cjneg  13887  imval2  13891  cjreim2  13901  sqr0lem  13981  sqrlem5  13987  sqrlem7  13989  resqrtthlem  13995  remsqsqrt  13997  sqrtmul  14000  sqrtdiv  14006  sqrtneg  14008  sqrtmsq  14011  absdiv  14035  absid  14036  absexp  14044  absexpz  14045  absimle  14049  abslt  14054  absle  14055  abssubne0  14056  releabs  14061  recval  14062  abstri  14070  abs2difabs  14074  abs1m  14075  abslem2  14079  absrdbnd  14081  sqreulem  14099  sqreu  14100  amgm2  14109  icodiamlt  14174  lo1bddrp  14256  o1lo1  14268  rlimrecl  14311  rlimge0  14312  climrecl  14314  climge0  14315  climabs0  14316  reccn2  14327  o1rlimmul  14349  lo1mul2  14359  lo1sub  14361  climle  14370  climsqz  14371  climsqz2  14372  rlimsqz  14380  rlimsqz2  14381  climlec2  14389  isercolllem1  14395  climsup  14400  caucvgrlem  14403  caurcvgr  14404  caucvgrlem2  14405  iseraltlem1  14412  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  isumrecl  14496  isumge0  14497  fsumless  14528  fsumge1  14529  fsum00  14530  fsumle  14531  fsumlt  14532  fsumabs  14533  o1fsum  14545  seqabs  14546  cvgcmp  14548  cvgcmpce  14550  abscvgcvg  14551  isumrpcl  14575  isumle  14576  isumless  14577  isumsup  14579  climcndslem1  14581  climcndslem2  14582  climcnds  14583  flo1  14586  supcvg  14588  trireciplem  14594  trirecip  14595  explecnv  14597  geo2sum  14604  geo2lim  14606  geomulcvg  14607  cvgrat  14615  mertenslem1  14616  mertenslem2  14617  fprodabs  14704  fprodle  14727  iprodrecl  14733  bpolydiflem  14785  bpoly4  14790  efcllem  14808  ege2le3  14820  efaddlem  14823  efgt0  14833  eftlub  14839  effsumlt  14841  eflt  14847  eflegeo  14851  resin4p  14868  recos4p  14869  retanhcl  14889  tanhlt1  14890  efeul  14892  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  absefi  14926  absef  14927  absefib  14928  efieq1re  14929  eirrlem  14932  rpnnen2lem5  14947  rpnnen2lem8  14950  rpnnen2lem9  14951  rpnnen2lem11  14953  rpnnen2lem12  14954  moddvds  14991  odd2np1  15065  divalglem5  15120  bitsp1o  15155  bitsfzo  15157  bitscmp  15160  sadcaddlem  15179  nn0seqcvgd  15283  sqnprm  15414  isprm5  15419  nonsq  15467  eulerthlem2  15487  prmdiveq  15491  odzdvds  15500  vfermltlALT  15507  pythagtriplem14  15533  pcid  15577  fldivp1  15601  pcfac  15603  pockthlem  15609  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmrec  15626  4sqlem5  15646  4sqlem10  15651  mul4sqlem  15657  4sqlem15  15663  4sqlem16  15664  mulgneg  17560  ghmmulg  17672  odmodnn0  17959  mndodconglem  17960  pgpfaclem2  18481  isabvd  18820  abv1z  18832  abvneg  18834  abvrec  18836  abvdiv  18837  abvdom  18838  rege0subm  19802  cnsubrg  19806  gzrngunitlem  19811  regsumfsum  19814  prmirredlem  19841  remulg  19953  regsumsupp  19968  bl2in  22205  blhalf  22210  blssps  22229  blss  22230  methaus  22325  nrmmetd  22379  nm2dif  22429  nminvr  22473  nmdvr  22474  nlmmul0or  22487  nrginvrcnlem  22495  nmolb2d  22522  nmoi2  22534  nmoleub  22535  nmo0  22539  nmoeq0  22540  nmoco  22541  nmotri  22543  nmoid  22546  blcvx  22601  xrsxmet  22612  recld2  22617  reconnlem2  22630  opnreen  22634  metdstri  22654  metnrmlem3  22664  icchmeo  22740  icopnfcnv  22741  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  icccvx  22749  cnheiborlem  22753  evth  22758  lebnumii  22765  pcoass  22824  pcorevlem  22826  pcorev2  22828  pi1xfrcnv  22857  nmoleub2lem  22914  nmoleub2lem3  22915  nmoleub3  22919  ncvsm1  22954  ncvspi  22956  ncvs1  22957  cphsqrtcl2  22986  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  tchcph  23036  cphipval2  23040  cphipval  23042  iscau3  23076  rrxnm  23179  rrxcph  23180  csbren  23182  trirn  23183  rrxmval  23188  rrxmetlem  23190  rrxmet  23191  rrxdstprj1  23192  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  minveclem7  23206  pjthlem1  23208  ivthlem2  23221  ivthlem3  23222  ivth2  23224  ovolfsval  23239  ovollb2lem  23256  ovolctb  23258  ovolunlem1a  23264  ovolunnul  23268  ovolfiniun  23269  ovoliunlem1  23270  ovoliun2  23274  shft2rab  23276  ovolshftlem1  23277  sca2rab  23280  ovolscalem1  23281  ovolsca  23283  ovolicc1  23284  ovolicc2lem4  23288  ovolicopnf  23292  cmmbl  23302  nulmbl  23303  nulmbl2  23304  unmbl  23305  volinun  23314  volfiniun  23315  voliunlem1  23318  voliunlem3  23320  ioombl1lem3  23328  ioombl1lem4  23329  ovolioo  23336  ioorcl2  23340  uniioovol  23347  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombllem6  23356  dyadovol  23361  dyaddisjlem  23363  opnmbllem  23369  vitalilem1  23376  vitalilem1OLD  23377  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  ismbf  23397  mbfmulc2lem  23414  mbfmulc2re  23415  mbfmulc2  23430  mbfinf  23432  itg1val2  23451  itg11  23458  i1fmullem  23461  i1fadd  23462  itg1addlem4  23466  itg1addlem5  23467  i1fmulclem  23469  i1fmulc  23470  itg1mulc  23471  itg1sub  23476  itg10a  23477  itg1ge0a  23478  itg1climres  23481  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfmullem2  23491  itg2const  23507  itg2const2  23508  itg2mulclem  23513  itg2mulc  23514  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2monolem3  23519  itg2addlem  23525  itgcl  23550  itgcnlem  23556  itgrevallem1  23561  itgposval  23562  iblneg  23569  itgneg  23570  i1fibl  23574  itgitg1  23575  itgconst  23585  ibladd  23587  itgaddlem2  23590  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2lem2  23599  itgmulc2  23600  itgabs  23601  itgsplit  23602  bddmulibl  23605  dvcjbr  23712  dvfre  23714  dvexp3  23741  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  c1liplem1  23759  c1lip1  23760  dveq0  23763  dv11cn  23764  dvlt0  23768  dvle  23770  dvivthlem1  23771  dvivth  23773  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem4  23792  dvfsumrlimge0  23793  dvfsumrlim2  23795  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  ftc1lem5  23803  plyeq0lem  23966  coemulhi  24010  plyrecj  24035  plydivlem3  24050  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  aalioulem5  24091  aalioulem6  24092  aaliou  24093  aaliou2  24095  aaliou2b  24096  aaliou3lem3  24099  aaliou3lem7  24104  aaliou3lem9  24105  taylthlem2  24128  ulmcn  24153  ulmdvlem1  24154  mtest  24158  mtestbdd  24159  itgulm  24162  radcnvlem1  24167  radcnvlem2  24168  radcnvlt1  24172  radcnvle  24174  dvradcnv  24175  pserulm  24176  abelthlem2  24186  abelthlem5  24189  abelthlem7  24192  abelth2  24196  reeff1olem  24200  efcvx  24203  pilem2  24206  pilem3  24207  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  coseq0negpitopi  24255  tanrpcl  24256  tangtx  24257  tanabsge  24258  sinq12gt0  24259  sinq34lt0t  24261  cosq14gt0  24262  cosq14ge0  24263  pige3  24269  coskpi  24272  cosordlem  24277  sinord  24280  tanord1  24283  tanord  24284  tanregt0  24285  efif1olem2  24289  efif1olem4  24291  eff1olem  24294  rzgrp  24300  logrnaddcl  24321  logneg  24334  lognegb  24336  reexplog  24341  relogexp  24342  logfac  24347  efiarg  24353  cosargd  24354  cosarg0d  24355  argregt0  24356  argrege0  24357  argimgt0  24358  logneg2  24361  logmul2  24362  logdiv2  24363  abslogle  24364  tanarg  24365  logdivlti  24366  divlogrlim  24381  logcnlem2  24389  logcnlem3  24390  logcnlem4  24391  logcn  24393  logf1o2  24396  advlog  24400  advlogexp  24401  efopnlem1  24402  logtayllem  24405  logtayl  24406  logccv  24409  logcxp  24415  mulcxp  24431  divcxp  24433  cxpmul  24434  cxproot  24436  cxpmul2z  24437  abscxp  24438  abscxp2  24439  cxplt  24440  cxplea  24442  cxple2  24443  cxple2a  24445  cxplt3  24446  cxpsqrtlem  24448  cxpsqrt  24449  logsqrt  24450  dvcxp2  24482  cxpcn3lem  24488  resqrtcn  24490  cxpaddlelem  24492  cxpaddle  24493  abscxpbnd  24494  root1id  24495  root1eq1  24496  root1cj  24497  cxpeq  24498  loglesqrt  24499  relogbmul  24515  nnlogbexp  24519  logbrec  24520  cosangneg2d  24537  angrtmuld  24538  ang180lem2  24540  lawcoslem1  24545  lawcos  24546  pythag  24547  isosctrlem1  24548  isosctrlem2  24549  isosctrlem3  24550  ssscongptld  24552  chordthmlem  24559  chordthmlem2  24560  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  heron  24565  asinsinlem  24618  reasinsin  24623  acosrecl  24630  atancj  24637  atanrecl  24638  atanlogaddlem  24640  atanlogsublem  24642  atanbndlem  24652  atans2  24658  ressatans  24661  atantayl  24664  leibpilem2  24668  leibpi  24669  leibpisum  24670  log2tlbnd  24672  log2ublem2  24674  birthdaylem2  24679  birthdaylem3  24680  cxp2limlem  24702  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  divsqrtsumo1  24710  cvxcl  24711  scvxcvx  24712  jensenlem2  24714  jensen  24715  amgmlem  24716  logdiflbnd  24721  emcllem2  24723  emcllem3  24724  emcllem5  24726  emcllem6  24727  emcllem7  24728  harmonicbnd4  24737  fsumharmonic  24738  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgambdd  24763  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  regamcl  24787  relgamcl  24788  lgam1  24790  ftalem1  24799  ftalem2  24800  ftalem4  24802  ftalem5  24803  basellem3  24809  basellem4  24810  basellem5  24811  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  efnnfsumcl  24829  chtprm  24879  chpp1  24881  chtdif  24884  efchtdvds  24885  prmorcht  24904  mumullem2  24906  fsumfldivdiaglem  24915  ppiub  24929  chtleppi  24935  chtublem  24936  chtub  24937  pclogsum  24940  vmasum  24941  logfac2  24942  chpval2  24943  chpchtsum  24944  chpub  24945  logfaclbnd  24947  logfacbnd3  24948  logfacrlim  24949  logexprlim  24950  logfacrlim2  24951  mersenne  24952  dchrabs  24985  dchrptlem1  24989  dchrptlem2  24990  bcmax  25003  bcp1ctr  25004  bposlem1  25009  bposlem9  25017  lgsvalmod  25041  lgsdilem  25049  lgsne0  25060  lgsqrlem2  25072  gausslemma2dlem1a  25090  gausslemma2dlem6  25097  lgseisenlem1  25100  lgseisenlem2  25101  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  mul2sq  25144  2sqlem3  25145  2sqlem8  25151  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chto1ub  25165  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  vmadivsum  25171  vmadivsumb  25172  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlema  25177  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrmusumlem  25211  dchrvmasumlem  25212  rpvmasum  25215  rplogsum  25216  dirith2  25217  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  logdivsum  25222  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma  25231  logsqvma2  25232  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberglem3  25236  selberg  25237  selbergb  25238  selberg2lem  25239  selberg2  25240  selberg2b  25241  chpdifbndlem1  25242  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrmax  25253  pntrsumo1  25254  pntrsumbnd  25255  pntrsumbnd2  25256  selbergr  25257  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntsval2  25265  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6a  25271  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntibndlem3  25281  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemn  25289  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntlem3  25298  pntleml  25300  pnt2  25302  pnt  25303  abvcxp  25304  ostth2lem1  25307  qabvexp  25315  padicabv  25319  padicabvcxp  25321  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  ostth3  25327  ttgcontlem1  25765  fveecn  25782  eqeelen  25784  brbtwn2  25785  colinearalglem4  25789  colinearalg  25790  axsegconlem9  25805  axsegconlem10  25806  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem6  25814  ax5seglem9  25817  ax5seg  25818  axbtwnid  25819  axpaschlem  25820  axpasch  25821  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  nvm1  27520  nvpi  27522  nvz0  27523  nvmtri  27526  nvabs  27527  nvge0  27528  nv1  27530  smcnlem  27552  ipval2lem4  27561  ipval2  27562  4ipval2  27563  ipidsq  27565  dipcj  27569  dip0r  27572  ipz  27574  nmoub3i  27628  nmlno0lem  27648  nmblolbii  27654  blocnilem  27659  cncph  27674  ipasslem4  27689  ipasslem5  27690  ipblnfi  27711  minvecolem2  27731  minvecolem4  27736  minvecolem6  27738  minvecolem7  27739  htthlem  27774  normpyc  28003  hhph  28035  bcs2  28039  norm1  28106  norm1exi  28107  pjhthlem1  28250  eigvalcl  28820  eighmorth  28823  nmlnop0iALT  28854  nmbdoplbi  28883  nmcexi  28885  nmcoplbi  28887  nmbdfnlbi  28908  nmcfnlbi  28911  riesz4i  28922  cnlnadjlem2  28927  cnlnadjlem7  28932  nmopcoi  28954  nmopcoadji  28960  branmfn  28964  leopnmid  28997  opsqrlem1  28999  hst1h  29086  hstle  29089  hstoh  29091  sto2i  29096  stadd3i  29107  strlem1  29109  golem1  29130  stcltrlem1  29135  cdj1i  29292  cdj3lem1  29293  cdj3lem3b  29299  cdj3i  29300  lt2addrd  29516  le2halvesd  29520  fzsplit3  29553  bcm1n  29554  fsumiunle  29575  bhmafibid1  29644  bhmafibid2  29645  2sqmod  29648  psgnfzto1stlem  29850  elunitcn  29944  sqsscirc1  29954  sqsscirc2  29955  cnre2csqima  29957  rmulccn  29974  xrge0iifcnv  29979  xrge0iifhom  29983  zrhnm  30013  rezh  30015  nexple  30071  indsum  30083  esumpcvgval  30140  esumcvgsum  30150  dya2ub  30332  dya2icoseg  30339  omssubadd  30362  eulerpartlemgc  30424  ballotlemsi  30576  sgnmul  30604  sgnsub  30606  plymulx0  30624  signsply0  30628  signsvtp  30660  signsvtn  30661  signsvfpn  30662  signsvfnn  30663  divsqrtid  30672  reprgt  30699  reprinfz1  30700  breprexplemc  30710  circlemethhgt  30721  hgt750lemd  30726  hgt750lemf  30731  hgt750lemg  30732  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  subfacval2  31169  subfaclim  31170  subfacval3  31171  resconn  31228  sinccvglem  31566  circum  31568  climlec3  31619  faclimlem1  31629  faclimlem2  31630  faclimlem3  31631  faclim  31632  iprodfac  31633  faclim2  31634  dnicld1  32462  dnizeq0  32465  dnizphlfeqhlf  32466  dnibndlem2  32469  dnibndlem3  32470  dnibndlem5  32472  dnibndlem6  32473  dnibndlem7  32474  dnibndlem8  32475  dnibndlem9  32476  dnibndlem10  32477  dnibndlem11  32478  dnibndlem12  32479  dnibndlem13  32480  dnibnd  32481  dnicn  32482  knoppcnlem4  32486  knoppcnlem5  32487  knoppcnlem6  32488  knoppcnlem8  32490  knoppcnlem9  32491  knoppcnlem10  32492  knoppcnlem11  32493  unblimceq0  32498  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem1  32503  knoppndvlem6  32508  knoppndvlem8  32510  knoppndvlem9  32511  knoppndvlem10  32512  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem20  32522  knoppndvlem21  32523  ltflcei  33397  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem29  33438  opnmbllem0  33445  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  mbfposadd  33457  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ibladdnc  33467  itgaddnclem2  33469  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  bddiblnc  33480  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem1  33500  areacirclem5  33504  areacirc  33505  mettrifi  33553  lmclim2  33554  geomcau  33555  isbnd3  33583  ssbnd  33587  cntotbnd  33595  bfplem1  33621  bfplem2  33622  bfp  33623  rrnmet  33628  rrndstprj1  33629  rrndstprj2  33630  rrncmslem  33631  rrnequiv  33634  rrntotbnd  33635  ismrer1  33637  eldioph2lem1  37323  lzenom  37333  rencldnfilem  37384  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell1234qrreccl  37418  pell14qrgt0  37423  pell14qrdivcl  37429  pell14qrexpclnn0  37430  pell14qrexpcl  37431  pell14qrdich  37433  pell1qrgaplem  37437  pellfundex  37450  reglogmul  37457  reglogexp  37458  reglogbas  37459  reglog1  37460  pellfund14  37462  rmspecsqrtnqOLD  37471  rmspecfund  37474  monotoddzzfi  37507  expmordi  37512  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  jm2.24  37530  acongrep  37547  fzmaxdif  37548  acongeq  37550  modabsdifz  37553  jm2.19lem4  37559  jm2.19  37560  jm2.26lem3  37568  jm3.1lem1  37584  jm3.1lem2  37585  itgpowd  37800  areaquad  37802  absmulrposd  38457  extoimad  38464  imo72b2lem0  38465  imo72b2lem1  38471  imo72b2  38475  int-addcomd  38476  int-addassocd  38477  int-addsimpd  38478  int-mulcomd  38479  int-mulassocd  38480  int-mulsimpd  38481  int-leftdistd  38482  int-rightdistd  38483  int-sqdefd  38484  int-mul11d  38485  int-mul12d  38486  int-add01d  38487  int-add02d  38488  int-sqgeq0d  38489  int-eqmvtd  38492  cvgdvgrat  38512  radcnvrat  38513  hashnzfzclim  38521  dvconstbi  38533  binomcxplemnn0  38548  binomcxplemnotnn0  38555  isosctrlem1ALT  39170  sineq0ALT  39173  infnsuprnmpt  39465  oddfl  39489  dstregt0  39493  zltlesub  39497  lt3addmuld  39515  fperiodmullem  39517  fperiodmul  39518  lt4addmuld  39520  fzdifsuc2  39525  supxrgere  39549  supxrgelem  39553  suplesup  39555  supsubc  39569  xralrple2  39570  abslt2sqd  39576  xralrple3  39590  reclt0d  39607  ltmulneg  39615  rexabslelem  39645  supminfrnmpt  39672  leneg2d  39676  leneg3d  39687  supminfxr  39694  absimnre  39707  absimlere  39710  iooabslt  39721  iccshift  39744  iooshift  39748  sqrlearg  39780  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fprodabs2  39827  climinf  39838  limcrecl  39861  lptre2pt  39872  limcleqr  39876  0ellimcdiv  39881  limclner  39883  climleltrp  39908  climinf2mpt  39946  climinf3  39948  climxrre  39982  climliminflimsupd  40033  liminfltlem  40036  liminflimsupclim  40039  cnrefiisplem  40055  sinaover2ne0  40079  cncfperiod  40092  ioccncflimc  40098  cncficcgt0  40101  icocncflimc  40102  cncfshiftioo  40105  cncfiooicc  40107  fperdvper  40133  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  itgcoscmulx  40185  volioc  40188  itgsincmulx  40190  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  volico  40200  voliooico  40209  voliccico  40216  stoweidlem7  40224  stoweidlem11  40228  stoweidlem13  40230  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem21  40238  stoweidlem22  40239  stoweidlem23  40240  stoweidlem24  40241  stoweidlem26  40243  stoweidlem32  40249  stoweidlem36  40253  stoweidlem44  40261  stoweidlem47  40264  wallispilem3  40284  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem5  40295  stirlinglem11  40301  stirlinglem12  40302  stirlinglem14  40304  dirkerval2  40311  dirkerre  40312  dirkertrigeqlem2  40316  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem6  40330  fourierdlem7  40331  fourierdlem13  40337  fourierdlem14  40338  fourierdlem16  40340  fourierdlem18  40342  fourierdlem19  40343  fourierdlem21  40345  fourierdlem22  40346  fourierdlem24  40348  fourierdlem26  40350  fourierdlem28  40352  fourierdlem30  40354  fourierdlem35  40359  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem43  40367  fourierdlem44  40368  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem53  40376  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem70  40393  fourierdlem71  40394  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem77  40400  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem83  40406  fourierdlem84  40407  fourierdlem85  40408  fourierdlem87  40410  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem109  40432  fourierdlem111  40434  fourierdlem112  40435  fouriercnp  40443  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem14  40465  etransclem18  40469  etransclem23  40474  etransclem24  40475  etransclem27  40478  etransclem46  40497  etransclem48  40499  qndenserrnbllem  40514  ioorrnopnlem  40524  sge0tsms  40597  sge0cl  40598  sge0split  40626  sge0iunmptlemfi  40630  sge0rpcpnf  40638  sge0isum  40644  sge0ad2en  40648  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0gtfsumgt  40660  sge0seq  40663  meadif  40696  meaiininclem  40700  carageniuncllem1  40735  carageniuncllem2  40736  hoicvrrex  40770  ovnsubaddlem1  40784  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmvval0  40801  hoiprodp1  40802  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoiqssbllem2  40837  hspmbllem1  40840  ovolval2lem  40857  ovolval3  40861  ovolval5lem1  40866  ovnovollem1  40870  ovnovollem2  40871  vonioolem1  40894  vonioo  40896  vonicclem1  40897  vonicc  40899  smfaddlem1  40971  smflimlem4  40982  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  smfdiv  41004  smfneg  41010  sigaras  41044  sigarms  41045  sigarls  41046  sigarexp  41048  sigarperm  41049  sigarimcd  41051  sigarcol  41053  sharhght  41054  cevathlem2  41057  m1mod0mod1  41339  bgoldbtbndlem2  41694  ltsubaddb  42304  ltsubsubb  42305  ltsubadd2b  42306  flsubz  42312  fldivmod  42313  m1modmmod  42316  logblt1b  42358  dignn0fr  42395  dignn0flhalflem1  42409  dignn0flhalflem2  42410  nn0sumshdiglemA  42413  amgmwlem  42548  amgmlemALT  42549