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 11263	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11127  ℝ⁺crp 13008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11186

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943  df-rp 13009

This theorem is referenced by:  rpcnne0d  13060  ltaddrp2d  13085  prodge0ld  13117  iccf1o  13513  ltexp2r  14191  discr  14258  bcp1nk  14335  bcpasc  14339  01sqrexlem6  15266  sqrtdiv  15284  absdiv  15314  o1rlimmul  15635  isumrpcl  15859  isumltss  15864  expcnv  15880  mertenslem1  15900  bitsmod  16455  nmoi2  24669  reperflem  24758  icchmeoOLD  24890  icopnfcnv  24891  lebnumlem3  24913  nmoleub2lem2  25067  nmoleub3  25070  minveclem3  25381  pjthlem1  25389  ovollb2lem  25441  sca2rab  25465  ovolscalem1  25466  ovolsca  25468  itg2mulc  25700  itg2cnlem2  25715  c1liplem1  25953  lhop1  25971  aalioulem4  26295  aaliou2b  26301  aaliou3lem2  26303  aaliou3lem3  26304  aaliou3lem8  26305  aaliou3lem6  26308  aaliou3lem7  26309  itgulm  26369  dvradcnv  26382  pserdvlem2  26390  abelthlem7  26400  abelthlem8  26401  lognegb  26551  logno1  26597  advlog  26615  advlogexp  26616  cxprec  26647  divcxp  26648  cxpsqrt  26664  dvcxp1  26701  cxpcn3lem  26709  loglesqrt  26723  relogbval  26734  nnlogbexp  26743  logbrec  26744  asinlem3  26833  cxplim  26934  rlimcxp  26936  cxp2limlem  26938  cxp2lim  26939  cxploglim  26940  cxploglim2  26941  divsqrtsumlem  26942  divsqrtsumo1  26946  amgmlem  26952  zetacvg  26977  lgamucov  27000  basellem3  27045  basellem4  27046  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  30678  blocnilem  30785  ubthlem2  30852  bcm1n  32772  probmeasb  34462  signsply0  34583  iprodgam  35759  faclimlem1  35760  faclimlem3  35762  faclim  35763  iprodfac  35764  knoppndvlem17  36546  mblfinlem3  37683  itg2addnclem3  37697  ftc1cnnclem  37715  geomcau  37783  cntotbnd  37820  heibor1lem  37833  rrndstprj2  37855  rrncmslem  37856  relogbzexpd  41988  lcmineqlem21  42062  aks4d1p1p1  42076  aks4d1p6  42094  2ap1caineq  42158  exp11d  42375  rplog11d  42396  pell1qrgaplem  42896  pellfund14  42921  rmxyneg  42944  rmxy1  42946  rmxy0  42947  jm2.23  43020  proot1ex  43220  amgm2d  44222  amgm3d  44223  amgm4d  44224  cvgdvgrat  44337  binomcxplemnn0  44373  binomcxplemnotnn0  44380  ltdivgt1  45383  xralrple4  45400  xralrple3  45401  0ellimcdiv  45678  limclner  45680  fprodsubrecnncnvlem  45936  fprodaddrecnncnvlem  45938  dvdivbd  45952  stoweidlem1  46030  stoweidlem3  46032  stoweidlem7  46036  stoweidlem11  46040  stoweidlem14  46043  stoweidlem24  46053  stoweidlem25  46054  stoweidlem26  46055  stoweidlem42  46071  stoweidlem51  46080  stoweidlem59  46088  stoweidlem62  46091  wallispilem4  46097  wallispilem5  46098  wallispi  46099  wallispi2lem1  46100  stirlinglem4  46106  stirlinglem8  46110  stirlinglem12  46114  stirlinglem15  46117  dirkercncflem4  46135  fourierdlem30  46166  fourierdlem73  46208  fourierdlem87  46222  qndenserrnbllem  46323  hoiqssbllem2  46652  dignn0flhalflem2  48596  itsclc0yqsol  48744  amgmwlem  49666  amgmlemALT  49667  amgmw2d  49668  young2d  49669