Theorem rpcn 12903

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11011  ℝ⁺crp 12892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-rp 12893

This theorem is referenced by:  rpcnne0  12911  rpmtmip  12918  divge1  12962  ltdifltdiv  13740  modvalr  13778  flpmodeq  13780  mulmod0  13783  negmod0  13784  modlt  13786  moddiffl  13788  modvalp1  13796  modid  13802  modid0  13803  modcyc  13812  modcyc2  13813  modadd1  13814  muladdmodid  13819  modmuladdnn0  13824  negmod  13825  modm1p1mod0  13831  modmul1  13833  2txmodxeq0  13840  2submod  13841  moddi  13848  01sqrexlem2  15152  sqrtdiv  15174  caurcvgr  15583  o1fsum  15722  divrcnv  15761  efgt1p2  16025  efgt1p  16026  rpmsubg  21370  uniioombl  25518  abelthlem8  26377  pilem1  26389  logne0  26516  logneg  26525  advlogexp  26592  logcxp  26606  cxprec  26623  cxpmul  26625  abscxp  26629  logsqrt  26641  dvcxp1  26677  dvcxp2  26678  dvsqrt  26679  cxpcn2  26684  loglesqrt  26699  relogbreexp  26713  relogbzexp  26714  relogbmul  26715  relogbdiv  26717  relogbexp  26718  relogbcxp  26723  relogbcxpb  26725  relogbf  26729  logbgt0b  26731  rlimcnp  26903  efrlim  26907  efrlimOLD  26908  cxplim  26910  sqrtlim  26911  cxploglim  26916  logdifbnd  26932  harmonicbnd4  26949  rpdmgm  26963  logfaclbnd  27161  logexprlim  27164  logfacrlim2  27165  vmadivsum  27421  dchrisum0lem1a  27425  dchrvmasumlema  27439  dchrisum0lem1  27455  dchrisum0lem2  27457  mudivsum  27469  mulogsumlem  27470  logdivsum  27472  selberg2lem  27489  selberg2  27490  pntrmax  27503  selbergr  27507  pntibndlem1  27528  pntlem3  27548  blocnilem  30786  nmcexi  32008  nmcopexi  32009  nmcfnexi  32033  dp20h  32866  dpexpp1  32895  0dp2dp  32896  sqsscirc1  33942  logdivsqrle  34684  taupilem3  37384  taupilem1  37386  poimirlem29  37709  heicant  37715  itg2addnclem3  37733  itg2gt0cn  37735  ftc1anclem6  37758  ftc1anclem8  37760  areacirclem1  37768  areacirclem4  37771  areacirc  37773  isbnd2  37843  cntotbnd  37856  heiborlem6  37876  heiborlem7  37877  dvrelog3  42178  irrapxlem5  42943  2timesgt  45413  xralrple2  45477  recnnltrp  45499  rpgtrecnn  45502  rrpsscn  45712  stirlinglem14  46209  fourierdlem73  46301  fldivmod  47462  ceildivmod  47463  divge1b  48637  divgt1b  48638  relogbmulbexp  48686  relogbdivb  48687  itschlc0yqe  48885  itschlc0xyqsol1  48891  itsclc0xyqsolr  48894  amgmwlem  49927