Theorem rpcn 12911

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11014  ℝ⁺crp 12900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-ss 3916  df-rp 12901

This theorem is referenced by:  rpcnne0  12919  rpmtmip  12926  divge1  12970  ltdifltdiv  13748  modvalr  13786  flpmodeq  13788  mulmod0  13791  negmod0  13792  modlt  13794  moddiffl  13796  modvalp1  13804  modid  13810  modid0  13811  modcyc  13820  modcyc2  13821  modadd1  13822  muladdmodid  13827  modmuladdnn0  13832  negmod  13833  modm1p1mod0  13839  modmul1  13841  2txmodxeq0  13848  2submod  13849  moddi  13856  01sqrexlem2  15160  sqrtdiv  15182  caurcvgr  15591  o1fsum  15730  divrcnv  15769  efgt1p2  16033  efgt1p  16034  rpmsubg  21378  uniioombl  25527  abelthlem8  26386  pilem1  26398  logne0  26525  logneg  26534  advlogexp  26601  logcxp  26615  cxprec  26632  cxpmul  26634  abscxp  26638  logsqrt  26650  dvcxp1  26686  dvcxp2  26687  dvsqrt  26688  cxpcn2  26693  loglesqrt  26708  relogbreexp  26722  relogbzexp  26723  relogbmul  26724  relogbdiv  26726  relogbexp  26727  relogbcxp  26732  relogbcxpb  26734  relogbf  26738  logbgt0b  26740  rlimcnp  26912  efrlim  26916  efrlimOLD  26917  cxplim  26919  sqrtlim  26920  cxploglim  26925  logdifbnd  26941  harmonicbnd4  26958  rpdmgm  26972  logfaclbnd  27170  logexprlim  27173  logfacrlim2  27174  vmadivsum  27430  dchrisum0lem1a  27434  dchrvmasumlema  27448  dchrisum0lem1  27464  dchrisum0lem2  27466  mudivsum  27478  mulogsumlem  27479  logdivsum  27481  selberg2lem  27498  selberg2  27499  pntrmax  27512  selbergr  27516  pntibndlem1  27537  pntlem3  27557  blocnilem  30795  nmcexi  32017  nmcopexi  32018  nmcfnexi  32042  dp20h  32870  dpexpp1  32899  0dp2dp  32900  sqsscirc1  33932  logdivsqrle  34674  taupilem3  37374  taupilem1  37376  poimirlem29  37699  heicant  37705  itg2addnclem3  37723  itg2gt0cn  37725  ftc1anclem6  37748  ftc1anclem8  37750  areacirclem1  37758  areacirclem4  37761  areacirc  37763  isbnd2  37833  cntotbnd  37846  heiborlem6  37866  heiborlem7  37867  dvrelog3  42168  irrapxlem5  42933  2timesgt  45403  xralrple2  45467  recnnltrp  45489  rpgtrecnn  45492  rrpsscn  45702  stirlinglem14  46199  fourierdlem73  46291  fldivmod  47452  ceildivmod  47453  divge1b  48627  divgt1b  48628  relogbmulbexp  48676  relogbdivb  48677  itschlc0yqe  48875  itschlc0xyqsol1  48881  itsclc0xyqsolr  48884  amgmwlem  49917