Theorem recnd 9070

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

Syntax hints:   -> wi 4   e. wcel 1721   CCcc 8944   RRcr 8945

This theorem is referenced by:  00id  9197  mul02lem1  9198  addid1  9202  cnegex  9203  ltadd1  9451  leadd2  9453  ltsubadd  9454  ltsubadd2  9455  lesubadd  9456  lesubadd2  9457  lesub1  9478  lesub2  9479  ltnegcon1  9485  ltnegcon2  9486  add20  9496  subge0  9497  suble0  9498  lesub0  9500  mulge0  9501  eqord2  9514  rereccl  9688  redivcl  9689  recgt0  9810  prodgt0  9811  prodge0  9813  ltmul1a  9815  ltdiv1  9830  ltmuldiv  9836  ltrec  9847  recp1lt1  9864  recreclt  9865  ledivp1  9868  infmsup  9942  infmrcl  9943  rimul  9947  cru  9948  avglt1  10161  avglt2  10162  nn0cnd  10232  zcn  10243  zeo  10311  zcnd  10332  cnref1o  10563  rpcn  10576  rpcnd  10606  ltaddrp2d  10634  qbtwnre  10741  xralrple  10747  xpncan  10786  xmulcom  10801  xmulneg1  10804  xlemul1  10825  icoshftf1o  10976  lincmb01cmp  10994  iccf1o  10995  fladdz  11182  flzadd  11183  flhalf  11186  ceim1l  11189  intfracq  11195  fldiv  11196  mod0  11210  modlt  11213  moddiffl  11214  modfrac  11216  flmod  11217  intfrac  11218  modmulnn  11220  modid  11225  modcyc  11231  modadd1  11233  modnegd  11236  modadd12d  11237  modsub12d  11238  moddi  11239  modsubdir  11240  modirr  11241  seqf1olem1  11317  serle  11333  expcl2lem  11348  expnegz  11369  expaddzlem  11378  expaddz  11379  expmulz  11381  ltexp2a  11386  leexp2a  11390  leexp2r  11392  exple1  11394  expubnd  11395  sq11  11409  bernneq2  11461  expmulnbnd  11466  discr1  11470  discr  11471  faclbnd  11536  bcp1nk  11563  remim  11877  reim0b  11879  rereb  11880  mulre  11881  cjreb  11883  recj  11884  reneg  11885  readd  11886  resub  11887  remullem  11888  remul2  11890  rediv  11891  imcj  11892  imneg  11893  imadd  11894  imsub  11895  immul2  11897  imdiv  11898  cjcj  11900  cjadd  11901  ipcnval  11903  cjmulval  11905  cjneg  11907  imval2  11911  cjreim2  11921  sqr0lem  12001  sqrlem5  12007  sqrlem7  12009  resqrthlem  12015  remsqsqr  12017  sqrmul  12020  sqrdiv  12026  sqrneg  12028  sqrmsq  12031  absdiv  12055  absid  12056  absexp  12064  absexpz  12065  absimle  12069  abslt  12073  absle  12074  abssubne0  12075  releabs  12080  recval  12081  abstri  12089  abs2difabs  12093  abs1m  12094  abslem2  12098  absrdbnd  12100  sqreulem  12118  sqreu  12119  amgm2  12128  lo1bddrp  12274  o1lo1  12286  rlimrecl  12329  rlimge0  12330  climrecl  12332  climge0  12333  climabs0  12334  reccn2  12345  o1rlimmul  12367  lo1mul2  12377  lo1sub  12379  climle  12388  climsqz  12389  climsqz2  12390  rlimsqz  12398  rlimsqz2  12399  rlimno1  12402  climlec2  12407  isercolllem1  12413  climsup  12418  caucvgrlem  12421  caurcvgr  12422  caucvgrlem2  12423  iseraltlem1  12430  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  isumrecl  12504  isumge0  12505  fsumless  12530  fsumge1  12531  fsum00  12532  fsumle  12533  fsumlt  12534  fsumabs  12535  o1fsum  12547  seqabs  12548  cvgcmp  12550  cvgcmpce  12552  abscvgcvg  12553  isumrpcl  12578  isumle  12579  isumless  12580  isumsup  12582  climcndslem1  12584  climcndslem2  12585  climcnds  12586  flo1  12589  supcvg  12590  trireciplem  12596  trirecip  12597  explecnv  12599  geo2sum  12605  geo2lim  12607  geomulcvg  12608  cvgrat  12615  mertenslem1  12616  mertenslem2  12617  efcllem  12635  ege2le3  12647  efaddlem  12650  efgt0  12659  eftlub  12665  effsumlt  12667  eflt  12673  eflegeo  12677  resin4p  12694  recos4p  12695  retanhcl  12715  tanhlt1  12716  efeul  12718  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  absefi  12752  absef  12753  absefib  12754  efieq1re  12755  eirrlem  12758  rpnnen2lem5  12773  rpnnen2lem8  12776  rpnnen2lem9  12777  rpnnen2lem11  12779  rpnnen2  12780  moddvds  12814  odd2np1  12863  divalglem5  12872  bitsp1o  12900  bitsfzo  12902  bitscmp  12905  sadcaddlem  12924  nn0seqcvgd  13016  sqnprm  13053  isprm5  13067  nonsq  13106  eulerthlem2  13126  prmdiveq  13130  odzdvds  13136  pythagtriplem14  13157  pcid  13201  fldivp1  13221  pcfac  13223  pockthlem  13228  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  prmrec  13245  4sqlem5  13265  4sqlem10  13270  mul4sqlem  13276  4sqlem15  13282  4sqlem16  13283  mulgneg  14863  ghmmulg  14973  odmodnn0  15133  mndodconglem  15134  pgpfaclem2  15595  isabvd  15863  abv1z  15875  abvneg  15877  abvrec  15879  abvdiv  15880  abvdom  15881  rege0subm  16710  cnsubrg  16714  gzrngunitlem  16718  prmirredlem  16728  bl2in  18383  blhalf  18388  blssps  18407  blss  18408  methaus  18503  nrmmetd  18575  nm2dif  18624  nminvr  18658  nmdvr  18659  nlmmul0or  18672  nrginvrcnlem  18679  nmolb2d  18705  nmoi2  18717  nmoleub  18718  nmo0  18722  nmoeq0  18723  nmoco  18724  nmotri  18726  nmoid  18729  blcvx  18782  xrsxmet  18793  recld2  18798  reconnlem2  18811  opnreen  18815  metdstri  18834  metnrmlem3  18844  iihalf2cn  18912  icchmeo  18919  icopnfcnv  18920  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  icccvx  18928  cnheiborlem  18932  evth  18937  lebnumii  18944  pcoass  19002  pcorevlem  19004  pcorev2  19006  pi1xfrcnv  19035  nmoleub2lem  19075  nmoleub2lem3  19076  nmoleub3  19080  cphsqrcl2  19102  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  tchcph  19147  iscau3  19184  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  minveclem7  19289  pjthlem1  19291  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ovolfsval  19320  ovollb2lem  19337  ovolctb  19339  ovolunlem1a  19345  ovolunnul  19349  ovolfiniun  19350  ovoliunlem1  19351  ovoliun2  19355  shft2rab  19357  ovolshftlem1  19358  sca2rab  19361  ovolscalem1  19362  ovolsca  19364  ovolicc1  19365  ovolicc2lem4  19369  ovolicopnf  19373  cmmbl  19382  nulmbl  19383  nulmbl2  19384  unmbl  19385  volinun  19393  volfiniun  19394  voliunlem1  19397  voliunlem3  19399  ioombl1lem3  19407  ioombl1lem4  19408  ovolioo  19415  ioorcl2  19417  uniioovol  19424  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  dyadovol  19438  dyaddisjlem  19440  opnmbllem  19446  vitalilem1  19453  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  ismbf  19475  mbfmulc2lem  19492  mbfmulc2re  19493  mbfpos  19496  mbfmulc2  19508  mbfinf  19510  itg1val2  19529  itg11  19536  i1fmullem  19539  i1fadd  19540  itg1addlem4  19544  itg1addlem5  19545  i1fmulclem  19547  i1fmulc  19548  itg1mulc  19549  itg1sub  19554  itg10a  19555  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfmullem2  19569  itg2const  19585  itg2const2  19586  itg2mulclem  19591  itg2mulc  19592  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem3  19597  itg2addlem  19603  itgcl  19628  itgcnlem  19634  itgrevallem1  19639  itgposval  19640  iblneg  19647  itgneg  19648  i1fibl  19652  itgitg1  19653  itgconst  19663  ibladd  19665  itgaddlem2  19668  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem2  19677  itgmulc2  19678  itgabs  19679  itgsplit  19680  bddmulibl  19683  dvcjbr  19788  dvfre  19790  dvexp3  19815  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  c1liplem1  19833  c1lip1  19834  dveq0  19837  dv11cn  19838  dvlt0  19842  dvle  19844  dvivthlem1  19845  dvivth  19847  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlimge0  19867  dvfsumrlim2  19869  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  ftc1lem5  19877  plyeq0lem  20082  coemulhi  20125  plyrecj  20150  plydivlem3  20165  aalioulem2  20203  aalioulem3  20204  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou2  20210  aaliou2b  20211  aaliou3lem3  20214  aaliou3lem7  20219  aaliou3lem9  20220  taylthlem2  20243  ulmcn  20268  ulmdvlem1  20269  mtest  20273  mtestbdd  20274  itgulm  20277  radcnvlem1  20282  radcnvlem2  20283  radcnvlt1  20287  radcnvle  20289  dvradcnv  20290  pserulm  20291  abelthlem2  20301  abelthlem5  20304  abelthlem7  20307  abelth2  20311  reeff1olem  20315  efcvx  20318  pilem2  20321  pilem3  20322  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  coseq0negpitopi  20364  tanrpcl  20365  tangtx  20366  tanabsge  20367  sinq12gt0  20368  sinq34lt0t  20370  cosq14gt0  20371  cosq14ge0  20372  pige3  20378  coskpi  20381  sineq0  20382  cosordlem  20386  sinord  20389  tanord1  20392  tanord  20393  tanregt0  20394  efif1olem2  20398  efif1olem4  20400  eff1olem  20403  logrnaddcl  20425  logneg  20435  lognegb  20437  reexplog  20442  relogexp  20443  logfac  20448  efiarg  20455  cosargd  20456  cosarg0d  20457  argregt0  20458  argrege0  20459  argimgt0  20460  logneg2  20463  logmul2  20464  logdiv2  20465  abslogle  20466  tanarg  20467  logdivlti  20468  divlogrlim  20479  logcnlem2  20487  logcnlem3  20488  logcnlem4  20489  logcn  20491  logf1o2  20494  advlog  20498  advlogexp  20499  efopnlem1  20500  logtayllem  20503  logtayl  20504  logccv  20507  logcxp  20513  mulcxp  20529  divcxp  20531  cxpmul  20532  cxproot  20534  cxpmul2z  20535  abscxp  20536  abscxp2  20537  cxplt  20538  cxplea  20540  cxple2  20541  cxple2a  20543  cxplt3  20544  cxpsqrlem  20546  cxpsqr  20547  logsqr  20548  dvcxp2  20580  cxpcn3lem  20584  resqrcn  20586  cxpaddlelem  20588  cxpaddle  20589  abscxpbnd  20590  root1id  20591  root1eq1  20592  root1cj  20593  cxpeq  20594  loglesqr  20595  cosangneg2d  20602  angrtmuld  20603  ang180lem2  20605  lawcoslem1  20610  lawcos  20611  pythag  20612  isosctrlem1  20615  isosctrlem2  20616  isosctrlem3  20617  ssscongptld  20619  chordthmlem  20626  chordthmlem2  20627  chordthmlem3  20628  chordthmlem4  20629  chordthmlem5  20630  asinsinlem  20684  reasinsin  20689  acosrecl  20696  atancj  20703  atanrecl  20704  atanlogaddlem  20706  atanlogsublem  20708  atanbndlem  20718  atans2  20724  ressatans  20727  atantayl  20730  leibpilem2  20734  leibpi  20735  leibpisum  20736  log2tlbnd  20738  log2ublem2  20740  birthdaylem2  20744  birthdaylem3  20745  cxp2limlem  20767  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  divsqrsumo1  20775  cvxcl  20776  scvxcvx  20777  jensenlem2  20779  jensen  20780  amgmlem  20781  logdiflbnd  20786  emcllem2  20788  emcllem3  20789  emcllem5  20791  emcllem6  20792  emcllem7  20793  harmonicbnd4  20802  fsumharmonic  20803  ftalem1  20808  ftalem2  20809  ftalem4  20811  ftalem5  20812  basellem3  20818  basellem4  20819  basellem5  20820  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  efnnfsumcl  20838  chtprm  20889  chpp1  20891  chtdif  20894  efchtdvds  20895  prmorcht  20914  mumullem2  20916  fsumfldivdiaglem  20927  ppiub  20941  chtleppi  20947  chtublem  20948  chtub  20949  pclogsum  20952  vmasum  20953  logfac2  20954  chpval2  20955  chpchtsum  20956  chpub  20957  logfaclbnd  20959  logfacbnd3  20960  logfacrlim  20961  logexprlim  20962  logfacrlim2  20963  mersenne  20964  dchrabs  20997  dchrptlem1  21001  dchrptlem2  21002  bcmax  21015  bcp1ctr  21016  bposlem1  21021  bposlem9  21029  lgsvalmod  21052  lgsdilem  21059  lgsne0  21070  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  mul2sq  21102  2sqlem3  21103  2sqlem8  21109  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chto1ub  21123  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  vmadivsum  21129  vmadivsumb  21130  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasum2if  21144  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  dchrisum0flblem1  21155  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrmusumlem  21169  dchrvmasumlem  21170  rpvmasum  21173  rplogsum  21174  dirith2  21175  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  logdivsum  21180  mulog2sumlem1  21181  mulog2sumlem2  21182  mulog2sumlem3  21183  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  logsqvma  21189  logsqvma2  21190  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberglem3  21194  selberg  21195  selbergb  21196  selberg2lem  21197  selberg2  21198  selberg2b  21199  chpdifbndlem1  21200  logdivbnd  21203  selberg3lem1  21204  selberg3lem2  21205  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrmax  21211  pntrsumo1  21212  pntrsumbnd  21213  pntrsumbnd2  21214  selbergr  21215  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntsval2  21223  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6a  21229  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntibndlem3  21239  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemn  21247  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlem3  21256  pntleml  21258  pnt2  21260  pnt  21261  abvcxp  21262  ostth2lem1  21265  qabvexp  21273  padicabv  21277  padicabvcxp  21279  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  eupap1  21651  nvm1  22106  nvpi  22108  nvz0  22110  nvmtri  22113  nvabs  22115  nvge0  22116  nv1  22118  smcnlem  22146  ipval2lem4  22155  ipval2  22156  4ipval2  22157  4ipval3  22161  ipidsq  22162  dipcj  22166  dip0r  22169  ipz  22171  nmoub3i  22227  nmlno0lem  22247  nmblolbii  22253  blocnilem  22258  cncph  22273  ipasslem4  22288  ipasslem5  22289  ipblnfi  22310  minvecolem2  22330  minvecolem4  22335  minvecolem6  22337  minvecolem7  22338  htthlem  22373  normpyc  22601  hhph  22633  bcs2  22637  norm1  22704  norm1exi  22705  pjhthlem1  22846  eigvalcl  23417  eighmorth  23420  nmlnop0iALT  23451  nmbdoplbi  23480  nmcexi  23482  nmcoplbi  23484  nmbdfnlbi  23505  nmcfnlbi  23508  riesz4i  23519  cnlnadjlem2  23524  cnlnadjlem7  23529  nmopcoi  23551  nmopcoadji  23557  branmfn  23561  leopnmid  23594  opsqrlem1  23596  hst1h  23683  hstle  23686  hstoh  23688  sto2i  23693  stadd3i  23704  strlem1  23706  golem1  23727  stcltrlem1  23732  cdj1i  23889  cdj3lem1  23890  cdj3lem3b  23896  cdj3i  23897  lt2addrd  24068  le2halvesd  24075  fzsplit3  24103  bcm1n  24104  remulg  24223  elunitcn  24249  sqsscirc1  24259  sqsscirc2  24260  cnre2csqima  24262  rmulccn  24267  xrge0iifcnv  24272  xrge0iifhom  24276  zrhnm  24306  nnlogbexp  24357  logbrec  24358  indsum  24373  esumpcvgval  24421  dya2ub  24573  dya2icoseg  24580  ballotlemsi  24725  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgambdd  24774  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  regamcl  24798  relgamcl  24799  lgam1  24801  subfacval2  24826  subfaclim  24827  subfacval3  24828  rescon  24886  sinccvglem  25062  circum  25064  modaddabs  25068  possumd  25162  climlec3  25167  fprodabs  25250  iprodrecl  25268  faclimlem1  25310  faclimlem2  25311  faclimlem3  25312  faclim  25313  iprodfac  25314  faclim2  25315  fveecn  25745  eqeelen  25747  brbtwn2  25748  colinearalglem4  25752  colinearalg  25753  axsegconlem9  25768  axsegconlem10  25769  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3  25774  ax5seglem5  25776  ax5seglem6  25777  ax5seglem9  25780  ax5seg  25781  axbtwnid  25782  axpaschlem  25783  axpasch  25784  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  bpolydiflem  26004  bpoly4  26009  supadd  26138  ltflcei  26140  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnc  26161  itgaddnclem2  26163  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem2  26171  itgmulc2nc  26172  itgabsnc  26173  bddiblnc  26174  ftc1cnnclem  26177  ftc1cnnc  26178  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  areacirclem6  26186  areacirc  26187  nn0prpwlem  26215  csbrn  26346  trirn  26347  mettrifi  26353  lmclim2  26354  geomcau  26355  isbnd3  26383  ssbnd  26387  cntotbnd  26395  bfplem1  26421  bfplem2  26422  bfp  26423  rrnmet  26428  rrndstprj1  26429  rrndstprj2  26430  rrncmslem  26431  rrnequiv  26434  rrntotbnd  26435  ismrer1  26437  eldioph2lem1  26708  lzenom  26718  rencldnfilem  26771  icodiamlt  26773  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell1234qrreccl  26807  pell14qrgt0  26812  pell14qrdivcl  26818  pell14qrexpclnn0  26819  pell14qrexpcl  26820  pell14qrdich  26822  pell1qrgaplem  26826  pellfundex  26839  reglogmul  26846  reglogexp  26847  reglogbas  26848  reglog1  26849  pellfund14  26851  rmspecsqrnq  26859  rmspecfund  26862  rmym1  26888  rmyluc  26890  monotoddzzfi  26895  expmordi  26900  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.24  26918  acongrep  26935  fzmaxdif  26936  acongeq  26938  modabsdifz  26946  jm2.19lem4  26953  jm2.19  26954  jm2.26lem3  26962  jm3.1lem1  26978  jm3.1lem2  26979  dvconstbi  27419  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  eluzelcn  27591  climinf  27599  stoweidlem7  27623  stoweidlem11  27627  stoweidlem13  27629  stoweidlem17  27633  stoweidlem20  27636  stoweidlem21  27637  stoweidlem22  27638  stoweidlem23  27639  stoweidlem24  27640  stoweidlem26  27642  stoweidlem32  27648  stoweidlem36  27652  stoweidlem44  27660  stoweidlem47  27663  wallispilem3  27683  wallispi2lem1  27687  stirlinglem1  27690  stirlinglem5  27694  stirlinglem11  27700  stirlinglem12  27701  stirlinglem14  27703  sigaras  27712  sigarms  27713  sigarls  27714  sigarexp  27716  sigarperm  27717  sigarimcd  27719  sigarcol  27721  sharhght  27722  cevathlem2  27725

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294