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

Theorem rpcnd 10408
Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpcnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem rpcnd
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 10406 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 8877 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   CCcc 8751   RR+crp 10370
This theorem is referenced by:  rpcnne0d  10415  ltaddrp2d  10436  iccf1o  10794  ltexp2r  11174  discr  11254  bcp1nk  11345  bcpasc  11349  sqrlem6  11749  sqrdiv  11767  absdiv  11796  o1rlimmul  12108  isumrpcl  12318  isumltss  12323  expcnv  12338  mertenslem1  12356  bitsmod  12643  nmoi2  18255  reperflem  18339  icchmeo  18455  icopnfcnv  18456  lebnumlem3  18477  nmoleub2lem2  18613  nmoleub3  18616  minveclem3  18809  pjthlem1  18817  ovollb2lem  18863  sca2rab  18887  ovolscalem1  18888  ovolsca  18890  itg2mulc  19118  itg2cnlem2  19133  c1liplem1  19359  lhop1  19377  aalioulem4  19731  aaliou2b  19737  aaliou3lem2  19739  aaliou3lem3  19740  aaliou3lem8  19741  aaliou3lem6  19744  aaliou3lem7  19745  itgulm  19800  dvradcnv  19813  pserdvlem2  19820  abelthlem7  19830  abelthlem8  19831  lognegb  19959  logno1  19999  advlog  20017  advlogexp  20018  cxprec  20049  divcxp  20050  cxpsqr  20066  dvcxp1  20098  cxpcn3lem  20103  loglesqr  20114  asinlem3  20183  cxplim  20282  rlimcxp  20284  cxp2limlem  20286  cxp2lim  20287  cxploglim  20288  cxploglim2  20289  divsqrsumlem  20290  divsqrsumo1  20294  amgmlem  20300  basellem3  20336  basellem4  20337  chpval2  20473  logexprlim  20480  bclbnd  20535  bposlem9  20547  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem2  20639  chtppilim  20640  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ubb  20646  rplogsumlem1  20649  rplogsumlem2  20650  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrisum0  20685  mulogsumlem  20696  mulog2sumlem1  20699  mulog2sumlem2  20700  vmalogdivsum2  20703  log2sumbnd  20709  selberg3lem1  20722  selberg3lem2  20723  selberg4lem1  20725  selberg4  20726  selberg34r  20736  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem1  20754  pntibndlem2  20756  pntlemd  20759  pntlemc  20760  pntlemb  20762  pntlemq  20766  pntlemr  20767  pntlemj  20768  pntlemf  20770  pntlemo  20772  pntlem3  20774  pntleml  20776  pnt  20779  padicabvcxp  20797  ostth2lem4  20801  ostth2  20802  smcnlem  21286  blocnilem  21398  ubthlem2  21466  bcm1n  23048  rnlogbval  23417  nnlogbexp  23421  logbrec  23422  zetacvg  23704  faclimlem5  24121  itg2addnc  25005  ftc1cnnclem  25024  mslb1  25710  2wsms  25711  geomcau  26578  cntotbnd  26623  heibor1lem  26636  rrndstprj2  26658  rrncmslem  26659  pell1qrgaplem  27061  pellfund14  27086  rmxyneg  27108  rmxy1  27110  rmxy0  27111  jm2.23  27192  proot1ex  27623  stoweidlem62  27914  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  stirlinglem4  27929  stirlinglem8  27933  stirlinglem12  27937  stirlinglem15  27940
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179  df-rp 10371
  Copyright terms: Public domain W3C validator