Theorem rpcn 12669

Description: A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)

Assertion

Ref	Expression
rpcn	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)

Proof of Theorem rpcn

Step	Hyp	Ref	Expression
1		rpre 12667	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	recnd 10934	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-rp 12660

This theorem is referenced by:  rpcnne0  12677  rpmtmip  12683  divge1  12727  ltdifltdiv  13482  modvalr  13520  flpmodeq  13522  mulmod0  13525  negmod0  13526  modlt  13528  moddiffl  13530  modvalp1  13538  modid  13544  modid0  13545  modcyc  13554  modcyc2  13555  modadd1  13556  muladdmodid  13559  modmuladdnn0  13563  negmod  13564  modm1p1mod0  13570  modmul1  13572  2txmodxeq0  13579  2submod  13580  moddi  13587  sqrlem2  14883  sqrtdiv  14905  caurcvgr  15313  o1fsum  15453  divrcnv  15492  efgt1p2  15751  efgt1p  15752  rpmsubg  20574  uniioombl  24658  abelthlem8  25503  pilem1  25515  logne0  25640  logneg  25648  advlogexp  25715  logcxp  25729  cxprec  25746  cxpmul  25748  abscxp  25752  logsqrt  25764  dvcxp1  25798  dvcxp2  25799  dvsqrt  25800  cxpcn2  25804  loglesqrt  25816  relogbreexp  25830  relogbzexp  25831  relogbmul  25832  relogbdiv  25834  relogbexp  25835  relogbcxp  25840  relogbcxpb  25842  relogbf  25846  logbgt0b  25848  rlimcnp  26020  efrlim  26024  cxplim  26026  sqrtlim  26027  cxploglim  26032  logdifbnd  26048  harmonicbnd4  26065  rpdmgm  26079  logfaclbnd  26275  logexprlim  26278  logfacrlim2  26279  vmadivsum  26535  dchrisum0lem1a  26539  dchrvmasumlema  26553  dchrisum0lem1  26569  dchrisum0lem2  26571  mudivsum  26583  mulogsumlem  26584  logdivsum  26586  selberg2lem  26603  selberg2  26604  pntrmax  26617  selbergr  26621  pntibndlem1  26642  pntlem3  26662  blocnilem  29067  nmcexi  30289  nmcopexi  30290  nmcfnexi  30314  dp20h  31055  dpexpp1  31084  0dp2dp  31085  sqsscirc1  31760  logdivsqrle  32530  taupilem3  35417  taupilem1  35419  poimirlem29  35733  heicant  35739  itg2addnclem3  35757  itg2gt0cn  35759  ftc1anclem6  35782  ftc1anclem8  35784  areacirclem1  35792  areacirclem4  35795  areacirc  35797  isbnd2  35868  cntotbnd  35881  heiborlem6  35901  heiborlem7  35902  dvrelog3  40001  irrapxlem5  40564  2timesgt  42716  xralrple2  42783  recnnltrp  42806  rpgtrecnn  42809  rrpsscn  43019  stirlinglem14  43518  fourierdlem73  43610  divge1b  45741  divgt1b  45742  fldivmod  45752  relogbmulbexp  45795  relogbdivb  45796  itschlc0yqe  45994  itschlc0xyqsol1  46000  itsclc0xyqsolr  46003  amgmwlem  46392