Theorem rpcn 12928

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝ⁺crp 12917

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 11095

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 3402  df-ss 3920  df-rp 12918

This theorem is referenced by:  rpcnne0  12936  rpmtmip  12943  divge1  12987  ltdifltdiv  13766  modvalr  13804  flpmodeq  13806  mulmod0  13809  negmod0  13810  modlt  13812  moddiffl  13814  modvalp1  13822  modid  13828  modid0  13829  modcyc  13838  modcyc2  13839  modadd1  13840  muladdmodid  13845  modmuladdnn0  13850  negmod  13851  modm1p1mod0  13857  modmul1  13859  2txmodxeq0  13866  2submod  13867  moddi  13874  01sqrexlem2  15178  sqrtdiv  15200  caurcvgr  15609  o1fsum  15748  divrcnv  15787  efgt1p2  16051  efgt1p  16052  rpmsubg  21398  uniioombl  25558  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  26724  loglesqrt  26739  relogbreexp  26753  relogbzexp  26754  relogbmul  26755  relogbdiv  26757  relogbexp  26758  relogbcxp  26763  relogbcxpb  26765  relogbf  26769  logbgt0b  26771  rlimcnp  26943  efrlim  26947  efrlimOLD  26948  cxplim  26950  sqrtlim  26951  cxploglim  26956  logdifbnd  26972  harmonicbnd4  26989  rpdmgm  27003  logfaclbnd  27201  logexprlim  27204  logfacrlim2  27205  vmadivsum  27461  dchrisum0lem1a  27465  dchrvmasumlema  27479  dchrisum0lem1  27495  dchrisum0lem2  27497  mudivsum  27509  mulogsumlem  27510  logdivsum  27512  selberg2lem  27529  selberg2  27530  pntrmax  27543  selbergr  27547  pntibndlem1  27568  pntlem3  27588  blocnilem  30891  nmcexi  32113  nmcopexi  32114  nmcfnexi  32138  dp20h  32970  dpexpp1  32999  0dp2dp  33000  sqsscirc1  34085  logdivsqrle  34827  taupilem3  37568  taupilem1  37570  poimirlem29  37894  heicant  37900  itg2addnclem3  37918  itg2gt0cn  37920  ftc1anclem6  37943  ftc1anclem8  37945  areacirclem1  37953  areacirclem4  37956  areacirc  37958  isbnd2  38028  cntotbnd  38041  heiborlem6  38061  heiborlem7  38062  dvrelog3  42429  irrapxlem5  43177  2timesgt  45644  xralrple2  45707  recnnltrp  45729  rpgtrecnn  45732  rrpsscn  45942  stirlinglem14  46439  fourierdlem73  46531  fldivmod  47692  ceildivmod  47693  divge1b  48866  divgt1b  48867  relogbmulbexp  48915  relogbdivb  48916  itschlc0yqe  49114  itschlc0xyqsol1  49120  itsclc0xyqsolr  49123  amgmwlem  50155