Theorem rpcn 13018

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-rp 13008

This theorem is referenced by:  rpcnne0  13026  rpmtmip  13033  divge1  13077  ltdifltdiv  13858  modvalr  13896  flpmodeq  13898  mulmod0  13901  negmod0  13902  modlt  13904  moddiffl  13906  modvalp1  13914  modid  13920  modid0  13921  modcyc  13930  modcyc2  13931  modadd1  13932  muladdmodid  13937  modmuladdnn0  13942  negmod  13943  modm1p1mod0  13949  modmul1  13951  2txmodxeq0  13958  2submod  13959  moddi  13966  01sqrexlem2  15284  sqrtdiv  15306  caurcvgr  15715  o1fsum  15855  divrcnv  15896  efgt1p2  16160  efgt1p  16161  rpmsubg  21541  uniioombl  25709  abelthlem8  26560  pilem1  26572  logne0  26702  logneg  26711  advlogexp  26778  logcxp  26792  cxprec  26809  cxpmul  26811  abscxp  26815  logsqrt  26827  dvcxp1  26863  dvcxp2  26864  dvsqrt  26865  cxpcn2  26869  loglesqrt  26884  relogbreexp  26898  relogbzexp  26899  relogbmul  26900  relogbdiv  26902  relogbexp  26903  relogbcxp  26908  relogbcxpb  26910  relogbf  26914  logbgt0b  26916  rlimcnp  27088  efrlim  27092  cxplim  27094  sqrtlim  27095  cxploglim  27100  logdifbnd  27116  harmonicbnd4  27133  rpdmgm  27147  logfaclbnd  27344  logexprlim  27347  logfacrlim2  27348  vmadivsum  27604  dchrisum0lem1a  27608  dchrvmasumlema  27622  dchrisum0lem1  27638  dchrisum0lem2  27640  mudivsum  27652  mulogsumlem  27653  logdivsum  27655  selberg2lem  27672  selberg2  27673  pntrmax  27686  selbergr  27690  pntibndlem1  27711  pntlem3  27731  blocnilem  31065  nmcexi  32287  nmcopexi  32288  nmcfnexi  32312  dp20h  33111  dpexpp1  33140  0dp2dp  33141  sqsscirc1  34215  logdivsqrle  34954  taupilem3  37823  taupilem1  37825  poimirlem29  38160  heicant  38166  itg2addnclem3  38184  itg2gt0cn  38186  ftc1anclem6  38209  ftc1anclem8  38211  areacirclem1  38219  areacirclem4  38222  areacirc  38224  isbnd2  38294  cntotbnd  38307  heiborlem6  38327  heiborlem7  38328  dvrelog3  42694  irrapxlem5  43415  2timesgt  45865  xralrple2  45928  recnnltrp  45950  rpgtrecnn  45953  rrpsscn  46162  stirlinglem14  46659  fourierdlem73  46751  fldivmod  47936  ceildivmod  47937  divge1b  49143  divgt1b  49144  relogbmulbexp  49192  relogbdivb  49193  itschlc0yqe  49391  itschlc0xyqsol1  49397  itsclc0xyqsolr  49400  amgmwlem  50431