Theorem rpcn 12962

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-rp 12952

This theorem is referenced by:  rpcnne0  12970  rpmtmip  12977  divge1  13021  ltdifltdiv  13796  modvalr  13834  flpmodeq  13836  mulmod0  13839  negmod0  13840  modlt  13842  moddiffl  13844  modvalp1  13852  modid  13858  modid0  13859  modcyc  13868  modcyc2  13869  modadd1  13870  muladdmodid  13875  modmuladdnn0  13880  negmod  13881  modm1p1mod0  13887  modmul1  13889  2txmodxeq0  13896  2submod  13897  moddi  13904  01sqrexlem2  15209  sqrtdiv  15231  caurcvgr  15640  o1fsum  15779  divrcnv  15818  efgt1p2  16082  efgt1p  16083  rpmsubg  21348  uniioombl  25490  abelthlem8  26349  pilem1  26361  logne0  26488  logneg  26497  advlogexp  26564  logcxp  26578  cxprec  26595  cxpmul  26597  abscxp  26601  logsqrt  26613  dvcxp1  26649  dvcxp2  26650  dvsqrt  26651  cxpcn2  26656  loglesqrt  26671  relogbreexp  26685  relogbzexp  26686  relogbmul  26687  relogbdiv  26689  relogbexp  26690  relogbcxp  26695  relogbcxpb  26697  relogbf  26701  logbgt0b  26703  rlimcnp  26875  efrlim  26879  efrlimOLD  26880  cxplim  26882  sqrtlim  26883  cxploglim  26888  logdifbnd  26904  harmonicbnd4  26921  rpdmgm  26935  logfaclbnd  27133  logexprlim  27136  logfacrlim2  27137  vmadivsum  27393  dchrisum0lem1a  27397  dchrvmasumlema  27411  dchrisum0lem1  27427  dchrisum0lem2  27429  mudivsum  27441  mulogsumlem  27442  logdivsum  27444  selberg2lem  27461  selberg2  27462  pntrmax  27475  selbergr  27479  pntibndlem1  27500  pntlem3  27520  blocnilem  30733  nmcexi  31955  nmcopexi  31956  nmcfnexi  31980  dp20h  32799  dpexpp1  32828  0dp2dp  32829  sqsscirc1  33898  logdivsqrle  34641  taupilem3  37307  taupilem1  37309  poimirlem29  37643  heicant  37649  itg2addnclem3  37667  itg2gt0cn  37669  ftc1anclem6  37692  ftc1anclem8  37694  areacirclem1  37702  areacirclem4  37705  areacirc  37707  isbnd2  37777  cntotbnd  37790  heiborlem6  37810  heiborlem7  37811  dvrelog3  42053  irrapxlem5  42814  2timesgt  45286  xralrple2  45350  recnnltrp  45373  rpgtrecnn  45376  rrpsscn  45586  stirlinglem14  46085  fourierdlem73  46177  fldivmod  47339  ceildivmod  47340  divge1b  48501  divgt1b  48502  relogbmulbexp  48550  relogbdivb  48551  itschlc0yqe  48749  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  amgmwlem  49791