Theorem rpcn 13024

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11132  ℝ⁺crp 13013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-resscn 11191

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-ss 3948  df-rp 13014

This theorem is referenced by:  rpcnne0  13032  rpmtmip  13038  divge1  13082  ltdifltdiv  13856  modvalr  13894  flpmodeq  13896  mulmod0  13899  negmod0  13900  modlt  13902  moddiffl  13904  modvalp1  13912  modid  13918  modid0  13919  modcyc  13928  modcyc2  13929  modadd1  13930  muladdmodid  13933  modmuladdnn0  13938  negmod  13939  modm1p1mod0  13945  modmul1  13947  2txmodxeq0  13954  2submod  13955  moddi  13962  01sqrexlem2  15267  sqrtdiv  15289  caurcvgr  15695  o1fsum  15834  divrcnv  15873  efgt1p2  16137  efgt1p  16138  rpmsubg  21404  uniioombl  25547  abelthlem8  26406  pilem1  26418  logne0  26545  logneg  26554  advlogexp  26621  logcxp  26635  cxprec  26652  cxpmul  26654  abscxp  26658  logsqrt  26670  dvcxp1  26706  dvcxp2  26707  dvsqrt  26708  cxpcn2  26713  loglesqrt  26728  relogbreexp  26742  relogbzexp  26743  relogbmul  26744  relogbdiv  26746  relogbexp  26747  relogbcxp  26752  relogbcxpb  26754  relogbf  26758  logbgt0b  26760  rlimcnp  26932  efrlim  26936  efrlimOLD  26937  cxplim  26939  sqrtlim  26940  cxploglim  26945  logdifbnd  26961  harmonicbnd4  26978  rpdmgm  26992  logfaclbnd  27190  logexprlim  27193  logfacrlim2  27194  vmadivsum  27450  dchrisum0lem1a  27454  dchrvmasumlema  27468  dchrisum0lem1  27484  dchrisum0lem2  27486  mudivsum  27498  mulogsumlem  27499  logdivsum  27501  selberg2lem  27518  selberg2  27519  pntrmax  27532  selbergr  27536  pntibndlem1  27557  pntlem3  27577  blocnilem  30790  nmcexi  32012  nmcopexi  32013  nmcfnexi  32037  dp20h  32858  dpexpp1  32887  0dp2dp  32888  sqsscirc1  33944  logdivsqrle  34687  taupilem3  37342  taupilem1  37344  poimirlem29  37678  heicant  37684  itg2addnclem3  37702  itg2gt0cn  37704  ftc1anclem6  37727  ftc1anclem8  37729  areacirclem1  37737  areacirclem4  37740  areacirc  37742  isbnd2  37812  cntotbnd  37825  heiborlem6  37845  heiborlem7  37846  dvrelog3  42083  irrapxlem5  42824  2timesgt  45297  xralrple2  45361  recnnltrp  45384  rpgtrecnn  45387  rrpsscn  45597  stirlinglem14  46096  fourierdlem73  46188  fldivmod  47347  ceildivmod  47348  divge1b  48468  divgt1b  48469  relogbmulbexp  48521  relogbdivb  48522  itschlc0yqe  48720  itschlc0xyqsol1  48726  itsclc0xyqsolr  48729  amgmwlem  49646