Theorem rpcn 12953

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝ⁺crp 12942

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-rp 12943

This theorem is referenced by:  rpcnne0  12961  rpmtmip  12968  divge1  13012  ltdifltdiv  13793  modvalr  13831  flpmodeq  13833  mulmod0  13836  negmod0  13837  modlt  13839  moddiffl  13841  modvalp1  13849  modid  13855  modid0  13856  modcyc  13865  modcyc2  13866  modadd1  13867  muladdmodid  13872  modmuladdnn0  13877  negmod  13878  modm1p1mod0  13884  modmul1  13886  2txmodxeq0  13893  2submod  13894  moddi  13901  01sqrexlem2  15205  sqrtdiv  15227  caurcvgr  15636  o1fsum  15776  divrcnv  15817  efgt1p2  16081  efgt1p  16082  rpmsubg  21411  uniioombl  25556  abelthlem8  26404  pilem1  26416  logne0  26543  logneg  26552  advlogexp  26619  logcxp  26633  cxprec  26650  cxpmul  26652  abscxp  26656  logsqrt  26668  dvcxp1  26704  dvcxp2  26705  dvsqrt  26706  cxpcn2  26710  loglesqrt  26725  relogbreexp  26739  relogbzexp  26740  relogbmul  26741  relogbdiv  26743  relogbexp  26744  relogbcxp  26749  relogbcxpb  26751  relogbf  26755  logbgt0b  26757  rlimcnp  26929  efrlim  26933  cxplim  26935  sqrtlim  26936  cxploglim  26941  logdifbnd  26957  harmonicbnd4  26974  rpdmgm  26988  logfaclbnd  27185  logexprlim  27188  logfacrlim2  27189  vmadivsum  27445  dchrisum0lem1a  27449  dchrvmasumlema  27463  dchrisum0lem1  27479  dchrisum0lem2  27481  mudivsum  27493  mulogsumlem  27494  logdivsum  27496  selberg2lem  27513  selberg2  27514  pntrmax  27527  selbergr  27531  pntibndlem1  27552  pntlem3  27572  blocnilem  30875  nmcexi  32097  nmcopexi  32098  nmcfnexi  32122  dp20h  32938  dpexpp1  32967  0dp2dp  32968  sqsscirc1  34052  logdivsqrle  34794  taupilem3  37633  taupilem1  37635  poimirlem29  37970  heicant  37976  itg2addnclem3  37994  itg2gt0cn  37996  ftc1anclem6  38019  ftc1anclem8  38021  areacirclem1  38029  areacirclem4  38032  areacirc  38034  isbnd2  38104  cntotbnd  38117  heiborlem6  38137  heiborlem7  38138  dvrelog3  42504  irrapxlem5  43254  2timesgt  45721  xralrple2  45784  recnnltrp  45806  rpgtrecnn  45809  rrpsscn  46018  stirlinglem14  46515  fourierdlem73  46607  fldivmod  47792  ceildivmod  47793  divge1b  48988  divgt1b  48989  relogbmulbexp  49037  relogbdivb  49038  itschlc0yqe  49236  itschlc0xyqsol1  49242  itsclc0xyqsolr  49245  amgmwlem  50277