Theorem rpcn 12984

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 12982	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	recnd 11242	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-rp 12975

This theorem is referenced by:  rpcnne0  12992  rpmtmip  12998  divge1  13042  ltdifltdiv  13799  modvalr  13837  flpmodeq  13839  mulmod0  13842  negmod0  13843  modlt  13845  moddiffl  13847  modvalp1  13855  modid  13861  modid0  13862  modcyc  13871  modcyc2  13872  modadd1  13873  muladdmodid  13876  modmuladdnn0  13880  negmod  13881  modm1p1mod0  13887  modmul1  13889  2txmodxeq0  13896  2submod  13897  moddi  13904  01sqrexlem2  15190  sqrtdiv  15212  caurcvgr  15620  o1fsum  15759  divrcnv  15798  efgt1p2  16057  efgt1p  16058  rpmsubg  21009  uniioombl  25106  abelthlem8  25951  pilem1  25963  logne0  26088  logneg  26096  advlogexp  26163  logcxp  26177  cxprec  26194  cxpmul  26196  abscxp  26200  logsqrt  26212  dvcxp1  26248  dvcxp2  26249  dvsqrt  26250  cxpcn2  26254  loglesqrt  26266  relogbreexp  26280  relogbzexp  26281  relogbmul  26282  relogbdiv  26284  relogbexp  26285  relogbcxp  26290  relogbcxpb  26292  relogbf  26296  logbgt0b  26298  rlimcnp  26470  efrlim  26474  cxplim  26476  sqrtlim  26477  cxploglim  26482  logdifbnd  26498  harmonicbnd4  26515  rpdmgm  26529  logfaclbnd  26725  logexprlim  26728  logfacrlim2  26729  vmadivsum  26985  dchrisum0lem1a  26989  dchrvmasumlema  27003  dchrisum0lem1  27019  dchrisum0lem2  27021  mudivsum  27033  mulogsumlem  27034  logdivsum  27036  selberg2lem  27053  selberg2  27054  pntrmax  27067  selbergr  27071  pntibndlem1  27092  pntlem3  27112  blocnilem  30057  nmcexi  31279  nmcopexi  31280  nmcfnexi  31304  dp20h  32045  dpexpp1  32074  0dp2dp  32075  sqsscirc1  32888  logdivsqrle  33662  taupilem3  36200  taupilem1  36202  poimirlem29  36517  heicant  36523  itg2addnclem3  36541  itg2gt0cn  36543  ftc1anclem6  36566  ftc1anclem8  36568  areacirclem1  36576  areacirclem4  36579  areacirc  36581  isbnd2  36651  cntotbnd  36664  heiborlem6  36684  heiborlem7  36685  dvrelog3  40930  irrapxlem5  41564  2timesgt  43998  xralrple2  44064  recnnltrp  44087  rpgtrecnn  44090  rrpsscn  44304  stirlinglem14  44803  fourierdlem73  44895  divge1b  47193  divgt1b  47194  fldivmod  47204  relogbmulbexp  47247  relogbdivb  47248  itschlc0yqe  47446  itschlc0xyqsol1  47452  itsclc0xyqsolr  47455  amgmwlem  47849