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

Theorem rpcnd 10655
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 10653 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9119 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   CCcc 8993   RR+crp 10617
This theorem is referenced by:  rpcnne0d  10662  ltaddrp2d  10683  iccf1o  11044  ltexp2r  11441  discr  11521  bcp1nk  11613  bcpasc  11617  sqrlem6  12058  sqrdiv  12076  absdiv  12105  o1rlimmul  12417  isumrpcl  12628  isumltss  12633  expcnv  12648  mertenslem1  12666  bitsmod  12953  nmoi2  18769  reperflem  18854  icchmeo  18971  icopnfcnv  18972  lebnumlem3  18993  nmoleub2lem2  19129  nmoleub3  19132  minveclem3  19335  pjthlem1  19343  ovollb2lem  19389  sca2rab  19413  ovolscalem1  19414  ovolsca  19416  itg2mulc  19642  itg2cnlem2  19657  c1liplem1  19885  lhop1  19903  aalioulem4  20257  aaliou2b  20263  aaliou3lem2  20265  aaliou3lem3  20266  aaliou3lem8  20267  aaliou3lem6  20270  aaliou3lem7  20271  itgulm  20329  dvradcnv  20342  pserdvlem2  20349  abelthlem7  20359  abelthlem8  20360  lognegb  20489  logno1  20532  advlog  20550  advlogexp  20551  cxprec  20582  divcxp  20583  cxpsqr  20599  dvcxp1  20631  cxpcn3lem  20636  loglesqr  20647  asinlem3  20716  cxplim  20815  rlimcxp  20817  cxp2limlem  20819  cxp2lim  20820  cxploglim  20821  cxploglim2  20822  divsqrsumlem  20823  divsqrsumo1  20827  amgmlem  20833  basellem3  20870  basellem4  20871  chpval2  21007  logexprlim  21014  bclbnd  21069  bposlem9  21081  chebbnd1lem3  21170  chebbnd1  21171  chtppilimlem2  21173  chtppilim  21174  chebbnd2  21176  chto1lb  21177  chpchtlim  21178  chpo1ubb  21180  rplogsumlem1  21183  rplogsumlem2  21184  dchrvmasumlem1  21194  dchrvmasum2lem  21195  dchrisum0lema  21213  dchrisum0lem1b  21214  dchrisum0lem1  21215  dchrisum0lem2a  21216  dchrisum0lem2  21217  dchrisum0lem3  21218  dchrisum0  21219  mulogsumlem  21230  mulog2sumlem1  21233  mulog2sumlem2  21234  vmalogdivsum2  21237  log2sumbnd  21243  selberg3lem1  21256  selberg3lem2  21257  selberg4lem1  21259  selberg4  21260  selberg34r  21270  pntrlog2bndlem2  21277  pntrlog2bndlem3  21278  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  pntpbnd1a  21284  pntpbnd2  21286  pntibndlem1  21288  pntibndlem2  21290  pntlemd  21293  pntlemc  21294  pntlemb  21296  pntlemq  21300  pntlemr  21301  pntlemj  21302  pntlemf  21304  pntlemo  21306  pntlem3  21308  pntleml  21310  pnt  21313  padicabvcxp  21331  ostth2lem4  21335  ostth2  21336  ostth3  21337  smcnlem  22198  blocnilem  22310  ubthlem2  22378  bcm1n  24156  rnlogbval  24405  nnlogbexp  24409  logbrec  24410  probmeasb  24693  zetacvg  24804  lgamucov  24827  iprodgam  25324  faclimlem1  25367  faclimlem3  25369  faclim  25370  iprodfac  25371  mblfinlem3  26257  itg2addnclem3  26272  ftc1cnnclem  26292  geomcau  26479  cntotbnd  26519  heibor1lem  26532  rrndstprj2  26554  rrncmslem  26555  pell1qrgaplem  26950  pellfund14  26975  rmxyneg  26997  rmxy1  26999  rmxy0  27000  jm2.23  27081  proot1ex  27511  stoweidlem1  27740  stoweidlem3  27742  stoweidlem7  27746  stoweidlem11  27750  stoweidlem14  27753  stoweidlem24  27763  stoweidlem25  27764  stoweidlem26  27765  stoweidlem42  27781  stoweidlem51  27790  stoweidlem59  27798  stoweidlem62  27801  wallispilem4  27807  wallispilem5  27808  wallispi  27809  wallispi2lem1  27810  stirlinglem4  27816  stirlinglem8  27820  stirlinglem12  27824  stirlinglem15  27827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9052
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-in 3329  df-ss 3336  df-rp 10618
  Copyright terms: Public domain W3C validator