Theorem rpcn 12983

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11107  ℝ⁺crp 12973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-rp 12974

This theorem is referenced by:  rpcnne0  12991  rpmtmip  12997  divge1  13041  ltdifltdiv  13798  modvalr  13836  flpmodeq  13838  mulmod0  13841  negmod0  13842  modlt  13844  moddiffl  13846  modvalp1  13854  modid  13860  modid0  13861  modcyc  13870  modcyc2  13871  modadd1  13872  muladdmodid  13875  modmuladdnn0  13879  negmod  13880  modm1p1mod0  13886  modmul1  13888  2txmodxeq0  13895  2submod  13896  moddi  13903  01sqrexlem2  15189  sqrtdiv  15211  caurcvgr  15619  o1fsum  15758  divrcnv  15797  efgt1p2  16056  efgt1p  16057  rpmsubg  21008  uniioombl  25105  abelthlem8  25950  pilem1  25962  logne0  26087  logneg  26095  advlogexp  26162  logcxp  26176  cxprec  26193  cxpmul  26195  abscxp  26199  logsqrt  26211  dvcxp1  26245  dvcxp2  26246  dvsqrt  26247  cxpcn2  26251  loglesqrt  26263  relogbreexp  26277  relogbzexp  26278  relogbmul  26279  relogbdiv  26281  relogbexp  26282  relogbcxp  26287  relogbcxpb  26289  relogbf  26293  logbgt0b  26295  rlimcnp  26467  efrlim  26471  cxplim  26473  sqrtlim  26474  cxploglim  26479  logdifbnd  26495  harmonicbnd4  26512  rpdmgm  26526  logfaclbnd  26722  logexprlim  26725  logfacrlim2  26726  vmadivsum  26982  dchrisum0lem1a  26986  dchrvmasumlema  27000  dchrisum0lem1  27016  dchrisum0lem2  27018  mudivsum  27030  mulogsumlem  27031  logdivsum  27033  selberg2lem  27050  selberg2  27051  pntrmax  27064  selbergr  27068  pntibndlem1  27089  pntlem3  27109  blocnilem  30052  nmcexi  31274  nmcopexi  31275  nmcfnexi  31299  dp20h  32040  dpexpp1  32069  0dp2dp  32070  sqsscirc1  32883  logdivsqrle  33657  taupilem3  36195  taupilem1  36197  poimirlem29  36512  heicant  36518  itg2addnclem3  36536  itg2gt0cn  36538  ftc1anclem6  36561  ftc1anclem8  36563  areacirclem1  36571  areacirclem4  36574  areacirc  36576  isbnd2  36646  cntotbnd  36659  heiborlem6  36679  heiborlem7  36680  dvrelog3  40925  irrapxlem5  41554  2timesgt  43988  xralrple2  44054  recnnltrp  44077  rpgtrecnn  44080  rrpsscn  44294  stirlinglem14  44793  fourierdlem73  44885  divge1b  47183  divgt1b  47184  fldivmod  47194  relogbmulbexp  47237  relogbdivb  47238  itschlc0yqe  47436  itschlc0xyqsol1  47442  itsclc0xyqsolr  47445  amgmwlem  47839