Theorem rpcn 13028

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11136  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-resscn 11195

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-ss 3950  df-rp 13018

This theorem is referenced by:  rpcnne0  13036  rpmtmip  13042  divge1  13086  ltdifltdiv  13857  modvalr  13895  flpmodeq  13897  mulmod0  13900  negmod0  13901  modlt  13903  moddiffl  13905  modvalp1  13913  modid  13919  modid0  13920  modcyc  13929  modcyc2  13930  modadd1  13931  muladdmodid  13934  modmuladdnn0  13939  negmod  13940  modm1p1mod0  13946  modmul1  13948  2txmodxeq0  13955  2submod  13956  moddi  13963  01sqrexlem2  15265  sqrtdiv  15287  caurcvgr  15693  o1fsum  15832  divrcnv  15871  efgt1p2  16133  efgt1p  16134  rpmsubg  21416  uniioombl  25579  abelthlem8  26438  pilem1  26450  logne0  26576  logneg  26585  advlogexp  26652  logcxp  26666  cxprec  26683  cxpmul  26685  abscxp  26689  logsqrt  26701  dvcxp1  26737  dvcxp2  26738  dvsqrt  26739  cxpcn2  26744  loglesqrt  26759  relogbreexp  26773  relogbzexp  26774  relogbmul  26775  relogbdiv  26777  relogbexp  26778  relogbcxp  26783  relogbcxpb  26785  relogbf  26789  logbgt0b  26791  rlimcnp  26963  efrlim  26967  efrlimOLD  26968  cxplim  26970  sqrtlim  26971  cxploglim  26976  logdifbnd  26992  harmonicbnd4  27009  rpdmgm  27023  logfaclbnd  27221  logexprlim  27224  logfacrlim2  27225  vmadivsum  27481  dchrisum0lem1a  27485  dchrvmasumlema  27499  dchrisum0lem1  27515  dchrisum0lem2  27517  mudivsum  27529  mulogsumlem  27530  logdivsum  27532  selberg2lem  27549  selberg2  27550  pntrmax  27563  selbergr  27567  pntibndlem1  27588  pntlem3  27608  blocnilem  30770  nmcexi  31992  nmcopexi  31993  nmcfnexi  32017  dp20h  32808  dpexpp1  32837  0dp2dp  32838  sqsscirc1  33848  logdivsqrle  34606  taupilem3  37261  taupilem1  37263  poimirlem29  37597  heicant  37603  itg2addnclem3  37621  itg2gt0cn  37623  ftc1anclem6  37646  ftc1anclem8  37648  areacirclem1  37656  areacirclem4  37659  areacirc  37661  isbnd2  37731  cntotbnd  37744  heiborlem6  37764  heiborlem7  37765  dvrelog3  42007  irrapxlem5  42782  2timesgt  45245  xralrple2  45310  recnnltrp  45333  rpgtrecnn  45336  rrpsscn  45548  stirlinglem14  46047  fourierdlem73  46139  fldivmod  47286  ceildivmod  47287  divge1b  48375  divgt1b  48376  relogbmulbexp  48428  relogbdivb  48429  itschlc0yqe  48627  itschlc0xyqsol1  48633  itsclc0xyqsolr  48636  amgmwlem  49317