Theorem rpcnd 13053

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 13051	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11225	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-rp 13008

This theorem is referenced by:  rpcnne0d  13060  ltaddrp2d  13085  prodge0ld  13117  iccf1o  13514  ltexp2r  14200  discr  14267  bcp1nk  14344  bcpasc  14348  01sqrexlem6  15288  sqrtdiv  15306  absdiv  15336  o1rlimmul  15660  isumrpcl  15887  isumltss  15892  expcnv  15908  mertenslem1  15928  bitsmod  16484  nmoi2  24848  reperflem  24937  icopnfcnv  25062  lebnumlem3  25083  nmoleub2lem2  25236  nmoleub3  25239  minveclem3  25549  pjthlem1  25557  ovollb2lem  25608  sca2rab  25632  ovolscalem1  25633  ovolsca  25635  itg2mulc  25867  itg2cnlem2  25882  c1liplem1  26116  lhop1  26134  aalioulem4  26457  aaliou2b  26463  aaliou3lem2  26465  aaliou3lem3  26466  aaliou3lem8  26467  aaliou3lem6  26470  aaliou3lem7  26471  itgulm  26529  dvradcnv  26542  pserdvlem2  26549  abelthlem7  26559  abelthlem8  26560  lognegb  26713  logno1  26759  advlog  26777  advlogexp  26778  cxprec  26809  divcxp  26810  cxpsqrt  26826  dvcxp1  26863  cxpcn3lem  26870  loglesqrt  26884  relogbval  26895  nnlogbexp  26904  logbrec  26905  asinlem3  26994  cxplim  27094  rlimcxp  27096  cxp2limlem  27098  cxp2lim  27099  cxploglim  27100  cxploglim2  27101  divsqrtsumlem  27102  divsqrtsumo1  27106  amgmlem  27112  zetacvg  27137  lgamucov  27160  basellem3  27205  basellem4  27206  chpval2  27340  logexprlim  27347  bclbnd  27402  bposlem9  27414  chebbnd1lem3  27593  chebbnd1  27594  chtppilimlem2  27596  chtppilim  27597  chebbnd2  27599  chto1lb  27600  chpchtlim  27601  chpo1ubb  27603  rplogsumlem1  27606  rplogsumlem2  27607  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrisum0lema  27636  dchrisum0lem1b  27637  dchrisum0lem1  27638  dchrisum0lem2a  27639  dchrisum0lem2  27640  dchrisum0lem3  27641  dchrisum0  27642  mulogsumlem  27653  mulog2sumlem1  27656  mulog2sumlem2  27657  vmalogdivsum2  27660  log2sumbnd  27666  selberg3lem1  27679  selberg3lem2  27680  selberg4lem1  27682  selberg4  27683  selberg34r  27693  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntpbnd1a  27707  pntpbnd2  27709  pntibndlem1  27711  pntibndlem2  27713  pntlemd  27716  pntlemc  27717  pntlemb  27719  pntlemq  27723  pntlemr  27724  pntlemj  27725  pntlemf  27727  pntlemo  27729  pntlem3  27731  pntleml  27733  pnt  27736  padicabvcxp  27754  ostth2lem4  27758  ostth2  27759  ostth3  27760  smcnlem  30958  blocnilem  31065  ubthlem2  31132  bcm1n  33052  probmeasb  34737  signsply0  34855  iprodgam  36105  faclimlem1  36106  faclimlem3  36108  faclim  36109  iprodfac  36110  knoppndvlem17  36979  mblfinlem3  38170  itg2addnclem3  38184  ftc1cnnclem  38202  geomcau  38270  cntotbnd  38307  heibor1lem  38320  rrndstprj2  38342  rrncmslem  38343  relogbzexpd  42605  lcmineqlem21  42678  aks4d1p1p1  42692  aks4d1p6  42710  2ap1caineq  42774  exp11d  42947  rplog11d  42968  pell1qrgaplem  43462  pellfund14  43487  rmxyneg  43509  rmxy1  43511  rmxy0  43512  jm2.23  43585  proot1ex  43785  amgm2d  44786  amgm3d  44787  amgm4d  44788  cvgdvgrat  44887  binomcxplemnn0  44923  binomcxplemnotnn0  44930  ltdivgt1  45930  xralrple4  45946  xralrple3  45947  0ellimcdiv  46221  limclner  46223  fprodsubrecnncnvlem  46479  fprodaddrecnncnvlem  46481  dvdivbd  46495  stoweidlem1  46573  stoweidlem3  46575  stoweidlem7  46579  stoweidlem11  46583  stoweidlem14  46586  stoweidlem24  46596  stoweidlem25  46597  stoweidlem26  46598  stoweidlem42  46614  stoweidlem51  46623  stoweidlem59  46631  stoweidlem62  46634  wallispilem4  46640  wallispilem5  46641  wallispi  46642  wallispi2lem1  46643  stirlinglem4  46649  stirlinglem8  46653  stirlinglem12  46657  stirlinglem15  46660  dirkercncflem4  46678  fourierdlem30  46709  fourierdlem73  46751  fourierdlem87  46765  qndenserrnbllem  46866  hoiqssbllem2  47195  dignn0flhalflem2  49247  itsclc0yqsol  49395  amgmwlem  50431  amgmlemALT  50432  amgmw2d  50433  young2d  50434