Theorem rpcnd 12988

Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem rpcnd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 12986	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11173	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-rp 12943

This theorem is referenced by:  rpcnne0d  12995  ltaddrp2d  13020  prodge0ld  13052  iccf1o  13449  ltexp2r  14135  discr  14202  bcp1nk  14279  bcpasc  14283  01sqrexlem6  15209  sqrtdiv  15227  absdiv  15257  o1rlimmul  15581  isumrpcl  15808  isumltss  15813  expcnv  15829  mertenslem1  15849  bitsmod  16405  nmoi2  24695  reperflem  24784  icopnfcnv  24909  lebnumlem3  24930  nmoleub2lem2  25083  nmoleub3  25086  minveclem3  25396  pjthlem1  25404  ovollb2lem  25455  sca2rab  25479  ovolscalem1  25480  ovolsca  25482  itg2mulc  25714  itg2cnlem2  25729  c1liplem1  25963  lhop1  25981  aalioulem4  26301  aaliou2b  26307  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem8  26311  aaliou3lem6  26314  aaliou3lem7  26315  itgulm  26373  dvradcnv  26386  pserdvlem2  26393  abelthlem7  26403  abelthlem8  26404  lognegb  26554  logno1  26600  advlog  26618  advlogexp  26619  cxprec  26650  divcxp  26651  cxpsqrt  26667  dvcxp1  26704  cxpcn3lem  26711  loglesqrt  26725  relogbval  26736  nnlogbexp  26745  logbrec  26746  asinlem3  26835  cxplim  26935  rlimcxp  26937  cxp2limlem  26939  cxp2lim  26940  cxploglim  26941  cxploglim2  26942  divsqrtsumlem  26943  divsqrtsumo1  26947  amgmlem  26953  zetacvg  26978  lgamucov  27001  basellem3  27046  basellem4  27047  chpval2  27181  logexprlim  27188  bclbnd  27243  bposlem9  27255  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem2  27437  chtppilim  27438  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ubb  27444  rplogsumlem1  27447  rplogsumlem2  27448  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  mulogsumlem  27494  mulog2sumlem1  27497  mulog2sumlem2  27498  vmalogdivsum2  27501  log2sumbnd  27507  selberg3lem1  27520  selberg3lem2  27521  selberg4lem1  27523  selberg4  27524  selberg34r  27534  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem1  27552  pntibndlem2  27554  pntlemd  27557  pntlemc  27558  pntlemb  27560  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemo  27570  pntlem3  27572  pntleml  27574  pnt  27577  padicabvcxp  27595  ostth2lem4  27599  ostth2  27600  ostth3  27601  smcnlem  30768  blocnilem  30875  ubthlem2  30942  bcm1n  32868  probmeasb  34574  signsply0  34695  iprodgam  35924  faclimlem1  35925  faclimlem3  35927  faclim  35928  iprodfac  35929  knoppndvlem17  36788  mblfinlem3  37980  itg2addnclem3  37994  ftc1cnnclem  38012  geomcau  38080  cntotbnd  38117  heibor1lem  38130  rrndstprj2  38152  rrncmslem  38153  relogbzexpd  42415  lcmineqlem21  42488  aks4d1p1p1  42502  aks4d1p6  42520  2ap1caineq  42584  exp11d  42758  rplog11d  42779  pell1qrgaplem  43301  pellfund14  43326  rmxyneg  43348  rmxy1  43350  rmxy0  43351  jm2.23  43424  proot1ex  43624  amgm2d  44625  amgm3d  44626  amgm4d  44627  cvgdvgrat  44740  binomcxplemnn0  44776  binomcxplemnotnn0  44783  ltdivgt1  45786  xralrple4  45802  xralrple3  45803  0ellimcdiv  46077  limclner  46079  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvdivbd  46351  stoweidlem1  46429  stoweidlem3  46431  stoweidlem7  46435  stoweidlem11  46439  stoweidlem14  46442  stoweidlem24  46452  stoweidlem25  46453  stoweidlem26  46454  stoweidlem42  46470  stoweidlem51  46479  stoweidlem59  46487  stoweidlem62  46490  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  stirlinglem4  46505  stirlinglem8  46509  stirlinglem12  46513  stirlinglem15  46516  dirkercncflem4  46534  fourierdlem30  46565  fourierdlem73  46607  fourierdlem87  46621  qndenserrnbllem  46722  hoiqssbllem2  47051  dignn0flhalflem2  49086  itsclc0yqsol  49234  amgmwlem  50271  amgmlemALT  50272  amgmw2d  50273  young2d  50274