Theorem rpcn 13043

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11151  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-rp 13033

This theorem is referenced by:  rpcnne0  13051  rpmtmip  13057  divge1  13101  ltdifltdiv  13871  modvalr  13909  flpmodeq  13911  mulmod0  13914  negmod0  13915  modlt  13917  moddiffl  13919  modvalp1  13927  modid  13933  modid0  13934  modcyc  13943  modcyc2  13944  modadd1  13945  muladdmodid  13948  modmuladdnn0  13953  negmod  13954  modm1p1mod0  13960  modmul1  13962  2txmodxeq0  13969  2submod  13970  moddi  13977  01sqrexlem2  15279  sqrtdiv  15301  caurcvgr  15707  o1fsum  15846  divrcnv  15885  efgt1p2  16147  efgt1p  16148  rpmsubg  21467  uniioombl  25638  abelthlem8  26498  pilem1  26510  logne0  26636  logneg  26645  advlogexp  26712  logcxp  26726  cxprec  26743  cxpmul  26745  abscxp  26749  logsqrt  26761  dvcxp1  26797  dvcxp2  26798  dvsqrt  26799  cxpcn2  26804  loglesqrt  26819  relogbreexp  26833  relogbzexp  26834  relogbmul  26835  relogbdiv  26837  relogbexp  26838  relogbcxp  26843  relogbcxpb  26845  relogbf  26849  logbgt0b  26851  rlimcnp  27023  efrlim  27027  efrlimOLD  27028  cxplim  27030  sqrtlim  27031  cxploglim  27036  logdifbnd  27052  harmonicbnd4  27069  rpdmgm  27083  logfaclbnd  27281  logexprlim  27284  logfacrlim2  27285  vmadivsum  27541  dchrisum0lem1a  27545  dchrvmasumlema  27559  dchrisum0lem1  27575  dchrisum0lem2  27577  mudivsum  27589  mulogsumlem  27590  logdivsum  27592  selberg2lem  27609  selberg2  27610  pntrmax  27623  selbergr  27627  pntibndlem1  27648  pntlem3  27668  blocnilem  30833  nmcexi  32055  nmcopexi  32056  nmcfnexi  32080  dp20h  32846  dpexpp1  32875  0dp2dp  32876  sqsscirc1  33869  logdivsqrle  34644  taupilem3  37302  taupilem1  37304  poimirlem29  37636  heicant  37642  itg2addnclem3  37660  itg2gt0cn  37662  ftc1anclem6  37685  ftc1anclem8  37687  areacirclem1  37695  areacirclem4  37698  areacirc  37700  isbnd2  37770  cntotbnd  37783  heiborlem6  37803  heiborlem7  37804  dvrelog3  42047  irrapxlem5  42814  2timesgt  45239  xralrple2  45304  recnnltrp  45327  rpgtrecnn  45330  rrpsscn  45544  stirlinglem14  46043  fourierdlem73  46135  fldivmod  47278  ceildivmod  47279  divge1b  48358  divgt1b  48359  relogbmulbexp  48411  relogbdivb  48412  itschlc0yqe  48610  itschlc0xyqsol1  48616  itsclc0xyqsolr  48619  amgmwlem  49033