Theorem rpcn 12222

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

Syntax hints:   → wi 4   ∈ wcel 2051  ℂcc 10339  ℝ⁺crp 12210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752  ax-resscn 10398

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rab 3099  df-in 3838  df-ss 3845  df-rp 12211

This theorem is referenced by:  rpcnne0  12230  rpmtmip  12236  divge1  12280  ltdifltdiv  13025  modvalr  13061  flpmodeq  13063  mulmod0  13066  negmod0  13067  modlt  13069  moddiffl  13071  modvalp1  13079  modid  13085  modid0  13086  modcyc  13095  modcyc2  13096  modadd1  13097  muladdmodid  13100  modmuladdnn0  13104  negmod  13105  modm1p1mod0  13111  modmul1  13113  2txmodxeq0  13120  2submod  13121  moddi  13128  sqrlem2  14470  sqrtdiv  14492  caurcvgr  14897  o1fsum  15034  divrcnv  15073  efgt1p2  15333  efgt1p  15334  rpmsubg  20326  uniioombl  23908  abelthlem8  24745  pilem1  24757  logne0  24879  logneg  24887  advlogexp  24954  logcxp  24968  cxprec  24985  cxpmul  24987  abscxp  24991  logsqrt  25003  dvcxp1  25037  dvcxp2  25038  dvsqrt  25039  cxpcn2  25043  loglesqrt  25055  relogbreexp  25069  relogbzexp  25070  relogbmul  25071  relogbdiv  25073  relogbexp  25074  relogbcxp  25079  relogbcxpb  25081  relogbf  25085  logbgt0b  25087  rlimcnp  25260  efrlim  25264  cxplim  25266  sqrtlim  25267  cxploglim  25272  logdifbnd  25288  harmonicbnd4  25305  rpdmgm  25319  logfaclbnd  25515  logexprlim  25518  logfacrlim2  25519  vmadivsum  25775  dchrisum0lem1a  25779  dchrvmasumlema  25793  dchrisum0lem1  25809  dchrisum0lem2  25811  mudivsum  25823  mulogsumlem  25824  logdivsum  25826  selberg2lem  25843  selberg2  25844  pntrmax  25857  selbergr  25861  pntibndlem1  25882  pntlem3  25902  blocnilem  28373  nmcexi  29599  nmcopexi  29600  nmcfnexi  29624  dp20h  30325  dpexpp1  30354  0dp2dp  30355  sqsscirc1  30827  logdivsqrle  31601  taupilem3  34082  taupilem1  34084  poimirlem29  34402  heicant  34408  itg2addnclem3  34426  itg2gt0cn  34428  ftc1anclem6  34453  ftc1anclem8  34455  areacirclem1  34463  areacirclem4  34466  areacirc  34468  isbnd2  34543  cntotbnd  34556  heiborlem6  34576  heiborlem7  34577  irrapxlem5  38860  2timesgt  41018  xralrple2  41086  recnnltrp  41109  rpgtrecnn  41113  rrpsscn  41335  stirlinglem14  41838  fourierdlem73  41930  divge1b  43970  divgt1b  43971  fldivmod  43981  relogbmulbexp  44024  relogbdivb  44025  itschlc0yqe  44150  itschlc0xyqsol1  44156  itsclc0xyqsolr  44159  amgmwlem  44305