MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recnd Unicode version

Theorem recnd 8951
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
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 recn 8917 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 15 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   CCcc 8825   RRcr 8826
This theorem is referenced by:  00id  9077  mul02lem1  9078  addid1  9082  cnegex  9083  ltadd1  9331  leadd2  9333  ltsubadd  9334  ltsubadd2  9335  lesubadd  9336  lesubadd2  9337  lesub1  9358  lesub2  9359  ltnegcon1  9365  ltnegcon2  9366  add20  9376  subge0  9377  suble0  9378  lesub0  9380  mulge0  9381  eqord2  9394  rereccl  9568  redivcl  9569  recgt0  9690  prodgt0  9691  prodge0  9693  ltmul1a  9695  ltdiv1  9710  ltmuldiv  9716  ltrec  9727  recp1lt1  9744  recreclt  9745  ledivp1  9748  infmsup  9822  infmrcl  9823  rimul  9827  cru  9828  avglt1  10041  avglt2  10042  nn0cnd  10112  zcn  10121  zeo  10189  zcnd  10210  cnref1o  10441  rpcn  10454  rpcnd  10484  ltaddrp2d  10512  qbtwnre  10618  xralrple  10624  xpncan  10663  xmulcom  10678  xmulneg1  10681  xlemul1  10702  icoshftf1o  10851  lincmb01cmp  10869  iccf1o  10870  fladdz  11042  flzadd  11043  flhalf  11046  ceim1l  11049  intfracq  11055  fldiv  11056  mod0  11070  modlt  11073  moddiffl  11074  modfrac  11076  flmod  11077  intfrac  11078  modmulnn  11080  modid  11085  modcyc  11091  modadd1  11093  modnegd  11096  modadd12d  11097  modsub12d  11098  moddi  11099  modsubdir  11100  modirr  11101  seqf1olem1  11177  serle  11193  expcl2lem  11208  expnegz  11229  expaddzlem  11238  expaddz  11239  expmulz  11241  ltexp2a  11246  leexp2a  11250  leexp2r  11252  exple1  11254  expubnd  11255  sq11  11269  bernneq2  11321  expmulnbnd  11326  discr1  11330  discr  11331  faclbnd  11396  bcp1nk  11422  remim  11698  reim0b  11700  rereb  11701  mulre  11702  cjreb  11704  recj  11705  reneg  11706  readd  11707  resub  11708  remullem  11709  remul2  11711  rediv  11712  imcj  11713  imneg  11714  imadd  11715  imsub  11716  immul2  11718  imdiv  11719  cjcj  11721  cjadd  11722  ipcnval  11724  cjmulval  11726  cjneg  11728  imval2  11732  cjreim2  11742  sqr0lem  11822  sqrlem5  11828  sqrlem7  11830  resqrthlem  11836  remsqsqr  11838  sqrmul  11841  sqrdiv  11847  sqrneg  11849  sqrmsq  11852  absdiv  11876  absid  11877  absexp  11885  absexpz  11886  absimle  11890  abslt  11894  absle  11895  abssubne0  11896  releabs  11901  recval  11902  abstri  11910  abs2difabs  11914  abs1m  11915  abslem2  11919  absrdbnd  11921  sqreulem  11939  sqreu  11940  amgm2  11949  lo1bddrp  12095  o1lo1  12107  rlimrecl  12150  rlimge0  12151  climrecl  12153  climge0  12154  climabs0  12155  reccn2  12166  o1rlimmul  12188  lo1mul2  12198  lo1sub  12200  climle  12209  climsqz  12210  climsqz2  12211  rlimsqz  12219  rlimsqz2  12220  rlimno1  12223  climlec2  12228  isercolllem1  12234  climsup  12239  caucvgrlem  12242  caurcvgr  12243  caucvgrlem2  12244  iseraltlem1  12251  iseraltlem2  12252  iseraltlem3  12253  iseralt  12254  isumrecl  12325  isumge0  12326  fsumless  12351  fsumge1  12352  fsum00  12353  fsumle  12354  fsumlt  12355  fsumabs  12356  o1fsum  12368  seqabs  12369  cvgcmp  12371  cvgcmpce  12373  abscvgcvg  12374  isumrpcl  12399  isumle  12400  isumless  12401  isumsup  12403  climcndslem1  12405  climcndslem2  12406  climcnds  12407  flo1  12410  supcvg  12411  trireciplem  12417  trirecip  12418  explecnv  12420  geo2sum  12426  geo2lim  12428  geomulcvg  12429  cvgrat  12436  mertenslem1  12437  mertenslem2  12438  efcllem  12456  ege2le3  12468  efaddlem  12471  efgt0  12480  eftlub  12486  effsumlt  12488  eflt  12494  eflegeo  12498  resin4p  12515  recos4p  12516  retanhcl  12536  tanhlt1  12537  efeul  12539  ef01bndlem  12561  sin01bnd  12562  cos01bnd  12563  sin01gt0  12567  cos01gt0  12568  sin02gt0  12569  absefi  12573  absef  12574  absefib  12575  efieq1re  12576  eirrlem  12579  rpnnen2lem5  12594  rpnnen2lem8  12597  rpnnen2lem9  12598  rpnnen2lem11  12600  rpnnen2  12601  moddvds  12635  odd2np1  12684  divalglem5  12693  bitsp1  12719  bitsp1o  12721  bitsfzo  12723  bitscmp  12726  sadcaddlem  12745  nn0seqcvgd  12837  sqnprm  12874  isprm5  12888  nonsq  12927  eulerthlem2  12947  prmdiveq  12951  odzdvds  12957  pythagtriplem14  12978  pcid  13022  fldivp1  13042  pcfac  13044  pockthlem  13049  prmreclem3  13062  prmreclem4  13063  prmreclem5  13064  prmrec  13066  4sqlem5  13086  4sqlem10  13091  mul4sqlem  13097  4sqlem15  13103  4sqlem16  13104  mulgneg  14684  ghmmulg  14794  odmodnn0  14954  mndodconglem  14955  pgpfaclem2  15416  isabvd  15684  abv1z  15696  abvneg  15698  abvrec  15700  abvdiv  15701  abvdom  15702  rege0subm  16534  cnsubrg  16538  gzrngunitlem  16542  prmirredlem  16552  bl2in  18059  blhalf  18062  blss  18074  methaus  18168  nrmmetd  18199  nm2dif  18248  nminvr  18282  nmdvr  18283  nlmmul0or  18296  nrginvrcnlem  18303  nmolb2d  18329  nmoi2  18341  nmoleub  18342  nmo0  18346  nmoeq0  18347  nmoco  18348  nmotri  18350  nmoid  18353  blcvx  18406  xrsxmet  18417  recld2  18422  reconnlem2  18435  opnreen  18439  metdstri  18458  metnrmlem3  18468  iihalf2cn  18536  icchmeo  18543  icopnfcnv  18544  icopnfhmeo  18545  iccpnfhmeo  18547  xrhmeo  18548  icccvx  18552  cnheiborlem  18556  evth  18561  lebnumii  18568  pcoass  18626  pcorevlem  18628  pcorev2  18630  pi1xfrcnv  18659  nmoleub2lem  18699  nmoleub2lem3  18700  nmoleub3  18704  cphsqrcl2  18726  ipcau2  18768  tchcphlem1  18769  tchcphlem2  18770  tchcph  18771  iscau3  18808  minveclem2  18894  minveclem3b  18896  minveclem4  18900  minveclem6  18902  minveclem7  18903  pjthlem1  18905  ivthlem2  18916  ivthlem3  18917  ivth2  18919  ovolfsval  18934  ovollb2lem  18951  ovolctb  18953  ovolunlem1a  18959  ovolunnul  18963  ovolfiniun  18964  ovoliunlem1  18965  ovoliun2  18969  shft2rab  18971  ovolshftlem1  18972  sca2rab  18975  ovolscalem1  18976  ovolsca  18978  ovolicc1  18979  ovolicc2lem4  18983  ovolicopnf  18987  cmmbl  18996  nulmbl  18997  nulmbl2  18998  unmbl  18999  volinun  19007  volfiniun  19008  voliunlem1  19011  voliunlem3  19013  ioombl1lem3  19021  ioombl1lem4  19022  ovolioo  19029  ioorcl2  19031  uniioovol  19038  uniioombllem3  19044  uniioombllem4  19045  uniioombllem5  19046  uniioombllem6  19047  dyadovol  19052  dyaddisjlem  19054  opnmbllem  19060  vitalilem1  19067  vitalilem2  19068  vitalilem3  19069  vitalilem4  19070  ismbf  19089  mbfmulc2lem  19106  mbfmulc2re  19107  mbfpos  19110  mbfmulc2  19122  mbfinf  19124  itg1val2  19143  itg11  19150  i1fmullem  19153  i1fadd  19154  itg1addlem4  19158  itg1addlem5  19159  i1fmulclem  19161  i1fmulc  19162  itg1mulc  19163  itg1sub  19168  itg10a  19169  itg1ge0a  19170  itg1climres  19173  mbfi1fseqlem3  19176  mbfi1fseqlem4  19177  mbfi1fseqlem5  19178  mbfi1fseqlem6  19179  mbfi1flimlem  19181  mbfmullem2  19183  itg2const  19199  itg2const2  19200  itg2mulclem  19205  itg2mulc  19206  itg2splitlem  19207  itg2split  19208  itg2monolem1  19209  itg2monolem3  19211  itg2addlem  19217  itgcl  19242  itgcnlem  19248  itgrevallem1  19253  itgposval  19254  iblneg  19261  itgneg  19262  i1fibl  19266  itgitg1  19267  itgconst  19277  ibladd  19279  itgaddlem2  19282  iblabslem  19286  iblabs  19287  iblabsr  19288  iblmulc2  19289  itgmulc2lem2  19291  itgmulc2  19292  itgabs  19293  itgsplit  19294  bddmulibl  19297  dvcjbr  19402  dvfre  19404  dvexp3  19429  dveflem  19430  dvferm1lem  19435  dvferm2lem  19437  rolle  19441  cmvth  19442  mvth  19443  dvlip  19444  dvlipcn  19445  c1liplem1  19447  c1lip1  19448  dveq0  19451  dv11cn  19452  dvlt0  19456  dvle  19458  dvivthlem1  19459  dvivth  19461  lhop1lem  19464  lhop1  19465  lhop2  19466  lhop  19467  dvcvx  19471  dvfsumle  19472  dvfsumge  19473  dvfsumabs  19474  dvfsumlem1  19477  dvfsumlem2  19478  dvfsumlem4  19480  dvfsumrlimge0  19481  dvfsumrlim2  19483  dvfsum2  19485  ftc1a  19488  ftc1lem4  19490  ftc1lem5  19491  plyeq0lem  19696  coemulhi  19739  plyrecj  19764  plydivlem3  19779  aalioulem2  19817  aalioulem3  19818  aalioulem4  19819  aalioulem5  19820  aalioulem6  19821  aaliou  19822  aaliou2  19824  aaliou2b  19825  aaliou3lem3  19828  aaliou3lem7  19833  aaliou3lem9  19834  taylthlem2  19857  ulmcn  19882  ulmdvlem1  19883  mtest  19887  mtestbdd  19888  itgulm  19891  radcnvlem1  19896  radcnvlem2  19897  radcnvlt1  19901  radcnvle  19903  dvradcnv  19904  pserulm  19905  abelthlem2  19915  abelthlem5  19918  abelthlem7  19921  abelth2  19925  reeff1olem  19929  efcvx  19932  pilem2  19935  pilem3  19936  sincosq2sgn  19974  sincosq3sgn  19975  sincosq4sgn  19976  coseq0negpitopi  19978  tanrpcl  19979  tangtx  19980  tanabsge  19981  sinq12gt0  19982  sinq34lt0t  19984  cosq14gt0  19985  cosq14ge0  19986  pige3  19992  coskpi  19995  sineq0  19996  cosordlem  20000  sinord  20003  tanord1  20006  tanord  20007  tanregt0  20008  efif1olem2  20012  efif1olem4  20014  eff1olem  20017  logrnaddcl  20039  logneg  20049  lognegb  20051  reexplog  20056  relogexp  20057  logfac  20062  efiarg  20069  cosargd  20070  cosarg0d  20071  argregt0  20072  argrege0  20073  argimgt0  20074  logneg2  20077  logmul2  20078  logdiv2  20079  abslogle  20080  tanarg  20081  logdivlti  20082  divlogrlim  20093  logcnlem2  20101  logcnlem3  20102  logcnlem4  20103  logcn  20105  logf1o2  20108  advlog  20112  advlogexp  20113  efopnlem1  20114  logtayllem  20117  logtayl  20118  logccv  20121  logcxp  20127  mulcxp  20143  divcxp  20145  cxpmul  20146  cxproot  20148  cxpmul2z  20149  abscxp  20150  abscxp2  20151  cxplt  20152  cxplea  20154  cxple2  20155  cxple2a  20157  cxplt3  20158  cxpsqrlem  20160  cxpsqr  20161  logsqr  20162  dvcxp2  20194  cxpcn3lem  20198  resqrcn  20200  cxpaddlelem  20202  cxpaddle  20203  abscxpbnd  20204  root1id  20205  root1eq1  20206  root1cj  20207  cxpeq  20208  loglesqr  20209  cosangneg2d  20216  angrtmuld  20217  ang180lem2  20219  lawcoslem1  20224  lawcos  20225  pythag  20226  isosctrlem1  20229  isosctrlem2  20230  isosctrlem3  20231  ssscongptld  20233  chordthmlem  20240  chordthmlem2  20241  chordthmlem3  20242  chordthmlem4  20243  chordthmlem5  20244  asinsinlem  20298  reasinsin  20303  acosrecl  20310  atancj  20317  atanrecl  20318  atanlogaddlem  20320  atanlogsublem  20322  atanbndlem  20332  atans2  20338  ressatans  20341  atantayl  20344  leibpilem2  20348  leibpi  20349  leibpisum  20350  log2tlbnd  20352  log2ublem2  20354  birthdaylem2  20358  birthdaylem3  20359  cxp2limlem  20381  cxp2lim  20382  cxploglim  20383  cxploglim2  20384  divsqrsumo1  20389  cvxcl  20390  scvxcvx  20391  jensenlem2  20393  jensen  20394  amgmlem  20395  logdiflbnd  20400  emcllem2  20402  emcllem3  20403  emcllem5  20405  emcllem6  20406  emcllem7  20407  harmonicbnd4  20416  fsumharmonic  20417  ftalem1  20422  ftalem2  20423  ftalem4  20425  ftalem5  20426  basellem3  20432  basellem4  20433  basellem5  20434  basellem6  20435  basellem7  20436  basellem8  20437  basellem9  20438  efnnfsumcl  20452  chtprm  20503  chpp1  20505  chtdif  20508  efchtdvds  20509  prmorcht  20528  mumullem2  20530  fsumfldivdiaglem  20541  ppiub  20555  chtleppi  20561  chtublem  20562  chtub  20563  pclogsum  20566  vmasum  20567  logfac2  20568  chpval2  20569  chpchtsum  20570  chpub  20571  logfaclbnd  20573  logfacbnd3  20574  logfacrlim  20575  logexprlim  20576  logfacrlim2  20577  mersenne  20578  dchrabs  20611  dchrptlem1  20615  dchrptlem2  20616  bcmax  20629  bcp1ctr  20630  bposlem1  20635  bposlem9  20643  lgsvalmod  20666  lgsdilem  20673  lgsne0  20684  lgsqrlem2  20693  lgseisenlem1  20700  lgseisenlem2  20701  lgseisen  20704  lgsquadlem1  20705  lgsquadlem2  20706  mul2sq  20716  2sqlem3  20717  2sqlem8  20723  chebbnd1lem1  20730  chebbnd1lem2  20731  chebbnd1lem3  20732  chtppilimlem1  20734  chtppilimlem2  20735  chtppilim  20736  chto1ub  20737  chto1lb  20739  chpchtlim  20740  chpo1ub  20741  vmadivsum  20743  vmadivsumb  20744  rplogsumlem1  20745  rplogsumlem2  20746  rpvmasumlem  20748  dchrisumlema  20749  dchrisumlem1  20750  dchrisumlem2  20751  dchrisumlem3  20752  dchrmusumlema  20754  dchrmusum2  20755  dchrvmasumlem1  20756  dchrvmasum2lem  20757  dchrvmasum2if  20758  dchrvmasumlem2  20759  dchrvmasumlem3  20760  dchrvmasumiflem1  20762  dchrvmasumiflem2  20763  dchrisum0flblem1  20769  dchrisum0fno1  20772  rpvmasum2  20773  dchrisum0re  20774  dchrisum0lema  20775  dchrisum0lem1b  20776  dchrisum0lem1  20777  dchrisum0lem2a  20778  dchrisum0lem2  20779  dchrisum0lem3  20780  dchrmusumlem  20783  dchrvmasumlem  20784  rpvmasum  20787  rplogsum  20788  dirith2  20789  mudivsum  20791  mulogsumlem  20792  mulogsum  20793  logdivsum  20794  mulog2sumlem1  20795  mulog2sumlem2  20796  mulog2sumlem3  20797  vmalogdivsum2  20799  vmalogdivsum  20800  2vmadivsumlem  20801  logsqvma  20803  logsqvma2  20804  log2sumbnd  20805  selberglem1  20806  selberglem2  20807  selberglem3  20808  selberg  20809  selbergb  20810  selberg2lem  20811  selberg2  20812  selberg2b  20813  chpdifbndlem1  20814  logdivbnd  20817  selberg3lem1  20818  selberg3lem2  20819  selberg3  20820  selberg4lem1  20821  selberg4  20822  pntrmax  20825  pntrsumo1  20826  pntrsumbnd  20827  pntrsumbnd2  20828  selbergr  20829  selberg3r  20830  selberg4r  20831  selberg34r  20832  pntsval2  20837  pntrlog2bndlem1  20838  pntrlog2bndlem2  20839  pntrlog2bndlem3  20840  pntrlog2bndlem4  20841  pntrlog2bndlem5  20842  pntrlog2bndlem6a  20843  pntrlog2bndlem6  20844  pntrlog2bnd  20845  pntpbnd1a  20846  pntpbnd1  20847  pntpbnd2  20848  pntibndlem2  20852  pntibndlem3  20853  pntlemb  20858  pntlemg  20859  pntlemh  20860  pntlemn  20861  pntlemr  20863  pntlemj  20864  pntlemf  20866  pntlemk  20867  pntlemo  20868  pntlem3  20870  pntleml  20872  pnt2  20874  pnt  20875  abvcxp  20876  ostth2lem1  20879  qabvexp  20887  padicabv  20891  padicabvcxp  20893  ostth2lem2  20895  ostth2lem3  20896  ostth2lem4  20897  ostth2  20898  ostth3  20899  nvm1  21344  nvpi  21346  nvz0  21348  nvmtri  21351  nvabs  21353  nvge0  21354  nv1  21356  smcnlem  21384  ipval2lem4  21393  ipval2  21394  4ipval2  21395  4ipval3  21399  ipidsq  21400  dipcj  21404  dip0r  21407  ipz  21409  nmoub3i  21465  nmlno0lem  21485  nmblolbii  21491  blocnilem  21496  cncph  21511  ipasslem4  21526  ipasslem5  21527  ipblnfi  21548  minvecolem2  21568  minvecolem4  21573  minvecolem6  21575  minvecolem7  21576  htthlem  21611  normpyc  21839  hhph  21871  bcs2  21875  norm1  21942  norm1exi  21943  pjhthlem1  22084  eigvalcl  22655  eighmorth  22658  nmlnop0iALT  22689  nmbdoplbi  22718  nmcexi  22720  nmcoplbi  22722  nmbdfnlbi  22743  nmcfnlbi  22746  riesz4i  22757  cnlnadjlem2  22762  cnlnadjlem7  22767  nmopcoi  22789  nmopcoadji  22795  branmfn  22799  leopnmid  22832  opsqrlem1  22834  hst1h  22921  hstle  22924  hstoh  22926  sto2i  22931  stadd3i  22942  strlem1  22944  golem1  22965  stcltrlem1  22970  cdj1i  23127  cdj3lem1  23128  cdj3lem3b  23134  cdj3i  23135  lt2addrd  23320  le2halvesd  23323  fzsplit3  23352  bcm1n  23353  remulg  23436  sqsscirc1  23462  sqsscirc2  23463  cnre2csqima  23465  rmulccn  23470  xrge0iifcnv  23475  xrge0iifhom  23479  zrhnm  23628  nnlogbexp  23670  logbrec  23671  indsum  23686  esumpcvgval  23734  dya2ub  23884  dya2icoseg  23891  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemsgt1  24017  ballotlemsel1i  24019  ballotlemsi  24021  zetacvg  24048  lgamgulmlem2  24063  lgamgulmlem3  24064  lgamgulmlem4  24065  lgamgulmlem5  24066  lgamgulmlem6  24067  lgamgulm2  24069  lgambdd  24070  lgamucov  24071  lgamcvg2  24088  gamcvg  24089  gamcvg2lem  24092  regamcl  24094  relgamcl  24095  lgam1  24097  subfacval2  24122  subfaclim  24123  subfacval3  24124  rescon  24181  eupap1  24304  sinccvglem  24409  circum  24411  modaddabs  24415  possumd  24510  climlec3  24515  fprodabs  24598  iprodrecl  24609  faclimlem1  24654  faclimlem2  24655  faclimlem3  24656  faclim  24657  iprodfac  24658  faclim2  24659  fveecn  25089  eqeelen  25091  brbtwn2  25092  colinearalglem4  25096  colinearalg  25097  axsegconlem9  25112  axsegconlem10  25113  ax5seglem1  25115  ax5seglem2  25116  ax5seglem3  25118  ax5seglem5  25120  ax5seglem6  25121  ax5seglem9  25124  ax5seg  25125  axbtwnid  25126  axpaschlem  25127  axpasch  25128  axeuclidlem  25149  axcontlem2  25152  axcontlem4  25154  axcontlem7  25157  axcontlem8  25158  bpolydiflem  25348  bpoly4  25353  supadd  25483  ltflcei  25485  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  itg2gt0cn  25495  ibladdnc  25497  itgaddnclem2  25499  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nclem2  25507  itgmulc2nc  25508  itgabsnc  25509  bddiblnc  25510  ftc1cnnclem  25513  ftc1cnnc  25514  dvreasin  25515  dvreacos  25516  areacirclem2  25517  areacirclem3  25518  areacirclem6  25522  areacirc  25523  nn0prpwlem  25562  csbrn  25786  trirn  25787  mettrifi  25797  lmclim2  25798  geomcau  25799  isbnd3  25831  ssbnd  25835  cntotbnd  25843  bfplem1  25869  bfplem2  25870  bfp  25871  rrnmet  25876  rrndstprj1  25877  rrndstprj2  25878  rrncmslem  25879  rrnequiv  25882  rrntotbnd  25883  ismrer1  25885  eldioph2lem1  26162  lzenom  26172  rencldnfilem  26226  icodiamlt  26228  irrapxlem1  26230  irrapxlem2  26231  irrapxlem3  26232  irrapxlem4  26233  irrapxlem5  26234  pellexlem2  26238  pellexlem6  26242  pell1234qrreccl  26262  pell14qrgt0  26267  pell14qrdivcl  26273  pell14qrexpclnn0  26274  pell14qrexpcl  26275  pell14qrdich  26277  pell1qrgaplem  26281  pellfundex  26294  reglogmul  26301  reglogexp  26302  reglogbas  26303  reglog1  26304  pellfund14  26306  rmspecsqrnq  26314  rmspecfund  26317  rmym1  26343  rmyluc  26345  monotoddzzfi  26350  expmordi  26355  jm2.24nn  26369  jm2.17a  26370  jm2.17b  26371  jm2.17c  26372  jm2.24  26373  acongrep  26390  fzmaxdif  26391  acongeq  26393  modabsdifz  26401  jm2.19lem4  26408  jm2.19  26409  jm2.26lem3  26417  jm3.1lem1  26433  jm3.1lem2  26434  dvconstbi  26874  climinf  27055  stoweidlem13  27085  stoweidlem17  27089  stoweidlem21  27093  stoweidlem47  27119  stoweidlem59  27131  wallispilem3  27139  wallispilem5  27141  wallispi2lem1  27143  stirlinglem1  27146  stirlinglem5  27150  stirlinglem11  27156  stirlinglem12  27157  stirlinglem14  27159  sigaras  27168  sigarms  27169  sigarls  27170  sigarexp  27172  sigarperm  27173  sigarimcd  27175  sigarcol  27177  sharhght  27178  cevathlem2  27181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-resscn 8884
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator