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

Theorem rpcnd 11016
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 11014 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9399 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   CCcc 9267   RR+crp 10978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9326
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330  df-rp 10979
This theorem is referenced by:  rpcnne0d  11023  ltaddrp2d  11044  iccf1o  11415  ltexp2r  11903  discr  11984  bcp1nk  12076  bcpasc  12080  sqrlem6  12720  sqrdiv  12738  absdiv  12767  o1rlimmul  13079  isumrpcl  13288  isumltss  13293  expcnv  13308  mertenslem1  13326  bitsmod  13614  nmoi2  20150  reperflem  20236  icchmeo  20354  icopnfcnv  20355  lebnumlem3  20376  nmoleub2lem2  20512  nmoleub3  20515  minveclem3  20757  pjthlem1  20765  ovollb2lem  20812  sca2rab  20836  ovolscalem1  20837  ovolsca  20839  itg2mulc  21066  itg2cnlem2  21081  c1liplem1  21309  lhop1  21327  aalioulem4  21685  aaliou2b  21691  aaliou3lem2  21693  aaliou3lem3  21694  aaliou3lem8  21695  aaliou3lem6  21698  aaliou3lem7  21699  itgulm  21757  dvradcnv  21770  pserdvlem2  21777  abelthlem7  21787  abelthlem8  21788  lognegb  21922  logno1  21965  advlog  21983  advlogexp  21984  cxprec  22015  divcxp  22016  cxpsqr  22032  dvcxp1  22064  cxpcn3lem  22069  loglesqr  22080  asinlem3  22150  cxplim  22249  rlimcxp  22251  cxp2limlem  22253  cxp2lim  22254  cxploglim  22255  cxploglim2  22256  divsqrsumlem  22257  divsqrsumo1  22261  amgmlem  22267  basellem3  22304  basellem4  22305  chpval2  22441  logexprlim  22448  bclbnd  22503  bposlem9  22515  chebbnd1lem3  22604  chebbnd1  22605  chtppilimlem2  22607  chtppilim  22608  chebbnd2  22610  chto1lb  22611  chpchtlim  22612  chpo1ubb  22614  rplogsumlem1  22617  rplogsumlem2  22618  dchrvmasumlem1  22628  dchrvmasum2lem  22629  dchrisum0lema  22647  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  dchrisum0lem3  22652  dchrisum0  22653  mulogsumlem  22664  mulog2sumlem1  22667  mulog2sumlem2  22668  vmalogdivsum2  22671  log2sumbnd  22677  selberg3lem1  22690  selberg3lem2  22691  selberg4lem1  22693  selberg4  22694  selberg34r  22704  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntrlog2bndlem5  22714  pntpbnd1a  22718  pntpbnd2  22720  pntibndlem1  22722  pntibndlem2  22724  pntlemd  22727  pntlemc  22728  pntlemb  22730  pntlemq  22734  pntlemr  22735  pntlemj  22736  pntlemf  22738  pntlemo  22740  pntlem3  22742  pntleml  22744  pnt  22747  padicabvcxp  22765  ostth2lem4  22769  ostth2  22770  ostth3  22771  smcnlem  23914  blocnilem  24026  ubthlem2  24094  mul2lt0bi  25866  bcm1n  25901  rnlogbval  26312  nnlogbexp  26316  logbrec  26317  probmeasb  26660  zetacvg  26848  lgamucov  26871  iprodgam  27352  faclimlem1  27395  faclimlem3  27397  faclim  27398  iprodfac  27399  mblfinlem3  28271  itg2addnclem3  28286  ftc1cnnclem  28306  geomcau  28496  cntotbnd  28536  heibor1lem  28549  rrndstprj2  28571  rrncmslem  28572  pell1qrgaplem  29056  pellfund14  29081  rmxyneg  29103  rmxy1  29105  rmxy0  29106  jm2.23  29187  proot1ex  29411  stoweidlem1  29639  stoweidlem3  29641  stoweidlem7  29645  stoweidlem11  29649  stoweidlem14  29652  stoweidlem24  29662  stoweidlem25  29663  stoweidlem26  29664  stoweidlem42  29680  stoweidlem51  29689  stoweidlem59  29697  stoweidlem62  29700  wallispilem4  29706  wallispilem5  29707  wallispi  29708  wallispi2lem1  29709  stirlinglem4  29715  stirlinglem8  29719  stirlinglem12  29723  stirlinglem15  29726
  Copyright terms: Public domain W3C validator