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

Theorem rpcnd 10640
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 10638 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9104 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8978   RR+crp 10602
This theorem is referenced by:  rpcnne0d  10647  ltaddrp2d  10668  iccf1o  11029  ltexp2r  11426  discr  11506  bcp1nk  11598  bcpasc  11602  sqrlem6  12043  sqrdiv  12061  absdiv  12090  o1rlimmul  12402  isumrpcl  12613  isumltss  12618  expcnv  12633  mertenslem1  12651  bitsmod  12938  nmoi2  18754  reperflem  18839  icchmeo  18956  icopnfcnv  18957  lebnumlem3  18978  nmoleub2lem2  19114  nmoleub3  19117  minveclem3  19320  pjthlem1  19328  ovollb2lem  19374  sca2rab  19398  ovolscalem1  19399  ovolsca  19401  itg2mulc  19629  itg2cnlem2  19644  c1liplem1  19870  lhop1  19888  aalioulem4  20242  aaliou2b  20248  aaliou3lem2  20250  aaliou3lem3  20251  aaliou3lem8  20252  aaliou3lem6  20255  aaliou3lem7  20256  itgulm  20314  dvradcnv  20327  pserdvlem2  20334  abelthlem7  20344  abelthlem8  20345  lognegb  20474  logno1  20517  advlog  20535  advlogexp  20536  cxprec  20567  divcxp  20568  cxpsqr  20584  dvcxp1  20616  cxpcn3lem  20621  loglesqr  20632  asinlem3  20701  cxplim  20800  rlimcxp  20802  cxp2limlem  20804  cxp2lim  20805  cxploglim  20806  cxploglim2  20807  divsqrsumlem  20808  divsqrsumo1  20812  amgmlem  20818  basellem3  20855  basellem4  20856  chpval2  20992  logexprlim  20999  bclbnd  21054  bposlem9  21066  chebbnd1lem3  21155  chebbnd1  21156  chtppilimlem2  21158  chtppilim  21159  chebbnd2  21161  chto1lb  21162  chpchtlim  21163  chpo1ubb  21165  rplogsumlem1  21168  rplogsumlem2  21169  dchrvmasumlem1  21179  dchrvmasum2lem  21180  dchrisum0lema  21198  dchrisum0lem1b  21199  dchrisum0lem1  21200  dchrisum0lem2a  21201  dchrisum0lem2  21202  dchrisum0lem3  21203  dchrisum0  21204  mulogsumlem  21215  mulog2sumlem1  21218  mulog2sumlem2  21219  vmalogdivsum2  21222  log2sumbnd  21228  selberg3lem1  21241  selberg3lem2  21242  selberg4lem1  21244  selberg4  21245  selberg34r  21255  pntrlog2bndlem2  21262  pntrlog2bndlem3  21263  pntrlog2bndlem4  21264  pntrlog2bndlem5  21265  pntpbnd1a  21269  pntpbnd2  21271  pntibndlem1  21273  pntibndlem2  21275  pntlemd  21278  pntlemc  21279  pntlemb  21281  pntlemq  21285  pntlemr  21286  pntlemj  21287  pntlemf  21289  pntlemo  21291  pntlem3  21293  pntleml  21295  pnt  21298  padicabvcxp  21316  ostth2lem4  21320  ostth2  21321  ostth3  21322  smcnlem  22183  blocnilem  22295  ubthlem2  22363  bcm1n  24141  rnlogbval  24390  nnlogbexp  24394  logbrec  24395  probmeasb  24678  zetacvg  24789  lgamucov  24812  iprodgam  25309  faclimlem1  25352  faclimlem3  25354  faclim  25355  iprodfac  25356  mblfinlem2  26208  itg2addnclem3  26221  ftc1cnnclem  26241  geomcau  26419  cntotbnd  26459  heibor1lem  26472  rrndstprj2  26494  rrncmslem  26495  pell1qrgaplem  26890  pellfund14  26915  rmxyneg  26937  rmxy1  26939  rmxy0  26940  jm2.23  27021  proot1ex  27452  stoweidlem1  27681  stoweidlem3  27683  stoweidlem7  27687  stoweidlem11  27691  stoweidlem14  27694  stoweidlem24  27704  stoweidlem25  27705  stoweidlem26  27706  stoweidlem42  27722  stoweidlem51  27731  stoweidlem59  27739  stoweidlem62  27742  wallispilem4  27748  wallispilem5  27749  wallispi  27750  wallispi2lem1  27751  stirlinglem4  27757  stirlinglem8  27761  stirlinglem12  27765  stirlinglem15  27768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9037
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326  df-rp 10603
  Copyright terms: Public domain W3C validator