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

Theorem rpcnd 10584
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 10582 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9049 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8923   RR+crp 10546
This theorem is referenced by:  rpcnne0d  10591  ltaddrp2d  10612  iccf1o  10973  ltexp2r  11365  discr  11445  bcp1nk  11537  bcpasc  11541  sqrlem6  11982  sqrdiv  12000  absdiv  12029  o1rlimmul  12341  isumrpcl  12552  isumltss  12557  expcnv  12572  mertenslem1  12590  bitsmod  12877  nmoi2  18637  reperflem  18722  icchmeo  18839  icopnfcnv  18840  lebnumlem3  18861  nmoleub2lem2  18997  nmoleub3  19000  minveclem3  19199  pjthlem1  19207  ovollb2lem  19253  sca2rab  19277  ovolscalem1  19278  ovolsca  19280  itg2mulc  19508  itg2cnlem2  19523  c1liplem1  19749  lhop1  19767  aalioulem4  20121  aaliou2b  20127  aaliou3lem2  20129  aaliou3lem3  20130  aaliou3lem8  20131  aaliou3lem6  20134  aaliou3lem7  20135  itgulm  20193  dvradcnv  20206  pserdvlem2  20213  abelthlem7  20223  abelthlem8  20224  lognegb  20353  logno1  20396  advlog  20414  advlogexp  20415  cxprec  20446  divcxp  20447  cxpsqr  20463  dvcxp1  20495  cxpcn3lem  20500  loglesqr  20511  asinlem3  20580  cxplim  20679  rlimcxp  20681  cxp2limlem  20683  cxp2lim  20684  cxploglim  20685  cxploglim2  20686  divsqrsumlem  20687  divsqrsumo1  20691  amgmlem  20697  basellem3  20734  basellem4  20735  chpval2  20871  logexprlim  20878  bclbnd  20933  bposlem9  20945  chebbnd1lem3  21034  chebbnd1  21035  chtppilimlem2  21037  chtppilim  21038  chebbnd2  21040  chto1lb  21041  chpchtlim  21042  chpo1ubb  21044  rplogsumlem1  21047  rplogsumlem2  21048  dchrvmasumlem1  21058  dchrvmasum2lem  21059  dchrisum0lema  21077  dchrisum0lem1b  21078  dchrisum0lem1  21079  dchrisum0lem2a  21080  dchrisum0lem2  21081  dchrisum0lem3  21082  dchrisum0  21083  mulogsumlem  21094  mulog2sumlem1  21097  mulog2sumlem2  21098  vmalogdivsum2  21101  log2sumbnd  21107  selberg3lem1  21120  selberg3lem2  21121  selberg4lem1  21123  selberg4  21124  selberg34r  21134  pntrlog2bndlem2  21141  pntrlog2bndlem3  21142  pntrlog2bndlem4  21143  pntrlog2bndlem5  21144  pntpbnd1a  21148  pntpbnd2  21150  pntibndlem1  21152  pntibndlem2  21154  pntlemd  21157  pntlemc  21158  pntlemb  21160  pntlemq  21164  pntlemr  21165  pntlemj  21166  pntlemf  21168  pntlemo  21170  pntlem3  21172  pntleml  21174  pnt  21177  padicabvcxp  21195  ostth2lem4  21199  ostth2  21200  ostth3  21201  smcnlem  22043  blocnilem  22155  ubthlem2  22223  bcm1n  23989  rnlogbval  24198  nnlogbexp  24202  logbrec  24203  probmeasb  24469  zetacvg  24580  lgamucov  24603  faclimlem1  25122  faclimlem3  25124  faclim  25125  iprodfac  25126  itg2addnc  25961  ftc1cnnclem  25980  geomcau  26158  cntotbnd  26198  heibor1lem  26211  rrndstprj2  26233  rrncmslem  26234  pell1qrgaplem  26629  pellfund14  26654  rmxyneg  26676  rmxy1  26678  rmxy0  26679  jm2.23  26760  proot1ex  27191  stoweidlem1  27420  stoweidlem3  27422  stoweidlem7  27426  stoweidlem11  27430  stoweidlem14  27433  stoweidlem24  27443  stoweidlem25  27444  stoweidlem26  27445  stoweidlem42  27461  stoweidlem51  27470  stoweidlem59  27478  stoweidlem62  27481  wallispilem4  27487  wallispilem5  27488  wallispi  27489  wallispi2lem1  27490  stirlinglem4  27496  stirlinglem8  27500  stirlinglem12  27504  stirlinglem15  27507
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-resscn 8982
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-in 3272  df-ss 3279  df-rp 10547
  Copyright terms: Public domain W3C validator