Theorem rpcn 13132

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11199  ℝ⁺crp 13121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3915  df-rp 13122

This theorem is used by:  rpcnne0  13140  rpmtmip  13147  divge1  13191  ltdifltdiv  13975  modvalr  14013  flpmodeq  14015  mulmod0  14018  negmod0  14019  modlt  14021  moddiffl  14023  modvalp1  14031  modid  14037  modid0  14038  modcyc  14047  modcyc2  14048  modadd1  14049  muladdmodid  14054  modmuladdnn0  14059  negmod  14060  modm1p1mod0  14066  modmul1  14068  2txmodxeq0  14075  2submod  14076  moddi  14083  01sqrexlem2  15411  sqrtdiv  15433  caurcvgr  15842  o1fsum  15981  divrcnv  16022  efgt1p2  16283  efgt1p  16284  rpmsubg  21738  uniioombl  25911  abelthlem8  26767  pilem1  26779  logne0  26908  logneg  26917  advlogexp  26984  logcxp  26998  cxprec  27015  cxpmul  27017  abscxp  27021  logsqrt  27033  dvcxp1  27069  dvcxp2  27070  dvsqrt  27071  cxpcn2  27075  loglesqrt  27090  relogbreexp  27104  relogbzexp  27105  relogbmul  27106  relogbdiv  27108  relogbexp  27109  relogbcxp  27114  relogbcxpb  27116  relogbf  27120  logbgt0b  27122  rlimcnp  27294  efrlim  27298  cxplim  27300  sqrtlim  27301  cxploglim  27306  logdifbnd  27322  harmonicbnd4  27339  rpdmgm  27353  logfaclbnd  27550  logexprlim  27553  logfacrlim2  27554  vmadivsum  27810  dchrisum0lem1a  27814  dchrvmasumlema  27828  dchrisum0lem1  27844  dchrisum0lem2  27846  mudivsum  27858  mulogsumlem  27859  logdivsum  27861  selberg2lem  27878  selberg2  27879  pntrmax  27892  selbergr  27896  pntibndlem1  27917  pntlem3  27937  blocnilem  31407  nmcexi  32629  nmcopexi  32630  nmcfnexi  32654  dp20h  33446  dpexpp1  33475  0dp2dp  33476  sqsscirc1  34541  logdivsqrle  35280  taupilem3  38242  taupilem1  38244  poimirlem29  38569  heicant  38575  itg2addnclem3  38593  itg2gt0cn  38595  ftc1anclem6  38618  ftc1anclem8  38620  areacirclem1  38628  areacirclem4  38631  areacirc  38633  isbnd2  38719  cntotbnd  38732  heiborlem6  38752  heiborlem7  38753  dvrelog3  43117  irrapxlem5  43834  2timesgt  46305  xralrple2  46367  recnnltrp  46389  rpgtrecnn  46392  rrpsscn  46601  stirlinglem14  47098  fourierdlem73  47190  fldivmod  48415  ceildivmod  48416  divge1b  49625  divgt1b  49626  relogbmulbexp  49674  relogbdivb  49675  itschlc0yqe  49873  itschlc0xyqsol1  49879  itsclc0xyqsolr  49882  amgmwlem  50988