Theorem rpcn 13134

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11201  ℝ⁺crp 13123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-rp 13124

This theorem is used by:  rpcnne0  13142  rpmtmip  13149  divge1  13193  ltdifltdiv  13977  modvalr  14015  flpmodeq  14017  mulmod0  14020  negmod0  14021  modlt  14023  moddiffl  14025  modvalp1  14033  modid  14039  modid0  14040  modcyc  14049  modcyc2  14050  modadd1  14051  muladdmodid  14056  modmuladdnn0  14061  negmod  14062  modm1p1mod0  14068  modmul1  14070  2txmodxeq0  14077  2submod  14078  moddi  14085  01sqrexlem2  15415  sqrtdiv  15437  caurcvgr  15846  o1fsum  15985  divrcnv  16026  efgt1p2  16287  efgt1p  16288  rpmsubg  21742  uniioombl  25915  abelthlem8  26771  pilem1  26783  logne0  26912  logneg  26921  advlogexp  26988  logcxp  27002  cxprec  27019  cxpmul  27021  abscxp  27025  logsqrt  27037  dvcxp1  27073  dvcxp2  27074  dvsqrt  27075  cxpcn2  27079  loglesqrt  27094  relogbreexp  27108  relogbzexp  27109  relogbmul  27110  relogbdiv  27112  relogbexp  27113  relogbcxp  27118  relogbcxpb  27120  relogbf  27124  logbgt0b  27126  rlimcnp  27298  efrlim  27302  cxplim  27304  sqrtlim  27305  cxploglim  27310  logdifbnd  27326  harmonicbnd4  27343  rpdmgm  27357  logfaclbnd  27554  logexprlim  27557  logfacrlim2  27558  vmadivsum  27814  dchrisum0lem1a  27818  dchrvmasumlema  27832  dchrisum0lem1  27848  dchrisum0lem2  27850  mudivsum  27862  mulogsumlem  27863  logdivsum  27865  selberg2lem  27882  selberg2  27883  pntrmax  27896  selbergr  27900  pntibndlem1  27921  pntlem3  27941  blocnilem  31411  nmcexi  32633  nmcopexi  32634  nmcfnexi  32658  dp20h  33491  dpexpp1  33520  0dp2dp  33521  sqsscirc1  34586  logdivsqrle  35325  taupilem3  38333  taupilem1  38335  poimirlem29  38660  heicant  38666  itg2addnclem3  38684  itg2gt0cn  38686  ftc1anclem6  38709  ftc1anclem8  38711  areacirclem1  38719  areacirclem4  38722  areacirc  38724  isbnd2  38810  cntotbnd  38823  heiborlem6  38843  heiborlem7  38844  dvrelog3  43208  irrapxlem5  43926  2timesgt  46397  xralrple2  46459  recnnltrp  46481  rpgtrecnn  46484  rrpsscn  46693  stirlinglem14  47190  fourierdlem73  47282  fldivmod  48507  ceildivmod  48508  divge1b  49717  divgt1b  49718  relogbmulbexp  49766  relogbdivb  49767  itschlc0yqe  49965  itschlc0xyqsol1  49971  itsclc0xyqsolr  49974  amgmwlem  51155