Theorem rpcn 13045

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11116  ℝ⁺crp 13034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925  df-rp 13035

This theorem is used by:  rpcnne0  13053  rpmtmip  13060  divge1  13104  ltdifltdiv  13887  modvalr  13925  flpmodeq  13927  mulmod0  13930  negmod0  13931  modlt  13933  moddiffl  13935  modvalp1  13943  modid  13949  modid0  13950  modcyc  13959  modcyc2  13960  modadd1  13961  muladdmodid  13966  modmuladdnn0  13971  negmod  13972  modm1p1mod0  13978  modmul1  13980  2txmodxeq0  13987  2submod  13988  moddi  13995  01sqrexlem2  15320  sqrtdiv  15342  caurcvgr  15751  o1fsum  15891  divrcnv  15932  efgt1p2  16195  efgt1p  16196  rpmsubg  21618  uniioombl  25785  abelthlem8  26639  pilem1  26651  logne0  26781  logneg  26790  advlogexp  26857  logcxp  26871  cxprec  26888  cxpmul  26890  abscxp  26894  logsqrt  26906  dvcxp1  26942  dvcxp2  26943  dvsqrt  26944  cxpcn2  26948  loglesqrt  26963  relogbreexp  26977  relogbzexp  26978  relogbmul  26979  relogbdiv  26981  relogbexp  26982  relogbcxp  26987  relogbcxpb  26989  relogbf  26993  logbgt0b  26995  rlimcnp  27167  efrlim  27171  cxplim  27173  sqrtlim  27174  cxploglim  27179  logdifbnd  27195  harmonicbnd4  27212  rpdmgm  27226  logfaclbnd  27423  logexprlim  27426  logfacrlim2  27427  vmadivsum  27683  dchrisum0lem1a  27687  dchrvmasumlema  27701  dchrisum0lem1  27717  dchrisum0lem2  27719  mudivsum  27731  mulogsumlem  27732  logdivsum  27734  selberg2lem  27751  selberg2  27752  pntrmax  27765  selbergr  27769  pntibndlem1  27790  pntlem3  27810  blocnilem  31193  nmcexi  32415  nmcopexi  32416  nmcfnexi  32440  dp20h  33235  dpexpp1  33264  0dp2dp  33265  sqsscirc1  34329  logdivsqrle  35069  taupilem3  38004  taupilem1  38006  poimirlem29  38341  heicant  38347  itg2addnclem3  38365  itg2gt0cn  38367  ftc1anclem6  38390  ftc1anclem8  38392  areacirclem1  38400  areacirclem4  38403  areacirc  38405  isbnd2  38475  cntotbnd  38488  heiborlem6  38508  heiborlem7  38509  dvrelog3  42873  irrapxlem5  43594  2timesgt  46048  xralrple2  46111  recnnltrp  46133  rpgtrecnn  46136  rrpsscn  46345  stirlinglem14  46842  fourierdlem73  46934  fldivmod  48122  ceildivmod  48123  divge1b  49333  divgt1b  49334  relogbmulbexp  49382  relogbdivb  49383  itschlc0yqe  49581  itschlc0xyqsol1  49587  itsclc0xyqsolr  49590  amgmwlem  50691