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

Theorem rpcnd 11257
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 11255 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9621 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CCcc 9489   RR+crp 11219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9548
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-in 3483  df-ss 3490  df-rp 11220
This theorem is referenced by:  rpcnne0d  11264  ltaddrp2d  11285  iccf1o  11663  ltexp2r  12189  discr  12270  bcp1nk  12362  bcpasc  12366  sqrlem6  13043  sqrtdiv  13061  absdiv  13090  o1rlimmul  13403  isumrpcl  13617  isumltss  13622  expcnv  13637  mertenslem1  13655  bitsmod  13944  nmoi2  20988  reperflem  21074  icchmeo  21192  icopnfcnv  21193  lebnumlem3  21214  nmoleub2lem2  21350  nmoleub3  21353  minveclem3  21595  pjthlem1  21603  ovollb2lem  21650  sca2rab  21674  ovolscalem1  21675  ovolsca  21677  itg2mulc  21905  itg2cnlem2  21920  c1liplem1  22148  lhop1  22166  aalioulem4  22481  aaliou2b  22487  aaliou3lem2  22489  aaliou3lem3  22490  aaliou3lem8  22491  aaliou3lem6  22494  aaliou3lem7  22495  itgulm  22553  dvradcnv  22566  pserdvlem2  22573  abelthlem7  22583  abelthlem8  22584  lognegb  22718  logno1  22761  advlog  22779  advlogexp  22780  cxprec  22811  divcxp  22812  cxpsqrt  22828  dvcxp1  22860  cxpcn3lem  22865  loglesqrt  22876  asinlem3  22946  cxplim  23045  rlimcxp  23047  cxp2limlem  23049  cxp2lim  23050  cxploglim  23051  cxploglim2  23052  divsqrtsumlem  23053  divsqrtsumo1  23057  amgmlem  23063  basellem3  23100  basellem4  23101  chpval2  23237  logexprlim  23244  bclbnd  23299  bposlem9  23311  chebbnd1lem3  23400  chebbnd1  23401  chtppilimlem2  23403  chtppilim  23404  chebbnd2  23406  chto1lb  23407  chpchtlim  23408  chpo1ubb  23410  rplogsumlem1  23413  rplogsumlem2  23414  dchrvmasumlem1  23424  dchrvmasum2lem  23425  dchrisum0lema  23443  dchrisum0lem1b  23444  dchrisum0lem1  23445  dchrisum0lem2a  23446  dchrisum0lem2  23447  dchrisum0lem3  23448  dchrisum0  23449  mulogsumlem  23460  mulog2sumlem1  23463  mulog2sumlem2  23464  vmalogdivsum2  23467  log2sumbnd  23473  selberg3lem1  23486  selberg3lem2  23487  selberg4lem1  23489  selberg4  23490  selberg34r  23500  pntrlog2bndlem2  23507  pntrlog2bndlem3  23508  pntrlog2bndlem4  23509  pntrlog2bndlem5  23510  pntpbnd1a  23514  pntpbnd2  23516  pntibndlem1  23518  pntibndlem2  23520  pntlemd  23523  pntlemc  23524  pntlemb  23526  pntlemq  23530  pntlemr  23531  pntlemj  23532  pntlemf  23534  pntlemo  23536  pntlem3  23538  pntleml  23540  pnt  23543  padicabvcxp  23561  ostth2lem4  23565  ostth2  23566  ostth3  23567  smcnlem  25299  blocnilem  25411  ubthlem2  25479  mul2lt0bi  27253  bcm1n  27284  rnlogbval  27672  nnlogbexp  27676  logbrec  27677  probmeasb  28025  zetacvg  28213  lgamucov  28236  iprodgam  28718  faclimlem1  28761  faclimlem3  28763  faclim  28764  iprodfac  28765  mblfinlem3  29646  itg2addnclem3  29661  ftc1cnnclem  29681  geomcau  29871  cntotbnd  29911  heibor1lem  29924  rrndstprj2  29946  rrncmslem  29947  pell1qrgaplem  30429  pellfund14  30454  rmxyneg  30476  rmxy1  30478  rmxy0  30479  jm2.23  30558  proot1ex  30782  oddfl  31052  0ellimcdiv  31207  limclner  31209  stoweidlem1  31317  stoweidlem3  31319  stoweidlem7  31323  stoweidlem11  31327  stoweidlem14  31330  stoweidlem24  31340  stoweidlem25  31341  stoweidlem26  31342  stoweidlem42  31358  stoweidlem51  31367  stoweidlem59  31375  stoweidlem62  31378  wallispilem4  31384  wallispilem5  31385  wallispi  31386  wallispi2lem1  31387  stirlinglem4  31393  stirlinglem8  31397  stirlinglem12  31401  stirlinglem15  31404  dirkercncflem4  31422  fourierdlem30  31453  fourierdlem73  31496  fourierdlem89  31512  fourierdlem90  31513  fourierdlem91  31514
  Copyright terms: Public domain W3C validator