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

Theorem rpcnd 11143
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 11141 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9526 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   CCcc 9394   RR+crp 11105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9453
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-in 3446  df-ss 3453  df-rp 11106
This theorem is referenced by:  rpcnne0d  11150  ltaddrp2d  11171  iccf1o  11549  ltexp2r  12040  discr  12121  bcp1nk  12213  bcpasc  12217  sqrlem6  12858  sqrdiv  12876  absdiv  12905  o1rlimmul  13217  isumrpcl  13427  isumltss  13432  expcnv  13447  mertenslem1  13465  bitsmod  13753  nmoi2  20444  reperflem  20530  icchmeo  20648  icopnfcnv  20649  lebnumlem3  20670  nmoleub2lem2  20806  nmoleub3  20809  minveclem3  21051  pjthlem1  21059  ovollb2lem  21106  sca2rab  21130  ovolscalem1  21131  ovolsca  21133  itg2mulc  21361  itg2cnlem2  21376  c1liplem1  21604  lhop1  21622  aalioulem4  21937  aaliou2b  21943  aaliou3lem2  21945  aaliou3lem3  21946  aaliou3lem8  21947  aaliou3lem6  21950  aaliou3lem7  21951  itgulm  22009  dvradcnv  22022  pserdvlem2  22029  abelthlem7  22039  abelthlem8  22040  lognegb  22174  logno1  22217  advlog  22235  advlogexp  22236  cxprec  22267  divcxp  22268  cxpsqr  22284  dvcxp1  22316  cxpcn3lem  22321  loglesqr  22332  asinlem3  22402  cxplim  22501  rlimcxp  22503  cxp2limlem  22505  cxp2lim  22506  cxploglim  22507  cxploglim2  22508  divsqrsumlem  22509  divsqrsumo1  22513  amgmlem  22519  basellem3  22556  basellem4  22557  chpval2  22693  logexprlim  22700  bclbnd  22755  bposlem9  22767  chebbnd1lem3  22856  chebbnd1  22857  chtppilimlem2  22859  chtppilim  22860  chebbnd2  22862  chto1lb  22863  chpchtlim  22864  chpo1ubb  22866  rplogsumlem1  22869  rplogsumlem2  22870  dchrvmasumlem1  22880  dchrvmasum2lem  22881  dchrisum0lema  22899  dchrisum0lem1b  22900  dchrisum0lem1  22901  dchrisum0lem2a  22902  dchrisum0lem2  22903  dchrisum0lem3  22904  dchrisum0  22905  mulogsumlem  22916  mulog2sumlem1  22919  mulog2sumlem2  22920  vmalogdivsum2  22923  log2sumbnd  22929  selberg3lem1  22942  selberg3lem2  22943  selberg4lem1  22945  selberg4  22946  selberg34r  22956  pntrlog2bndlem2  22963  pntrlog2bndlem3  22964  pntrlog2bndlem4  22965  pntrlog2bndlem5  22966  pntpbnd1a  22970  pntpbnd2  22972  pntibndlem1  22974  pntibndlem2  22976  pntlemd  22979  pntlemc  22980  pntlemb  22982  pntlemq  22986  pntlemr  22987  pntlemj  22988  pntlemf  22990  pntlemo  22992  pntlem3  22994  pntleml  22996  pnt  22999  padicabvcxp  23017  ostth2lem4  23021  ostth2  23022  ostth3  23023  smcnlem  24264  blocnilem  24376  ubthlem2  24444  mul2lt0bi  26213  bcm1n  26244  rnlogbval  26624  nnlogbexp  26628  logbrec  26629  probmeasb  26977  zetacvg  27165  lgamucov  27188  iprodgam  27670  faclimlem1  27713  faclimlem3  27715  faclim  27716  iprodfac  27717  mblfinlem3  28598  itg2addnclem3  28613  ftc1cnnclem  28633  geomcau  28823  cntotbnd  28863  heibor1lem  28876  rrndstprj2  28898  rrncmslem  28899  pell1qrgaplem  29382  pellfund14  29407  rmxyneg  29429  rmxy1  29431  rmxy0  29432  jm2.23  29513  proot1ex  29737  stoweidlem1  29964  stoweidlem3  29966  stoweidlem7  29970  stoweidlem11  29974  stoweidlem14  29977  stoweidlem24  29987  stoweidlem25  29988  stoweidlem26  29989  stoweidlem42  30005  stoweidlem51  30014  stoweidlem59  30022  stoweidlem62  30025  wallispilem4  30031  wallispilem5  30032  wallispi  30033  wallispi2lem1  30034  stirlinglem4  30040  stirlinglem8  30044  stirlinglem12  30048  stirlinglem15  30051
  Copyright terms: Public domain W3C validator