Theorem recnd 9404

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 9364	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 16	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1756   CCcc 9272   RRcr 9273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  00id  9536  mul02lem1  9537  addid1  9541  cnegex  9542  ltadd1  9798  leadd2  9800  ltsubadd  9801  ltsubadd2  9802  lesubadd  9803  lesubadd2  9804  lesub1  9825  lesub2  9826  ltnegcon1  9832  ltnegcon2  9833  add20  9843  subge0  9844  suble0  9845  lesub0  9848  mulge0  9849  eqord2  9863  rereccl  10041  redivcl  10042  recgt0  10165  prodgt0  10166  prodge0  10168  ltmul1a  10170  ltdiv1  10185  ltmuldiv  10194  ltrec  10205  recp1lt1  10222  recreclt  10223  ledivp1  10226  infmsup  10300  infmrcl  10301  rimul  10305  cru  10306  avglt1  10554  avglt2  10555  nn0cnd  10630  zcn  10643  zeo  10719  zcnd  10740  eluzelcn  10864  cnref1o  10978  rpcn  10991  rpcnd  11021  ltaddrp2d  11049  qbtwnre  11161  xralrple  11167  xpncan  11206  xmulcom  11221  xmulneg1  11224  xlemul1  11245  icoshftf1o  11400  lincmb01cmp  11420  iccf1o  11421  fladdz  11662  flzadd  11663  flhalf  11666  ceim1l  11678  intfracq  11690  fldiv  11691  modvalr  11703  flpmodeq  11705  mod0  11707  modlt  11710  moddiffl  11711  modfrac  11713  flmod  11714  intfrac  11715  modmulnn  11717  modvalp1  11718  modid  11724  modcyc  11735  modadd1  11737  modaddabs  11738  modadd2mod  11741  modnegd  11746  modadd12d  11747  modsub12d  11748  modaddmulmod  11757  moddi  11758  modsubdir  11759  modeqmodmin  11760  modirr  11761  seqf1olem1  11837  serle  11853  expcl2lem  11869  expnegz  11890  expaddzlem  11899  expaddz  11900  expmulz  11902  ltexp2a  11907  leexp2a  11911  leexp2r  11913  exple1  11915  expubnd  11916  sq11  11930  bernneq2  11983  expmulnbnd  11988  discr1  11992  discr  11993  faclbnd  12058  bcp1nk  12085  cshweqrep  12447  remim  12598  reim0b  12600  rereb  12601  mulre  12602  cjreb  12604  recj  12605  reneg  12606  readd  12607  resub  12608  remullem  12609  remul2  12611  rediv  12612  imcj  12613  imneg  12614  imadd  12615  imsub  12616  immul2  12618  imdiv  12619  cjcj  12621  cjadd  12622  ipcnval  12624  cjmulval  12626  cjneg  12628  imval2  12632  cjreim2  12642  sqr0lem  12722  sqrlem5  12728  sqrlem7  12730  resqrthlem  12736  remsqsqr  12738  sqrmul  12741  sqrdiv  12747  sqrneg  12749  sqrmsq  12752  absdiv  12776  absid  12777  absexp  12785  absexpz  12786  absimle  12790  abslt  12794  absle  12795  abssubne0  12796  releabs  12801  recval  12802  abstri  12810  abs2difabs  12814  abs1m  12815  abslem2  12819  absrdbnd  12821  sqreulem  12839  sqreu  12840  amgm2  12849  lo1bddrp  12995  o1lo1  13007  rlimrecl  13050  rlimge0  13051  climrecl  13053  climge0  13054  climabs0  13055  reccn2  13066  o1rlimmul  13088  lo1mul2  13098  lo1sub  13100  climle  13109  climsqz  13110  climsqz2  13111  rlimsqz  13119  rlimsqz2  13120  rlimno1  13123  climlec2  13128  isercolllem1  13134  climsup  13139  caucvgrlem  13142  caurcvgr  13143  caucvgrlem2  13144  iseraltlem1  13151  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  isumrecl  13224  isumge0  13225  fsumless  13251  fsumge1  13252  fsum00  13253  fsumle  13254  fsumlt  13255  fsumabs  13256  o1fsum  13268  seqabs  13269  cvgcmp  13271  cvgcmpce  13273  abscvgcvg  13274  isumrpcl  13298  isumle  13299  isumless  13300  isumsup  13302  climcndslem1  13304  climcndslem2  13305  climcnds  13306  flo1  13309  supcvg  13310  trireciplem  13316  trirecip  13317  explecnv  13319  geo2sum  13325  geo2lim  13327  geomulcvg  13328  cvgrat  13335  mertenslem1  13336  mertenslem2  13337  efcllem  13355  ege2le3  13367  efaddlem  13370  efgt0  13379  eftlub  13385  effsumlt  13387  eflt  13393  eflegeo  13397  resin4p  13414  recos4p  13415  retanhcl  13435  tanhlt1  13436  efeul  13438  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  sin01gt0  13466  cos01gt0  13467  sin02gt0  13468  absefi  13472  absef  13473  absefib  13474  efieq1re  13475  eirrlem  13478  rpnnen2lem5  13493  rpnnen2lem8  13496  rpnnen2lem9  13497  rpnnen2lem11  13499  rpnnen2  13500  moddvds  13534  odd2np1  13584  divalglem5  13593  bitsp1o  13621  bitsfzo  13623  bitscmp  13626  sadcaddlem  13645  nn0seqcvgd  13737  sqnprm  13776  isprm5  13790  nonsq  13829  eulerthlem2  13849  prmdiveq  13853  odzdvds  13859  pythagtriplem14  13887  pcid  13931  fldivp1  13951  pcfac  13953  pockthlem  13958  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  prmrec  13975  4sqlem5  13995  4sqlem10  14000  mul4sqlem  14006  4sqlem15  14012  4sqlem16  14013  mulgneg  15636  ghmmulg  15750  odmodnn0  16034  mndodconglem  16035  pgpfaclem2  16571  isabvd  16883  abv1z  16895  abvneg  16897  abvrec  16899  abvdiv  16900  abvdom  16901  rege0subm  17844  cnsubrg  17848  gzrngunitlem  17852  prmirredlem  17892  prmirredlemOLD  17895  remulg  18012  regsumsupp  18027  bl2in  19950  blhalf  19955  blssps  19974  blss  19975  methaus  20070  nrmmetd  20142  nm2dif  20191  nminvr  20225  nmdvr  20226  nlmmul0or  20239  nrginvrcnlem  20246  nmolb2d  20272  nmoi2  20284  nmoleub  20285  nmo0  20289  nmoeq0  20290  nmoco  20291  nmotri  20293  nmoid  20296  blcvx  20350  xrsxmet  20361  recld2  20366  reconnlem2  20379  opnreen  20383  metdstri  20402  metnrmlem3  20412  icchmeo  20488  icopnfcnv  20489  icopnfhmeo  20490  iccpnfhmeo  20492  xrhmeo  20493  icccvx  20497  cnheiborlem  20501  evth  20506  lebnumii  20513  pcoass  20571  pcorevlem  20573  pcorev2  20575  pi1xfrcnv  20604  nmoleub2lem  20644  nmoleub2lem3  20645  nmoleub3  20649  cphsqrcl2  20680  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  tchcph  20727  iscau3  20764  rrxnm  20870  rrxcph  20871  csbren  20873  trirn  20874  rrxmval  20879  rrxmetlem  20881  rrxmet  20882  rrxdstprj1  20883  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  minveclem7  20897  pjthlem1  20899  ivthlem2  20911  ivthlem3  20912  ivth2  20914  ovolfsval  20929  ovollb2lem  20946  ovolctb  20948  ovolunlem1a  20954  ovolunnul  20958  ovolfiniun  20959  ovoliunlem1  20960  ovoliun2  20964  shft2rab  20966  ovolshftlem1  20967  sca2rab  20970  ovolscalem1  20971  ovolsca  20973  ovolicc1  20974  ovolicc2lem4  20978  ovolicopnf  20982  cmmbl  20991  nulmbl  20992  nulmbl2  20993  unmbl  20994  volinun  21002  volfiniun  21003  voliunlem1  21006  voliunlem3  21008  ioombl1lem3  21016  ioombl1lem4  21017  ovolioo  21024  ioorcl2  21027  uniioovol  21034  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  uniioombllem6  21043  dyadovol  21048  dyaddisjlem  21050  opnmbllem  21056  vitalilem1  21063  vitalilem2  21064  vitalilem3  21065  vitalilem4  21066  ismbf  21083  mbfmulc2lem  21100  mbfmulc2re  21101  mbfmulc2  21116  mbfinf  21118  itg1val2  21137  itg11  21144  i1fmullem  21147  i1fadd  21148  itg1addlem4  21152  itg1addlem5  21153  i1fmulclem  21155  i1fmulc  21156  itg1mulc  21157  itg1sub  21162  itg10a  21163  itg1ge0a  21164  itg1climres  21167  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  mbfi1flimlem  21175  mbfmullem2  21177  itg2const  21193  itg2const2  21194  itg2mulclem  21199  itg2mulc  21200  itg2splitlem  21201  itg2split  21202  itg2monolem1  21203  itg2monolem3  21205  itg2addlem  21211  itgcl  21236  itgcnlem  21242  itgrevallem1  21247  itgposval  21248  iblneg  21255  itgneg  21256  i1fibl  21260  itgitg1  21261  itgconst  21271  ibladd  21273  itgaddlem2  21276  iblabslem  21280  iblabs  21281  iblabsr  21282  iblmulc2  21283  itgmulc2lem2  21285  itgmulc2  21286  itgabs  21287  itgsplit  21288  bddmulibl  21291  dvcjbr  21398  dvfre  21400  dvexp3  21425  dveflem  21426  dvferm1lem  21431  dvferm2lem  21433  rolle  21437  cmvth  21438  mvth  21439  dvlip  21440  dvlipcn  21441  c1liplem1  21443  c1lip1  21444  dveq0  21447  dv11cn  21448  dvlt0  21452  dvle  21454  dvivthlem1  21455  dvivth  21457  lhop1lem  21460  lhop1  21461  lhop2  21462  lhop  21463  dvcvx  21467  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumlem4  21476  dvfsumrlimge0  21477  dvfsumrlim2  21479  dvfsum2  21481  ftc1a  21484  ftc1lem4  21486  ftc1lem5  21487  plyeq0lem  21653  coemulhi  21696  plyrecj  21721  plydivlem3  21736  aalioulem2  21774  aalioulem3  21775  aalioulem4  21776  aalioulem5  21777  aalioulem6  21778  aaliou  21779  aaliou2  21781  aaliou2b  21782  aaliou3lem3  21785  aaliou3lem7  21790  aaliou3lem9  21791  taylthlem2  21814  ulmcn  21839  ulmdvlem1  21840  mtest  21844  mtestbdd  21845  itgulm  21848  radcnvlem1  21853  radcnvlem2  21854  radcnvlt1  21858  radcnvle  21860  dvradcnv  21861  pserulm  21862  abelthlem2  21872  abelthlem5  21875  abelthlem7  21878  abelth2  21882  reeff1olem  21886  efcvx  21889  pilem2  21892  pilem3  21893  sincosq2sgn  21936  sincosq3sgn  21937  sincosq4sgn  21938  coseq0negpitopi  21940  tanrpcl  21941  tangtx  21942  tanabsge  21943  sinq12gt0  21944  sinq34lt0t  21946  cosq14gt0  21947  cosq14ge0  21948  pige3  21954  coskpi  21957  sineq0  21958  cosordlem  21962  sinord  21965  tanord1  21968  tanord  21969  tanregt0  21970  efif1olem2  21974  efif1olem4  21976  eff1olem  21979  logrnaddcl  22001  logneg  22011  lognegb  22013  reexplog  22018  relogexp  22019  logfac  22024  efiarg  22031  cosargd  22032  cosarg0d  22033  argregt0  22034  argrege0  22035  argimgt0  22036  logneg2  22039  logmul2  22040  logdiv2  22041  abslogle  22042  tanarg  22043  logdivlti  22044  divlogrlim  22055  logcnlem2  22063  logcnlem3  22064  logcnlem4  22065  logcn  22067  logf1o2  22070  advlog  22074  advlogexp  22075  efopnlem1  22076  logtayllem  22079  logtayl  22080  logccv  22083  logcxp  22089  mulcxp  22105  divcxp  22107  cxpmul  22108  cxproot  22110  cxpmul2z  22111  abscxp  22112  abscxp2  22113  cxplt  22114  cxplea  22116  cxple2  22117  cxple2a  22119  cxplt3  22120  cxpsqrlem  22122  cxpsqr  22123  logsqr  22124  dvcxp2  22156  cxpcn3lem  22160  resqrcn  22162  cxpaddlelem  22164  cxpaddle  22165  abscxpbnd  22166  root1id  22167  root1eq1  22168  root1cj  22169  cxpeq  22170  loglesqr  22171  cosangneg2d  22178  angrtmuld  22179  ang180lem2  22181  lawcoslem1  22186  lawcos  22187  pythag  22188  isosctrlem1  22191  isosctrlem2  22192  isosctrlem3  22193  ssscongptld  22195  chordthmlem  22202  chordthmlem2  22203  chordthmlem3  22204  chordthmlem4  22205  chordthmlem5  22206  heron  22208  asinsinlem  22261  reasinsin  22266  acosrecl  22273  atancj  22280  atanrecl  22281  atanlogaddlem  22283  atanlogsublem  22285  atanbndlem  22295  atans2  22301  ressatans  22304  atantayl  22307  leibpilem2  22311  leibpi  22312  leibpisum  22313  log2tlbnd  22315  log2ublem2  22317  birthdaylem2  22321  birthdaylem3  22322  cxp2limlem  22344  cxp2lim  22345  cxploglim  22346  cxploglim2  22347  divsqrsumo1  22352  cvxcl  22353  scvxcvx  22354  jensenlem2  22356  jensen  22357  amgmlem  22358  logdiflbnd  22363  emcllem2  22365  emcllem3  22366  emcllem5  22368  emcllem6  22369  emcllem7  22370  harmonicbnd4  22379  fsumharmonic  22380  ftalem1  22385  ftalem2  22386  ftalem4  22388  ftalem5  22389  basellem3  22395  basellem4  22396  basellem5  22397  basellem6  22398  basellem7  22399  basellem8  22400  basellem9  22401  efnnfsumcl  22415  chtprm  22466  chpp1  22468  chtdif  22471  efchtdvds  22472  prmorcht  22491  mumullem2  22493  fsumfldivdiaglem  22504  ppiub  22518  chtleppi  22524  chtublem  22525  chtub  22526  pclogsum  22529  vmasum  22530  logfac2  22531  chpval2  22532  chpchtsum  22533  chpub  22534  logfaclbnd  22536  logfacbnd3  22537  logfacrlim  22538  logexprlim  22539  logfacrlim2  22540  mersenne  22541  dchrabs  22574  dchrptlem1  22578  dchrptlem2  22579  bcmax  22592  bcp1ctr  22593  bposlem1  22598  bposlem9  22606  lgsvalmod  22629  lgsdilem  22636  lgsne0  22647  lgsqrlem2  22656  lgseisenlem1  22663  lgseisenlem2  22664  lgseisen  22667  lgsquadlem1  22668  lgsquadlem2  22669  mul2sq  22679  2sqlem3  22680  2sqlem8  22686  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  chtppilimlem1  22697  chtppilimlem2  22698  chtppilim  22699  chto1ub  22700  chto1lb  22702  chpchtlim  22703  chpo1ub  22704  vmadivsum  22706  vmadivsumb  22707  rplogsumlem1  22708  rplogsumlem2  22709  rpvmasumlem  22711  dchrisumlema  22712  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusumlema  22717  dchrmusum2  22718  dchrvmasumlem1  22719  dchrvmasum2lem  22720  dchrvmasum2if  22721  dchrvmasumlem2  22722  dchrvmasumlem3  22723  dchrvmasumiflem1  22725  dchrvmasumiflem2  22726  dchrisum0flblem1  22732  dchrisum0fno1  22735  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrmusumlem  22746  dchrvmasumlem  22747  rpvmasum  22750  rplogsum  22751  dirith2  22752  mudivsum  22754  mulogsumlem  22755  mulogsum  22756  logdivsum  22757  mulog2sumlem1  22758  mulog2sumlem2  22759  mulog2sumlem3  22760  vmalogdivsum2  22762  vmalogdivsum  22763  2vmadivsumlem  22764  logsqvma  22766  logsqvma2  22767  log2sumbnd  22768  selberglem1  22769  selberglem2  22770  selberglem3  22771  selberg  22772  selbergb  22773  selberg2lem  22774  selberg2  22775  selberg2b  22776  chpdifbndlem1  22777  logdivbnd  22780  selberg3lem1  22781  selberg3lem2  22782  selberg3  22783  selberg4lem1  22784  selberg4  22785  pntrmax  22788  pntrsumo1  22789  pntrsumbnd  22790  pntrsumbnd2  22791  selbergr  22792  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntsval2  22800  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6a  22806  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntlemb  22821  pntlemg  22822  pntlemh  22823  pntlemn  22824  pntlemr  22826  pntlemj  22827  pntlemf  22829  pntlemk  22830  pntlemo  22831  pntlem3  22833  pntleml  22835  pnt2  22837  pnt  22838  abvcxp  22839  ostth2lem1  22842  qabvexp  22850  padicabv  22854  padicabvcxp  22856  ostth2lem2  22858  ostth2lem3  22859  ostth2lem4  22860  ostth2  22861  ostth3  22862  ttgcontlem1  23082  fveecn  23099  eqeelen  23101  brbtwn2  23102  colinearalglem4  23106  colinearalg  23107  axsegconlem9  23122  axsegconlem10  23123  ax5seglem1  23125  ax5seglem2  23126  ax5seglem3  23128  ax5seglem5  23130  ax5seglem6  23131  ax5seglem9  23134  ax5seg  23135  axbtwnid  23136  axpaschlem  23137  axpasch  23138  axeuclidlem  23159  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  axcontlem8  23168  eupap1  23548  nvm1  24003  nvpi  24005  nvz0  24007  nvmtri  24010  nvabs  24012  nvge0  24013  nv1  24015  smcnlem  24043  ipval2lem4  24052  ipval2  24053  4ipval2  24054  4ipval3  24058  ipidsq  24059  dipcj  24063  dip0r  24066  ipz  24068  nmoub3i  24124  nmlno0lem  24144  nmblolbii  24150  blocnilem  24155  cncph  24170  ipasslem4  24185  ipasslem5  24186  ipblnfi  24207  minvecolem2  24227  minvecolem4  24232  minvecolem6  24234  minvecolem7  24235  htthlem  24270  normpyc  24499  hhph  24531  bcs2  24535  norm1  24603  norm1exi  24604  pjhthlem1  24745  eigvalcl  25316  eighmorth  25319  nmlnop0iALT  25350  nmbdoplbi  25379  nmcexi  25381  nmcoplbi  25383  nmbdfnlbi  25404  nmcfnlbi  25407  riesz4i  25418  cnlnadjlem2  25423  cnlnadjlem7  25428  nmopcoi  25450  nmopcoadji  25456  branmfn  25460  leopnmid  25493  opsqrlem1  25495  hst1h  25582  hstle  25585  hstoh  25587  sto2i  25592  stadd3i  25603  strlem1  25605  golem1  25626  stcltrlem1  25631  cdj1i  25788  cdj3lem1  25789  cdj3lem3b  25795  cdj3i  25796  lt2addrd  25987  mul2lt0rlt0  25989  mul2lt0rgt0  25990  mul2lt0llt0  25991  mul2lt0lgt0  25992  mul2lt0bi  25993  le2halvesd  26000  fzsplit3  26029  bcm1n  26030  elunitcn  26280  sqsscirc1  26290  sqsscirc2  26291  cnre2csqima  26293  rmulccn  26310  xrge0iifcnv  26315  xrge0iifhom  26319  zrhnm  26350  nexple  26400  nnlogbexp  26415  logbrec  26416  indsum  26431  esumpcvgval  26479  dya2ub  26637  dya2icoseg  26644  eulerpartlemgc  26697  ballotlemsi  26849  sgnmul  26877  sgnsub  26879  eluzmn  26887  signsvtp  26936  signsvtn  26937  signsvfpn  26938  signsvfnn  26939  zetacvg  26953  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgambdd  26975  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  regamcl  26999  relgamcl  27000  lgam1  27002  subfacval2  27027  subfaclim  27028  subfacval3  27029  rescon  27087  sinccvglem  27268  circum  27270  possumd  27347  climlec3  27352  fprodabs  27435  iprodrecl  27453  faclimlem1  27500  faclimlem2  27501  faclimlem3  27502  faclim  27503  iprodfac  27504  faclim2  27505  bpolydiflem  28148  bpoly4  28153  supadd  28371  ltflcei  28372  sin2h  28375  cos2h  28376  tan2h  28377  opnmbllem0  28380  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  mbfposadd  28392  itg2addnclem  28396  itg2addnclem2  28397  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  ibladdnc  28402  itgaddnclem2  28404  iblabsnclem  28408  iblabsnc  28409  iblmulc2nc  28410  itgmulc2nclem2  28412  itgmulc2nc  28413  itgabsnc  28414  bddiblnc  28415  ftc1cnnclem  28418  ftc1cnnc  28419  ftc1anclem1  28420  ftc1anclem2  28421  ftc1anclem3  28422  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  areacirclem1  28437  areacirclem5  28441  areacirc  28442  nn0prpwlem  28470  mettrifi  28606  lmclim2  28607  geomcau  28608  isbnd3  28636  ssbnd  28640  cntotbnd  28648  bfplem1  28674  bfplem2  28675  bfp  28676  rrnmet  28681  rrndstprj1  28682  rrndstprj2  28683  rrncmslem  28684  rrnequiv  28687  rrntotbnd  28688  ismrer1  28690  eldioph2lem1  29051  lzenom  29061  rencldnfilem  29112  icodiamlt  29114  irrapxlem1  29116  irrapxlem2  29117  irrapxlem3  29118  irrapxlem4  29119  irrapxlem5  29120  pellexlem2  29124  pellexlem6  29128  pell1234qrreccl  29148  pell14qrgt0  29153  pell14qrdivcl  29159  pell14qrexpclnn0  29160  pell14qrexpcl  29161  pell14qrdich  29163  pell1qrgaplem  29167  pellfundex  29180  reglogmul  29187  reglogexp  29188  reglogbas  29189  reglog1  29190  pellfund14  29192  rmspecsqrnq  29200  rmspecfund  29203  rmym1  29229  rmyluc  29231  monotoddzzfi  29236  expmordi  29241  jm2.24nn  29255  jm2.17a  29256  jm2.17b  29257  jm2.17c  29258  jm2.24  29259  acongrep  29276  fzmaxdif  29277  acongeq  29279  modabsdifz  29287  jm2.19lem4  29294  jm2.19  29295  jm2.26lem3  29303  jm3.1lem1  29319  jm3.1lem2  29320  itgpowd  29543  areaquad  29545  dvconstbi  29561  fmul01  29714  fmul01lt1lem1  29718  fmul01lt1lem2  29719  climinf  29732  stoweidlem7  29755  stoweidlem11  29759  stoweidlem13  29761  stoweidlem17  29765  stoweidlem19  29767  stoweidlem20  29768  stoweidlem21  29769  stoweidlem22  29770  stoweidlem23  29771  stoweidlem24  29772  stoweidlem26  29774  stoweidlem32  29780  stoweidlem36  29784  stoweidlem44  29792  stoweidlem47  29795  wallispilem3  29815  wallispi2lem1  29819  stirlinglem1  29822  stirlinglem5  29826  stirlinglem11  29832  stirlinglem12  29833  stirlinglem14  29835  sigaras  29844  sigarms  29845  sigarls  29846  sigarexp  29848  sigarperm  29849  sigarimcd  29851  sigarcol  29853  sharhght  29854  cevathlem2  29857  isosctrlem1ALT  31557  sineq0ALT  31560