Theorem rpcn 12951

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11034  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-rp 12941

This theorem is referenced by:  rpcnne0  12959  rpmtmip  12966  divge1  13010  ltdifltdiv  13791  modvalr  13829  flpmodeq  13831  mulmod0  13834  negmod0  13835  modlt  13837  moddiffl  13839  modvalp1  13847  modid  13853  modid0  13854  modcyc  13863  modcyc2  13864  modadd1  13865  muladdmodid  13870  modmuladdnn0  13875  negmod  13876  modm1p1mod0  13882  modmul1  13884  2txmodxeq0  13891  2submod  13892  moddi  13899  01sqrexlem2  15203  sqrtdiv  15225  caurcvgr  15634  o1fsum  15774  divrcnv  15815  efgt1p2  16079  efgt1p  16080  rpmsubg  21413  uniioombl  25581  abelthlem8  26429  pilem1  26441  logne0  26568  logneg  26577  advlogexp  26644  logcxp  26658  cxprec  26675  cxpmul  26677  abscxp  26681  logsqrt  26693  dvcxp1  26729  dvcxp2  26730  dvsqrt  26731  cxpcn2  26735  loglesqrt  26750  relogbreexp  26764  relogbzexp  26765  relogbmul  26766  relogbdiv  26768  relogbexp  26769  relogbcxp  26774  relogbcxpb  26776  relogbf  26780  logbgt0b  26782  rlimcnp  26954  efrlim  26958  cxplim  26960  sqrtlim  26961  cxploglim  26966  logdifbnd  26982  harmonicbnd4  26999  rpdmgm  27013  logfaclbnd  27210  logexprlim  27213  logfacrlim2  27214  vmadivsum  27470  dchrisum0lem1a  27474  dchrvmasumlema  27488  dchrisum0lem1  27504  dchrisum0lem2  27506  mudivsum  27518  mulogsumlem  27519  logdivsum  27521  selberg2lem  27538  selberg2  27539  pntrmax  27552  selbergr  27556  pntibndlem1  27577  pntlem3  27597  blocnilem  30900  nmcexi  32122  nmcopexi  32123  nmcfnexi  32147  dp20h  32964  dpexpp1  32993  0dp2dp  32994  sqsscirc1  34099  logdivsqrle  34841  taupilem3  37686  taupilem1  37688  poimirlem29  38023  heicant  38029  itg2addnclem3  38047  itg2gt0cn  38049  ftc1anclem6  38072  ftc1anclem8  38074  areacirclem1  38082  areacirclem4  38085  areacirc  38087  isbnd2  38157  cntotbnd  38170  heiborlem6  38190  heiborlem7  38191  dvrelog3  42557  irrapxlem5  43278  2timesgt  45743  xralrple2  45806  recnnltrp  45828  rpgtrecnn  45831  rrpsscn  46040  stirlinglem14  46537  fourierdlem73  46629  fldivmod  47814  ceildivmod  47815  divge1b  49010  divgt1b  49011  relogbmulbexp  49059  relogbdivb  49060  itschlc0yqe  49258  itschlc0xyqsol1  49264  itsclc0xyqsolr  49267  amgmwlem  50299