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

Theorem recnd 9078
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 9044 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 16 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8952   RRcr 8953
This theorem is referenced by:  00id  9205  mul02lem1  9206  addid1  9210  cnegex  9211  ltadd1  9459  leadd2  9461  ltsubadd  9462  ltsubadd2  9463  lesubadd  9464  lesubadd2  9465  lesub1  9486  lesub2  9487  ltnegcon1  9493  ltnegcon2  9494  add20  9504  subge0  9505  suble0  9506  lesub0  9508  mulge0  9509  eqord2  9522  rereccl  9696  redivcl  9697  recgt0  9818  prodgt0  9819  prodge0  9821  ltmul1a  9823  ltdiv1  9838  ltmuldiv  9844  ltrec  9855  recp1lt1  9872  recreclt  9873  ledivp1  9876  infmsup  9950  infmrcl  9951  rimul  9955  cru  9956  avglt1  10169  avglt2  10170  nn0cnd  10240  zcn  10251  zeo  10319  zcnd  10340  cnref1o  10571  rpcn  10584  rpcnd  10614  ltaddrp2d  10642  qbtwnre  10749  xralrple  10755  xpncan  10794  xmulcom  10809  xmulneg1  10812  xlemul1  10833  icoshftf1o  10984  lincmb01cmp  11002  iccf1o  11003  fladdz  11190  flzadd  11191  flhalf  11194  ceim1l  11197  intfracq  11203  fldiv  11204  mod0  11218  modlt  11221  moddiffl  11222  modfrac  11224  flmod  11225  intfrac  11226  modmulnn  11228  modid  11233  modcyc  11239  modadd1  11241  modnegd  11244  modadd12d  11245  modsub12d  11246  moddi  11247  modsubdir  11248  modirr  11249  seqf1olem1  11325  serle  11341  expcl2lem  11356  expnegz  11377  expaddzlem  11386  expaddz  11387  expmulz  11389  ltexp2a  11394  leexp2a  11398  leexp2r  11400  exple1  11402  expubnd  11403  sq11  11417  bernneq2  11469  expmulnbnd  11474  discr1  11478  discr  11479  faclbnd  11544  bcp1nk  11571  remim  11885  reim0b  11887  rereb  11888  mulre  11889  cjreb  11891  recj  11892  reneg  11893  readd  11894  resub  11895  remullem  11896  remul2  11898  rediv  11899  imcj  11900  imneg  11901  imadd  11902  imsub  11903  immul2  11905  imdiv  11906  cjcj  11908  cjadd  11909  ipcnval  11911  cjmulval  11913  cjneg  11915  imval2  11919  cjreim2  11929  sqr0lem  12009  sqrlem5  12015  sqrlem7  12017  resqrthlem  12023  remsqsqr  12025  sqrmul  12028  sqrdiv  12034  sqrneg  12036  sqrmsq  12039  absdiv  12063  absid  12064  absexp  12072  absexpz  12073  absimle  12077  abslt  12081  absle  12082  abssubne0  12083  releabs  12088  recval  12089  abstri  12097  abs2difabs  12101  abs1m  12102  abslem2  12106  absrdbnd  12108  sqreulem  12126  sqreu  12127  amgm2  12136  lo1bddrp  12282  o1lo1  12294  rlimrecl  12337  rlimge0  12338  climrecl  12340  climge0  12341  climabs0  12342  reccn2  12353  o1rlimmul  12375  lo1mul2  12385  lo1sub  12387  climle  12396  climsqz  12397  climsqz2  12398  rlimsqz  12406  rlimsqz2  12407  rlimno1  12410  climlec2  12415  isercolllem1  12421  climsup  12426  caucvgrlem  12429  caurcvgr  12430  caucvgrlem2  12431  iseraltlem1  12438  iseraltlem2  12439  iseraltlem3  12440  iseralt  12441  isumrecl  12512  isumge0  12513  fsumless  12538  fsumge1  12539  fsum00  12540  fsumle  12541  fsumlt  12542  fsumabs  12543  o1fsum  12555  seqabs  12556  cvgcmp  12558  cvgcmpce  12560  abscvgcvg  12561  isumrpcl  12586  isumle  12587  isumless  12588  isumsup  12590  climcndslem1  12592  climcndslem2  12593  climcnds  12594  flo1  12597  supcvg  12598  trireciplem  12604  trirecip  12605  explecnv  12607  geo2sum  12613  geo2lim  12615  geomulcvg  12616  cvgrat  12623  mertenslem1  12624  mertenslem2  12625  efcllem  12643  ege2le3  12655  efaddlem  12658  efgt0  12667  eftlub  12673  effsumlt  12675  eflt  12681  eflegeo  12685  resin4p  12702  recos4p  12703  retanhcl  12723  tanhlt1  12724  efeul  12726  ef01bndlem  12748  sin01bnd  12749  cos01bnd  12750  sin01gt0  12754  cos01gt0  12755  sin02gt0  12756  absefi  12760  absef  12761  absefib  12762  efieq1re  12763  eirrlem  12766  rpnnen2lem5  12781  rpnnen2lem8  12784  rpnnen2lem9  12785  rpnnen2lem11  12787  rpnnen2  12788  moddvds  12822  odd2np1  12871  divalglem5  12880  bitsp1o  12908  bitsfzo  12910  bitscmp  12913  sadcaddlem  12932  nn0seqcvgd  13024  sqnprm  13061  isprm5  13075  nonsq  13114  eulerthlem2  13134  prmdiveq  13138  odzdvds  13144  pythagtriplem14  13165  pcid  13209  fldivp1  13229  pcfac  13231  pockthlem  13236  prmreclem3  13249  prmreclem4  13250  prmreclem5  13251  prmrec  13253  4sqlem5  13273  4sqlem10  13278  mul4sqlem  13284  4sqlem15  13290  4sqlem16  13291  mulgneg  14871  ghmmulg  14981  odmodnn0  15141  mndodconglem  15142  pgpfaclem2  15603  isabvd  15871  abv1z  15883  abvneg  15885  abvrec  15887  abvdiv  15888  abvdom  15889  rege0subm  16718  cnsubrg  16722  gzrngunitlem  16726  prmirredlem  16736  bl2in  18391  blhalf  18396  blssps  18415  blss  18416  methaus  18511  nrmmetd  18583  nm2dif  18632  nminvr  18666  nmdvr  18667  nlmmul0or  18680  nrginvrcnlem  18687  nmolb2d  18713  nmoi2  18725  nmoleub  18726  nmo0  18730  nmoeq0  18731  nmoco  18732  nmotri  18734  nmoid  18737  blcvx  18790  xrsxmet  18801  recld2  18806  reconnlem2  18819  opnreen  18823  metdstri  18842  metnrmlem3  18852  iihalf2cn  18920  icchmeo  18927  icopnfcnv  18928  icopnfhmeo  18929  iccpnfhmeo  18931  xrhmeo  18932  icccvx  18936  cnheiborlem  18940  evth  18945  lebnumii  18952  pcoass  19010  pcorevlem  19012  pcorev2  19014  pi1xfrcnv  19043  nmoleub2lem  19083  nmoleub2lem3  19084  nmoleub3  19088  cphsqrcl2  19110  ipcau2  19152  tchcphlem1  19153  tchcphlem2  19154  tchcph  19155  iscau3  19192  minveclem2  19288  minveclem3b  19290  minveclem4  19294  minveclem6  19296  minveclem7  19297  pjthlem1  19299  ivthlem2  19310  ivthlem3  19311  ivth2  19313  ovolfsval  19328  ovollb2lem  19345  ovolctb  19347  ovolunlem1a  19353  ovolunnul  19357  ovolfiniun  19358  ovoliunlem1  19359  ovoliun2  19363  shft2rab  19365  ovolshftlem1  19366  sca2rab  19369  ovolscalem1  19370  ovolsca  19372  ovolicc1  19373  ovolicc2lem4  19377  ovolicopnf  19381  cmmbl  19390  nulmbl  19391  nulmbl2  19392  unmbl  19393  volinun  19401  volfiniun  19402  voliunlem1  19405  voliunlem3  19407  ioombl1lem3  19415  ioombl1lem4  19416  ovolioo  19423  ioorcl2  19425  uniioovol  19432  uniioombllem3  19438  uniioombllem4  19439  uniioombllem5  19440  uniioombllem6  19441  dyadovol  19446  dyaddisjlem  19448  opnmbllem  19454  vitalilem1  19461  vitalilem2  19462  vitalilem3  19463  vitalilem4  19464  ismbf  19483  mbfmulc2lem  19500  mbfmulc2re  19501  mbfpos  19504  mbfmulc2  19516  mbfinf  19518  itg1val2  19537  itg11  19544  i1fmullem  19547  i1fadd  19548  itg1addlem4  19552  itg1addlem5  19553  i1fmulclem  19555  i1fmulc  19556  itg1mulc  19557  itg1sub  19562  itg10a  19563  itg1ge0a  19564  itg1climres  19567  mbfi1fseqlem3  19570  mbfi1fseqlem4  19571  mbfi1fseqlem5  19572  mbfi1fseqlem6  19573  mbfi1flimlem  19575  mbfmullem2  19577  itg2const  19593  itg2const2  19594  itg2mulclem  19599  itg2mulc  19600  itg2splitlem  19601  itg2split  19602  itg2monolem1  19603  itg2monolem3  19605  itg2addlem  19611  itgcl  19636  itgcnlem  19642  itgrevallem1  19647  itgposval  19648  iblneg  19655  itgneg  19656  i1fibl  19660  itgitg1  19661  itgconst  19671  ibladd  19673  itgaddlem2  19676  iblabslem  19680  iblabs  19681  iblabsr  19682  iblmulc2  19683  itgmulc2lem2  19685  itgmulc2  19686  itgabs  19687  itgsplit  19688  bddmulibl  19691  dvcjbr  19796  dvfre  19798  dvexp3  19823  dveflem  19824  dvferm1lem  19829  dvferm2lem  19831  rolle  19835  cmvth  19836  mvth  19837  dvlip  19838  dvlipcn  19839  c1liplem1  19841  c1lip1  19842  dveq0  19845  dv11cn  19846  dvlt0  19850  dvle  19852  dvivthlem1  19853  dvivth  19855  lhop1lem  19858  lhop1  19859  lhop2  19860  lhop  19861  dvcvx  19865  dvfsumle  19866  dvfsumge  19867  dvfsumabs  19868  dvfsumlem1  19871  dvfsumlem2  19872  dvfsumlem4  19874  dvfsumrlimge0  19875  dvfsumrlim2  19877  dvfsum2  19879  ftc1a  19882  ftc1lem4  19884  ftc1lem5  19885  plyeq0lem  20090  coemulhi  20133  plyrecj  20158  plydivlem3  20173  aalioulem2  20211  aalioulem3  20212  aalioulem4  20213  aalioulem5  20214  aalioulem6  20215  aaliou  20216  aaliou2  20218  aaliou2b  20219  aaliou3lem3  20222  aaliou3lem7  20227  aaliou3lem9  20228  taylthlem2  20251  ulmcn  20276  ulmdvlem1  20277  mtest  20281  mtestbdd  20282  itgulm  20285  radcnvlem1  20290  radcnvlem2  20291  radcnvlt1  20295  radcnvle  20297  dvradcnv  20298  pserulm  20299  abelthlem2  20309  abelthlem5  20312  abelthlem7  20315  abelth2  20319  reeff1olem  20323  efcvx  20326  pilem2  20329  pilem3  20330  sincosq2sgn  20368  sincosq3sgn  20369  sincosq4sgn  20370  coseq0negpitopi  20372  tanrpcl  20373  tangtx  20374  tanabsge  20375  sinq12gt0  20376  sinq34lt0t  20378  cosq14gt0  20379  cosq14ge0  20380  pige3  20386  coskpi  20389  sineq0  20390  cosordlem  20394  sinord  20397  tanord1  20400  tanord  20401  tanregt0  20402  efif1olem2  20406  efif1olem4  20408  eff1olem  20411  logrnaddcl  20433  logneg  20443  lognegb  20445  reexplog  20450  relogexp  20451  logfac  20456  efiarg  20463  cosargd  20464  cosarg0d  20465  argregt0  20466  argrege0  20467  argimgt0  20468  logneg2  20471  logmul2  20472  logdiv2  20473  abslogle  20474  tanarg  20475  logdivlti  20476  divlogrlim  20487  logcnlem2  20495  logcnlem3  20496  logcnlem4  20497  logcn  20499  logf1o2  20502  advlog  20506  advlogexp  20507  efopnlem1  20508  logtayllem  20511  logtayl  20512  logccv  20515  logcxp  20521  mulcxp  20537  divcxp  20539  cxpmul  20540  cxproot  20542  cxpmul2z  20543  abscxp  20544  abscxp2  20545  cxplt  20546  cxplea  20548  cxple2  20549  cxple2a  20551  cxplt3  20552  cxpsqrlem  20554  cxpsqr  20555  logsqr  20556  dvcxp2  20588  cxpcn3lem  20592  resqrcn  20594  cxpaddlelem  20596  cxpaddle  20597  abscxpbnd  20598  root1id  20599  root1eq1  20600  root1cj  20601  cxpeq  20602  loglesqr  20603  cosangneg2d  20610  angrtmuld  20611  ang180lem2  20613  lawcoslem1  20618  lawcos  20619  pythag  20620  isosctrlem1  20623  isosctrlem2  20624  isosctrlem3  20625  ssscongptld  20627  chordthmlem  20634  chordthmlem2  20635  chordthmlem3  20636  chordthmlem4  20637  chordthmlem5  20638  asinsinlem  20692  reasinsin  20697  acosrecl  20704  atancj  20711  atanrecl  20712  atanlogaddlem  20714  atanlogsublem  20716  atanbndlem  20726  atans2  20732  ressatans  20735  atantayl  20738  leibpilem2  20742  leibpi  20743  leibpisum  20744  log2tlbnd  20746  log2ublem2  20748  birthdaylem2  20752  birthdaylem3  20753  cxp2limlem  20775  cxp2lim  20776  cxploglim  20777  cxploglim2  20778  divsqrsumo1  20783  cvxcl  20784  scvxcvx  20785  jensenlem2  20787  jensen  20788  amgmlem  20789  logdiflbnd  20794  emcllem2  20796  emcllem3  20797  emcllem5  20799  emcllem6  20800  emcllem7  20801  harmonicbnd4  20810  fsumharmonic  20811  ftalem1  20816  ftalem2  20817  ftalem4  20819  ftalem5  20820  basellem3  20826  basellem4  20827  basellem5  20828  basellem6  20829  basellem7  20830  basellem8  20831  basellem9  20832  efnnfsumcl  20846  chtprm  20897  chpp1  20899  chtdif  20902  efchtdvds  20903  prmorcht  20922  mumullem2  20924  fsumfldivdiaglem  20935  ppiub  20949  chtleppi  20955  chtublem  20956  chtub  20957  pclogsum  20960  vmasum  20961  logfac2  20962  chpval2  20963  chpchtsum  20964  chpub  20965  logfaclbnd  20967  logfacbnd3  20968  logfacrlim  20969  logexprlim  20970  logfacrlim2  20971  mersenne  20972  dchrabs  21005  dchrptlem1  21009  dchrptlem2  21010  bcmax  21023  bcp1ctr  21024  bposlem1  21029  bposlem9  21037  lgsvalmod  21060  lgsdilem  21067  lgsne0  21078  lgsqrlem2  21087  lgseisenlem1  21094  lgseisenlem2  21095  lgseisen  21098  lgsquadlem1  21099  lgsquadlem2  21100  mul2sq  21110  2sqlem3  21111  2sqlem8  21117  chebbnd1lem1  21124  chebbnd1lem2  21125  chebbnd1lem3  21126  chtppilimlem1  21128  chtppilimlem2  21129  chtppilim  21130  chto1ub  21131  chto1lb  21133  chpchtlim  21134  chpo1ub  21135  vmadivsum  21137  vmadivsumb  21138  rplogsumlem1  21139  rplogsumlem2  21140  rpvmasumlem  21142  dchrisumlema  21143  dchrisumlem1  21144  dchrisumlem2  21145  dchrisumlem3  21146  dchrmusumlema  21148  dchrmusum2  21149  dchrvmasumlem1  21150  dchrvmasum2lem  21151  dchrvmasum2if  21152  dchrvmasumlem2  21153  dchrvmasumlem3  21154  dchrvmasumiflem1  21156  dchrvmasumiflem2  21157  dchrisum0flblem1  21163  dchrisum0fno1  21166  rpvmasum2  21167  dchrisum0re  21168  dchrisum0lema  21169  dchrisum0lem1b  21170  dchrisum0lem1  21171  dchrisum0lem2a  21172  dchrisum0lem2  21173  dchrisum0lem3  21174  dchrmusumlem  21177  dchrvmasumlem  21178  rpvmasum  21181  rplogsum  21182  dirith2  21183  mudivsum  21185  mulogsumlem  21186  mulogsum  21187  logdivsum  21188  mulog2sumlem1  21189  mulog2sumlem2  21190  mulog2sumlem3  21191  vmalogdivsum2  21193  vmalogdivsum  21194  2vmadivsumlem  21195  logsqvma  21197  logsqvma2  21198  log2sumbnd  21199  selberglem1  21200  selberglem2  21201  selberglem3  21202  selberg  21203  selbergb  21204  selberg2lem  21205  selberg2  21206  selberg2b  21207  chpdifbndlem1  21208  logdivbnd  21211  selberg3lem1  21212  selberg3lem2  21213  selberg3  21214  selberg4lem1  21215  selberg4  21216  pntrmax  21219  pntrsumo1  21220  pntrsumbnd  21221  pntrsumbnd2  21222  selbergr  21223  selberg3r  21224  selberg4r  21225  selberg34r  21226  pntsval2  21231  pntrlog2bndlem1  21232  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem4  21235  pntrlog2bndlem5  21236  pntrlog2bndlem6a  21237  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem2  21246  pntibndlem3  21247  pntlemb  21252  pntlemg  21253  pntlemh  21254  pntlemn  21255  pntlemr  21257  pntlemj  21258  pntlemf  21260  pntlemk  21261  pntlemo  21262  pntlem3  21264  pntleml  21266  pnt2  21268  pnt  21269  abvcxp  21270  ostth2lem1  21273  qabvexp  21281  padicabv  21285  padicabvcxp  21287  ostth2lem2  21289  ostth2lem3  21290  ostth2lem4  21291  ostth2  21292  ostth3  21293  eupap1  21659  nvm1  22114  nvpi  22116  nvz0  22118  nvmtri  22121  nvabs  22123  nvge0  22124  nv1  22126  smcnlem  22154  ipval2lem4  22163  ipval2  22164  4ipval2  22165  4ipval3  22169  ipidsq  22170  dipcj  22174  dip0r  22177  ipz  22179  nmoub3i  22235  nmlno0lem  22255  nmblolbii  22261  blocnilem  22266  cncph  22281  ipasslem4  22296  ipasslem5  22297  ipblnfi  22318  minvecolem2  22338  minvecolem4  22343  minvecolem6  22345  minvecolem7  22346  htthlem  22381  normpyc  22609  hhph  22641  bcs2  22645  norm1  22712  norm1exi  22713  pjhthlem1  22854  eigvalcl  23425  eighmorth  23428  nmlnop0iALT  23459  nmbdoplbi  23488  nmcexi  23490  nmcoplbi  23492  nmbdfnlbi  23513  nmcfnlbi  23516  riesz4i  23527  cnlnadjlem2  23532  cnlnadjlem7  23537  nmopcoi  23559  nmopcoadji  23565  branmfn  23569  leopnmid  23602  opsqrlem1  23604  hst1h  23691  hstle  23694  hstoh  23696  sto2i  23701  stadd3i  23712  strlem1  23714  golem1  23735  stcltrlem1  23740  cdj1i  23897  cdj3lem1  23898  cdj3lem3b  23904  cdj3i  23905  lt2addrd  24076  le2halvesd  24083  fzsplit3  24111  bcm1n  24112  remulg  24231  elunitcn  24257  sqsscirc1  24267  sqsscirc2  24268  cnre2csqima  24270  rmulccn  24275  xrge0iifcnv  24280  xrge0iifhom  24284  zrhnm  24314  nnlogbexp  24365  logbrec  24366  indsum  24381  esumpcvgval  24429  dya2ub  24581  dya2icoseg  24588  ballotlemsi  24733  zetacvg  24760  lgamgulmlem2  24775  lgamgulmlem3  24776  lgamgulmlem4  24777  lgamgulmlem5  24778  lgamgulmlem6  24779  lgamgulm2  24781  lgambdd  24782  lgamcvg2  24800  gamcvg  24801  gamcvg2lem  24804  regamcl  24806  relgamcl  24807  lgam1  24809  subfacval2  24834  subfaclim  24835  subfacval3  24836  rescon  24894  sinccvglem  25070  circum  25072  modaddabs  25076  possumd  25170  climlec3  25175  fprodabs  25258  iprodrecl  25276  faclimlem1  25318  faclimlem2  25319  faclimlem3  25320  faclim  25321  iprodfac  25322  faclim2  25323  fveecn  25753  eqeelen  25755  brbtwn2  25756  colinearalglem4  25760  colinearalg  25761  axsegconlem9  25776  axsegconlem10  25777  ax5seglem1  25779  ax5seglem2  25780  ax5seglem3  25782  ax5seglem5  25784  ax5seglem6  25785  ax5seglem9  25788  ax5seg  25789  axbtwnid  25790  axpaschlem  25791  axpasch  25792  axeuclidlem  25813  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  axcontlem8  25822  bpolydiflem  26012  bpoly4  26017  supadd  26146  ltflcei  26148  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  mbfposadd  26161  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  ibladdnc  26169  itgaddnclem2  26171  iblabsnclem  26175  iblabsnc  26176  iblmulc2nc  26177  itgmulc2nclem2  26179  itgmulc2nc  26180  itgabsnc  26181  bddiblnc  26182  ftc1cnnclem  26185  ftc1cnnc  26186  dvreasin  26187  dvreacos  26188  areacirclem2  26189  areacirclem3  26190  areacirclem6  26194  areacirc  26195  nn0prpwlem  26223  csbrn  26354  trirn  26355  mettrifi  26361  lmclim2  26362  geomcau  26363  isbnd3  26391  ssbnd  26395  cntotbnd  26403  bfplem1  26429  bfplem2  26430  bfp  26431  rrnmet  26436  rrndstprj1  26437  rrndstprj2  26438  rrncmslem  26439  rrnequiv  26442  rrntotbnd  26443  ismrer1  26445  eldioph2lem1  26716  lzenom  26726  rencldnfilem  26779  icodiamlt  26781  irrapxlem1  26783  irrapxlem2  26784  irrapxlem3  26785  irrapxlem4  26786  irrapxlem5  26787  pellexlem2  26791  pellexlem6  26795  pell1234qrreccl  26815  pell14qrgt0  26820  pell14qrdivcl  26826  pell14qrexpclnn0  26827  pell14qrexpcl  26828  pell14qrdich  26830  pell1qrgaplem  26834  pellfundex  26847  reglogmul  26854  reglogexp  26855  reglogbas  26856  reglog1  26857  pellfund14  26859  rmspecsqrnq  26867  rmspecfund  26870  rmym1  26896  rmyluc  26898  monotoddzzfi  26903  expmordi  26908  jm2.24nn  26922  jm2.17a  26923  jm2.17b  26924  jm2.17c  26925  jm2.24  26926  acongrep  26943  fzmaxdif  26944  acongeq  26946  modabsdifz  26954  jm2.19lem4  26961  jm2.19  26962  jm2.26lem3  26970  jm3.1lem1  26986  jm3.1lem2  26987  dvconstbi  27427  fmul01  27585  fmul01lt1lem1  27589  fmul01lt1lem2  27590  eluzelcn  27599  climinf  27607  stoweidlem7  27631  stoweidlem11  27635  stoweidlem13  27637  stoweidlem17  27641  stoweidlem20  27644  stoweidlem21  27645  stoweidlem22  27646  stoweidlem23  27647  stoweidlem24  27648  stoweidlem26  27650  stoweidlem32  27656  stoweidlem36  27660  stoweidlem44  27668  stoweidlem47  27671  wallispilem3  27691  wallispi2lem1  27695  stirlinglem1  27698  stirlinglem5  27702  stirlinglem11  27708  stirlinglem12  27709  stirlinglem14  27711  sigaras  27720  sigarms  27721  sigarls  27722  sigarexp  27724  sigarperm  27725  sigarimcd  27727  sigarcol  27729  sharhght  27730  cevathlem2  27733  isosctrlem1ALT  28765
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 2393  ax-resscn 9011
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 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator