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

Theorem rpcnd 11269
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 11267 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9625 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   RR+crp 11231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-resscn 9552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475  df-rp 11232
This theorem is referenced by:  rpcnne0d  11276  ltaddrp2d  11297  iccf1o  11675  ltexp2r  12204  discr  12285  bcp1nk  12377  bcpasc  12381  sqrlem6  13063  sqrtdiv  13081  absdiv  13110  o1rlimmul  13423  isumrpcl  13637  isumltss  13642  expcnv  13657  mertenslem1  13675  bitsmod  14068  nmoi2  21215  reperflem  21301  icchmeo  21419  icopnfcnv  21420  lebnumlem3  21441  nmoleub2lem2  21577  nmoleub3  21580  minveclem3  21822  pjthlem1  21830  ovollb2lem  21877  sca2rab  21901  ovolscalem1  21902  ovolsca  21904  itg2mulc  22132  itg2cnlem2  22147  c1liplem1  22375  lhop1  22393  aalioulem4  22709  aaliou2b  22715  aaliou3lem2  22717  aaliou3lem3  22718  aaliou3lem8  22719  aaliou3lem6  22722  aaliou3lem7  22723  itgulm  22781  dvradcnv  22794  pserdvlem2  22801  abelthlem7  22811  abelthlem8  22812  lognegb  22952  logno1  22995  advlog  23013  advlogexp  23014  cxprec  23045  divcxp  23046  cxpsqrt  23062  dvcxp1  23094  cxpcn3lem  23099  loglesqrt  23110  asinlem3  23180  cxplim  23279  rlimcxp  23281  cxp2limlem  23283  cxp2lim  23284  cxploglim  23285  cxploglim2  23286  divsqrtsumlem  23287  divsqrtsumo1  23291  amgmlem  23297  basellem3  23334  basellem4  23335  chpval2  23471  logexprlim  23478  bclbnd  23533  bposlem9  23545  chebbnd1lem3  23634  chebbnd1  23635  chtppilimlem2  23637  chtppilim  23638  chebbnd2  23640  chto1lb  23641  chpchtlim  23642  chpo1ubb  23644  rplogsumlem1  23647  rplogsumlem2  23648  dchrvmasumlem1  23658  dchrvmasum2lem  23659  dchrisum0lema  23677  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0lem3  23682  dchrisum0  23683  mulogsumlem  23694  mulog2sumlem1  23697  mulog2sumlem2  23698  vmalogdivsum2  23701  log2sumbnd  23707  selberg3lem1  23720  selberg3lem2  23721  selberg4lem1  23723  selberg4  23724  selberg34r  23734  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntpbnd1a  23748  pntpbnd2  23750  pntibndlem1  23752  pntibndlem2  23754  pntlemd  23757  pntlemc  23758  pntlemb  23760  pntlemq  23764  pntlemr  23765  pntlemj  23766  pntlemf  23768  pntlemo  23770  pntlem3  23772  pntleml  23774  pnt  23777  padicabvcxp  23795  ostth2lem4  23799  ostth2  23800  ostth3  23801  smcnlem  25585  blocnilem  25697  ubthlem2  25765  bcm1n  27578  rnlogbval  27994  nnlogbexp  27998  logbrec  27999  probmeasb  28347  signsply0  28486  zetacvg  28535  lgamucov  28558  iprodgam  29101  faclimlem1  29144  faclimlem3  29146  faclim  29147  iprodfac  29148  mblfinlem3  30029  itg2addnclem3  30044  ftc1cnnclem  30064  geomcau  30228  cntotbnd  30268  heibor1lem  30281  rrndstprj2  30303  rrncmslem  30304  pell1qrgaplem  30785  pellfund14  30810  rmxyneg  30832  rmxy1  30834  rmxy0  30835  jm2.23  30914  proot1ex  31137  cvgdvgrat  31170  0ellimcdiv  31609  limclner  31611  dvdivbd  31674  stoweidlem1  31737  stoweidlem3  31739  stoweidlem7  31743  stoweidlem11  31747  stoweidlem14  31750  stoweidlem24  31760  stoweidlem25  31761  stoweidlem26  31762  stoweidlem42  31778  stoweidlem51  31787  stoweidlem59  31795  stoweidlem62  31798  wallispilem4  31804  wallispilem5  31805  wallispi  31806  wallispi2lem1  31807  stirlinglem4  31813  stirlinglem8  31817  stirlinglem12  31821  stirlinglem15  31824  dirkercncflem4  31842  fourierdlem30  31873  fourierdlem73  31916  fourierdlem87  31930
  Copyright terms: Public domain W3C validator