Theorem rpcn 13028

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11099  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923  df-rp 13018

This theorem is referenced by:  rpcnne0  13036  rpmtmip  13043  divge1  13087  ltdifltdiv  13869  modvalr  13907  flpmodeq  13909  mulmod0  13912  negmod0  13913  modlt  13915  moddiffl  13917  modvalp1  13925  modid  13931  modid0  13932  modcyc  13941  modcyc2  13942  modadd1  13943  muladdmodid  13948  modmuladdnn0  13953  negmod  13954  modm1p1mod0  13960  modmul1  13962  2txmodxeq0  13969  2submod  13970  moddi  13977  01sqrexlem2  15296  sqrtdiv  15318  caurcvgr  15727  o1fsum  15867  divrcnv  15908  efgt1p2  16171  efgt1p  16172  rpmsubg  21562  uniioombl  25729  abelthlem8  26580  pilem1  26592  logne0  26722  logneg  26731  advlogexp  26798  logcxp  26812  cxprec  26829  cxpmul  26831  abscxp  26835  logsqrt  26847  dvcxp1  26883  dvcxp2  26884  dvsqrt  26885  cxpcn2  26889  loglesqrt  26904  relogbreexp  26918  relogbzexp  26919  relogbmul  26920  relogbdiv  26922  relogbexp  26923  relogbcxp  26928  relogbcxpb  26930  relogbf  26934  logbgt0b  26936  rlimcnp  27108  efrlim  27112  cxplim  27114  sqrtlim  27115  cxploglim  27120  logdifbnd  27136  harmonicbnd4  27153  rpdmgm  27167  logfaclbnd  27364  logexprlim  27367  logfacrlim2  27368  vmadivsum  27624  dchrisum0lem1a  27628  dchrvmasumlema  27642  dchrisum0lem1  27658  dchrisum0lem2  27660  mudivsum  27672  mulogsumlem  27673  logdivsum  27675  selberg2lem  27692  selberg2  27693  pntrmax  27706  selbergr  27710  pntibndlem1  27731  pntlem3  27751  blocnilem  31134  nmcexi  32356  nmcopexi  32357  nmcfnexi  32381  dp20h  33176  dpexpp1  33205  0dp2dp  33206  sqsscirc1  34276  logdivsqrle  35015  taupilem3  37941  taupilem1  37943  poimirlem29  38278  heicant  38284  itg2addnclem3  38302  itg2gt0cn  38304  ftc1anclem6  38327  ftc1anclem8  38329  areacirclem1  38337  areacirclem4  38340  areacirc  38342  isbnd2  38412  cntotbnd  38425  heiborlem6  38445  heiborlem7  38446  dvrelog3  42810  irrapxlem5  43533  2timesgt  45987  xralrple2  46050  recnnltrp  46072  rpgtrecnn  46075  rrpsscn  46284  stirlinglem14  46781  fourierdlem73  46873  fldivmod  48058  ceildivmod  48059  divge1b  49269  divgt1b  49270  relogbmulbexp  49318  relogbdivb  49319  itschlc0yqe  49517  itschlc0xyqsol1  49523  itsclc0xyqsolr  49526  amgmwlem  50579