Theorem rpcn 12944

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11027  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-rp 12934

This theorem is referenced by:  rpcnne0  12952  rpmtmip  12959  divge1  13003  ltdifltdiv  13784  modvalr  13822  flpmodeq  13824  mulmod0  13827  negmod0  13828  modlt  13830  moddiffl  13832  modvalp1  13840  modid  13846  modid0  13847  modcyc  13856  modcyc2  13857  modadd1  13858  muladdmodid  13863  modmuladdnn0  13868  negmod  13869  modm1p1mod0  13875  modmul1  13877  2txmodxeq0  13884  2submod  13885  moddi  13892  01sqrexlem2  15196  sqrtdiv  15218  caurcvgr  15627  o1fsum  15767  divrcnv  15808  efgt1p2  16072  efgt1p  16073  rpmsubg  21421  uniioombl  25566  abelthlem8  26417  pilem1  26429  logne0  26556  logneg  26565  advlogexp  26632  logcxp  26646  cxprec  26663  cxpmul  26665  abscxp  26669  logsqrt  26681  dvcxp1  26717  dvcxp2  26718  dvsqrt  26719  cxpcn2  26723  loglesqrt  26738  relogbreexp  26752  relogbzexp  26753  relogbmul  26754  relogbdiv  26756  relogbexp  26757  relogbcxp  26762  relogbcxpb  26764  relogbf  26768  logbgt0b  26770  rlimcnp  26942  efrlim  26946  efrlimOLD  26947  cxplim  26949  sqrtlim  26950  cxploglim  26955  logdifbnd  26971  harmonicbnd4  26988  rpdmgm  27002  logfaclbnd  27199  logexprlim  27202  logfacrlim2  27203  vmadivsum  27459  dchrisum0lem1a  27463  dchrvmasumlema  27477  dchrisum0lem1  27493  dchrisum0lem2  27495  mudivsum  27507  mulogsumlem  27508  logdivsum  27510  selberg2lem  27527  selberg2  27528  pntrmax  27541  selbergr  27545  pntibndlem1  27566  pntlem3  27586  blocnilem  30890  nmcexi  32112  nmcopexi  32113  nmcfnexi  32137  dp20h  32953  dpexpp1  32982  0dp2dp  32983  sqsscirc1  34068  logdivsqrle  34810  taupilem3  37649  taupilem1  37651  poimirlem29  37984  heicant  37990  itg2addnclem3  38008  itg2gt0cn  38010  ftc1anclem6  38033  ftc1anclem8  38035  areacirclem1  38043  areacirclem4  38046  areacirc  38048  isbnd2  38118  cntotbnd  38131  heiborlem6  38151  heiborlem7  38152  dvrelog3  42518  irrapxlem5  43272  2timesgt  45739  xralrple2  45802  recnnltrp  45824  rpgtrecnn  45827  rrpsscn  46036  stirlinglem14  46533  fourierdlem73  46625  fldivmod  47804  ceildivmod  47805  divge1b  49000  divgt1b  49001  relogbmulbexp  49049  relogbdivb  49050  itschlc0yqe  49248  itschlc0xyqsol1  49254  itsclc0xyqsolr  49257  amgmwlem  50289