Theorem rpcn 12969

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℝ⁺crp 12958

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 2702  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-rp 12959

This theorem is referenced by:  rpcnne0  12977  rpmtmip  12984  divge1  13028  ltdifltdiv  13803  modvalr  13841  flpmodeq  13843  mulmod0  13846  negmod0  13847  modlt  13849  moddiffl  13851  modvalp1  13859  modid  13865  modid0  13866  modcyc  13875  modcyc2  13876  modadd1  13877  muladdmodid  13882  modmuladdnn0  13887  negmod  13888  modm1p1mod0  13894  modmul1  13896  2txmodxeq0  13903  2submod  13904  moddi  13911  01sqrexlem2  15216  sqrtdiv  15238  caurcvgr  15647  o1fsum  15786  divrcnv  15825  efgt1p2  16089  efgt1p  16090  rpmsubg  21355  uniioombl  25497  abelthlem8  26356  pilem1  26368  logne0  26495  logneg  26504  advlogexp  26571  logcxp  26585  cxprec  26602  cxpmul  26604  abscxp  26608  logsqrt  26620  dvcxp1  26656  dvcxp2  26657  dvsqrt  26658  cxpcn2  26663  loglesqrt  26678  relogbreexp  26692  relogbzexp  26693  relogbmul  26694  relogbdiv  26696  relogbexp  26697  relogbcxp  26702  relogbcxpb  26704  relogbf  26708  logbgt0b  26710  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  cxplim  26889  sqrtlim  26890  cxploglim  26895  logdifbnd  26911  harmonicbnd4  26928  rpdmgm  26942  logfaclbnd  27140  logexprlim  27143  logfacrlim2  27144  vmadivsum  27400  dchrisum0lem1a  27404  dchrvmasumlema  27418  dchrisum0lem1  27434  dchrisum0lem2  27436  mudivsum  27448  mulogsumlem  27449  logdivsum  27451  selberg2lem  27468  selberg2  27469  pntrmax  27482  selbergr  27486  pntibndlem1  27507  pntlem3  27527  blocnilem  30740  nmcexi  31962  nmcopexi  31963  nmcfnexi  31987  dp20h  32806  dpexpp1  32835  0dp2dp  32836  sqsscirc1  33905  logdivsqrle  34648  taupilem3  37314  taupilem1  37316  poimirlem29  37650  heicant  37656  itg2addnclem3  37674  itg2gt0cn  37676  ftc1anclem6  37699  ftc1anclem8  37701  areacirclem1  37709  areacirclem4  37712  areacirc  37714  isbnd2  37784  cntotbnd  37797  heiborlem6  37817  heiborlem7  37818  dvrelog3  42060  irrapxlem5  42821  2timesgt  45293  xralrple2  45357  recnnltrp  45380  rpgtrecnn  45383  rrpsscn  45593  stirlinglem14  46092  fourierdlem73  46184  fldivmod  47343  ceildivmod  47344  divge1b  48505  divgt1b  48506  relogbmulbexp  48554  relogbdivb  48555  itschlc0yqe  48753  itschlc0xyqsol1  48759  itsclc0xyqsolr  48762  amgmwlem  49795