Theorem rpcn 12722

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 10853  ℝ⁺crp 12712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-resscn 10912

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-in 3898  df-ss 3908  df-rp 12713

This theorem is referenced by:  rpcnne0  12730  rpmtmip  12736  divge1  12780  ltdifltdiv  13535  modvalr  13573  flpmodeq  13575  mulmod0  13578  negmod0  13579  modlt  13581  moddiffl  13583  modvalp1  13591  modid  13597  modid0  13598  modcyc  13607  modcyc2  13608  modadd1  13609  muladdmodid  13612  modmuladdnn0  13616  negmod  13617  modm1p1mod0  13623  modmul1  13625  2txmodxeq0  13632  2submod  13633  moddi  13640  sqrlem2  14936  sqrtdiv  14958  caurcvgr  15366  o1fsum  15506  divrcnv  15545  efgt1p2  15804  efgt1p  15805  rpmsubg  20643  uniioombl  24734  abelthlem8  25579  pilem1  25591  logne0  25716  logneg  25724  advlogexp  25791  logcxp  25805  cxprec  25822  cxpmul  25824  abscxp  25828  logsqrt  25840  dvcxp1  25874  dvcxp2  25875  dvsqrt  25876  cxpcn2  25880  loglesqrt  25892  relogbreexp  25906  relogbzexp  25907  relogbmul  25908  relogbdiv  25910  relogbexp  25911  relogbcxp  25916  relogbcxpb  25918  relogbf  25922  logbgt0b  25924  rlimcnp  26096  efrlim  26100  cxplim  26102  sqrtlim  26103  cxploglim  26108  logdifbnd  26124  harmonicbnd4  26141  rpdmgm  26155  logfaclbnd  26351  logexprlim  26354  logfacrlim2  26355  vmadivsum  26611  dchrisum0lem1a  26615  dchrvmasumlema  26629  dchrisum0lem1  26645  dchrisum0lem2  26647  mudivsum  26659  mulogsumlem  26660  logdivsum  26662  selberg2lem  26679  selberg2  26680  pntrmax  26693  selbergr  26697  pntibndlem1  26718  pntlem3  26738  blocnilem  29145  nmcexi  30367  nmcopexi  30368  nmcfnexi  30392  dp20h  31132  dpexpp1  31161  0dp2dp  31162  sqsscirc1  31837  logdivsqrle  32609  taupilem3  35469  taupilem1  35471  poimirlem29  35785  heicant  35791  itg2addnclem3  35809  itg2gt0cn  35811  ftc1anclem6  35834  ftc1anclem8  35836  areacirclem1  35844  areacirclem4  35847  areacirc  35849  isbnd2  35920  cntotbnd  35933  heiborlem6  35953  heiborlem7  35954  dvrelog3  40053  irrapxlem5  40628  2timesgt  42780  xralrple2  42847  recnnltrp  42870  rpgtrecnn  42873  rrpsscn  43083  stirlinglem14  43582  fourierdlem73  43674  divge1b  45805  divgt1b  45806  fldivmod  45816  relogbmulbexp  45859  relogbdivb  45860  itschlc0yqe  46058  itschlc0xyqsol1  46064  itsclc0xyqsolr  46067  amgmwlem  46458