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

Theorem rpcnd 10606
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 10604 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9070 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8944   RR+crp 10568
This theorem is referenced by:  rpcnne0d  10613  ltaddrp2d  10634  iccf1o  10995  ltexp2r  11391  discr  11471  bcp1nk  11563  bcpasc  11567  sqrlem6  12008  sqrdiv  12026  absdiv  12055  o1rlimmul  12367  isumrpcl  12578  isumltss  12583  expcnv  12598  mertenslem1  12616  bitsmod  12903  nmoi2  18717  reperflem  18802  icchmeo  18919  icopnfcnv  18920  lebnumlem3  18941  nmoleub2lem2  19077  nmoleub3  19080  minveclem3  19283  pjthlem1  19291  ovollb2lem  19337  sca2rab  19361  ovolscalem1  19362  ovolsca  19364  itg2mulc  19592  itg2cnlem2  19607  c1liplem1  19833  lhop1  19851  aalioulem4  20205  aaliou2b  20211  aaliou3lem2  20213  aaliou3lem3  20214  aaliou3lem8  20215  aaliou3lem6  20218  aaliou3lem7  20219  itgulm  20277  dvradcnv  20290  pserdvlem2  20297  abelthlem7  20307  abelthlem8  20308  lognegb  20437  logno1  20480  advlog  20498  advlogexp  20499  cxprec  20530  divcxp  20531  cxpsqr  20547  dvcxp1  20579  cxpcn3lem  20584  loglesqr  20595  asinlem3  20664  cxplim  20763  rlimcxp  20765  cxp2limlem  20767  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  divsqrsumlem  20771  divsqrsumo1  20775  amgmlem  20781  basellem3  20818  basellem4  20819  chpval2  20955  logexprlim  20962  bclbnd  21017  bposlem9  21029  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem2  21121  chtppilim  21122  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ubb  21128  rplogsumlem1  21131  rplogsumlem2  21132  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrisum0  21167  mulogsumlem  21178  mulog2sumlem1  21181  mulog2sumlem2  21182  vmalogdivsum2  21185  log2sumbnd  21191  selberg3lem1  21204  selberg3lem2  21205  selberg4lem1  21207  selberg4  21208  selberg34r  21218  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem1  21236  pntibndlem2  21238  pntlemd  21241  pntlemc  21242  pntlemb  21244  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemo  21254  pntlem3  21256  pntleml  21258  pnt  21261  padicabvcxp  21279  ostth2lem4  21283  ostth2  21284  ostth3  21285  smcnlem  22146  blocnilem  22258  ubthlem2  22326  bcm1n  24104  rnlogbval  24353  nnlogbexp  24357  logbrec  24358  probmeasb  24641  zetacvg  24752  lgamucov  24775  iprodgam  25272  faclimlem1  25310  faclimlem3  25312  faclim  25313  iprodfac  25314  mblfinlem2  26144  itg2addnclem3  26157  ftc1cnnclem  26177  geomcau  26355  cntotbnd  26395  heibor1lem  26408  rrndstprj2  26430  rrncmslem  26431  pell1qrgaplem  26826  pellfund14  26851  rmxyneg  26873  rmxy1  26875  rmxy0  26876  jm2.23  26957  proot1ex  27388  stoweidlem1  27617  stoweidlem3  27619  stoweidlem7  27623  stoweidlem11  27627  stoweidlem14  27630  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem42  27658  stoweidlem51  27667  stoweidlem59  27675  stoweidlem62  27678  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  stirlinglem4  27693  stirlinglem8  27697  stirlinglem12  27701  stirlinglem15  27704
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-nfc 2529  df-rab 2675  df-in 3287  df-ss 3294  df-rp 10569
  Copyright terms: Public domain W3C validator