Theorem rpcn 13057

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

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

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 2734  ax-resscn 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-rp 13047

This theorem is used by:  rpcnne0  13065  rpmtmip  13072  divge1  13116  ltdifltdiv  13899  modvalr  13937  flpmodeq  13939  mulmod0  13942  negmod0  13943  modlt  13945  moddiffl  13947  modvalp1  13955  modid  13961  modid0  13962  modcyc  13971  modcyc2  13972  modadd1  13973  muladdmodid  13978  modmuladdnn0  13983  negmod  13984  modm1p1mod0  13990  modmul1  13992  2txmodxeq0  13999  2submod  14000  moddi  14007  01sqrexlem2  15334  sqrtdiv  15356  caurcvgr  15765  o1fsum  15904  divrcnv  15945  efgt1p2  16208  efgt1p  16209  rpmsubg  21650  uniioombl  25823  abelthlem8  26682  pilem1  26694  logne0  26824  logneg  26833  advlogexp  26900  logcxp  26914  cxprec  26931  cxpmul  26933  abscxp  26937  logsqrt  26949  dvcxp1  26985  dvcxp2  26986  dvsqrt  26987  cxpcn2  26991  loglesqrt  27006  relogbreexp  27020  relogbzexp  27021  relogbmul  27022  relogbdiv  27024  relogbexp  27025  relogbcxp  27030  relogbcxpb  27032  relogbf  27036  logbgt0b  27038  rlimcnp  27210  efrlim  27214  cxplim  27216  sqrtlim  27217  cxploglim  27222  logdifbnd  27238  harmonicbnd4  27255  rpdmgm  27269  logfaclbnd  27466  logexprlim  27469  logfacrlim2  27470  vmadivsum  27726  dchrisum0lem1a  27730  dchrvmasumlema  27744  dchrisum0lem1  27760  dchrisum0lem2  27762  mudivsum  27774  mulogsumlem  27775  logdivsum  27777  selberg2lem  27794  selberg2  27795  pntrmax  27808  selbergr  27812  pntibndlem1  27833  pntlem3  27853  blocnilem  31293  nmcexi  32515  nmcopexi  32516  nmcfnexi  32540  dp20h  33332  dpexpp1  33361  0dp2dp  33362  sqsscirc1  34426  logdivsqrle  35166  taupilem3  38079  taupilem1  38081  poimirlem29  38406  heicant  38412  itg2addnclem3  38430  itg2gt0cn  38432  ftc1anclem6  38455  ftc1anclem8  38457  areacirclem1  38465  areacirclem4  38468  areacirc  38470  isbnd2  38541  cntotbnd  38554  heiborlem6  38574  heiborlem7  38575  dvrelog3  42939  irrapxlem5  43675  2timesgt  46129  xralrple2  46192  recnnltrp  46214  rpgtrecnn  46217  rrpsscn  46426  stirlinglem14  46923  fourierdlem73  47015  fldivmod  48240  ceildivmod  48241  divge1b  49450  divgt1b  49451  relogbmulbexp  49499  relogbdivb  49500  itschlc0yqe  49698  itschlc0xyqsol1  49704  itsclc0xyqsolr  49707  amgmwlem  50828