Theorem rpcn 13001

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11068  ℝ⁺crp 12990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3921  df-rp 12991

This theorem is referenced by:  rpcnne0  13009  rpmtmip  13016  divge1  13060  ltdifltdiv  13841  modvalr  13879  flpmodeq  13881  mulmod0  13884  negmod0  13885  modlt  13887  moddiffl  13889  modvalp1  13897  modid  13903  modid0  13904  modcyc  13913  modcyc2  13914  modadd1  13915  muladdmodid  13920  modmuladdnn0  13925  negmod  13926  modm1p1mod0  13932  modmul1  13934  2txmodxeq0  13941  2submod  13942  moddi  13949  01sqrexlem2  15253  sqrtdiv  15275  caurcvgr  15684  o1fsum  15824  divrcnv  15865  efgt1p2  16129  efgt1p  16130  rpmsubg  21463  uniioombl  25631  abelthlem8  26479  pilem1  26491  logne0  26621  logneg  26630  advlogexp  26697  logcxp  26711  cxprec  26728  cxpmul  26730  abscxp  26734  logsqrt  26746  dvcxp1  26782  dvcxp2  26783  dvsqrt  26784  cxpcn2  26788  loglesqrt  26803  relogbreexp  26817  relogbzexp  26818  relogbmul  26819  relogbdiv  26821  relogbexp  26822  relogbcxp  26827  relogbcxpb  26829  relogbf  26833  logbgt0b  26835  rlimcnp  27007  efrlim  27011  cxplim  27013  sqrtlim  27014  cxploglim  27019  logdifbnd  27035  harmonicbnd4  27052  rpdmgm  27066  logfaclbnd  27263  logexprlim  27266  logfacrlim2  27267  vmadivsum  27523  dchrisum0lem1a  27527  dchrvmasumlema  27541  dchrisum0lem1  27557  dchrisum0lem2  27559  mudivsum  27571  mulogsumlem  27572  logdivsum  27574  selberg2lem  27591  selberg2  27592  pntrmax  27605  selbergr  27609  pntibndlem1  27630  pntlem3  27650  blocnilem  30953  nmcexi  32175  nmcopexi  32176  nmcfnexi  32200  dp20h  33017  dpexpp1  33046  0dp2dp  33047  sqsscirc1  34166  logdivsqrle  34908  taupilem3  37775  taupilem1  37777  poimirlem29  38112  heicant  38118  itg2addnclem3  38136  itg2gt0cn  38138  ftc1anclem6  38161  ftc1anclem8  38163  areacirclem1  38171  areacirclem4  38174  areacirc  38176  isbnd2  38246  cntotbnd  38259  heiborlem6  38279  heiborlem7  38280  dvrelog3  42646  irrapxlem5  43367  2timesgt  45831  xralrple2  45894  recnnltrp  45916  rpgtrecnn  45919  rrpsscn  46128  stirlinglem14  46625  fourierdlem73  46717  fldivmod  47902  ceildivmod  47903  divge1b  49098  divgt1b  49099  relogbmulbexp  49147  relogbdivb  49148  itschlc0yqe  49346  itschlc0xyqsol1  49352  itsclc0xyqsolr  49355  amgmwlem  50387