Theorem rpcn 12898

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11001  ℝ⁺crp 12887

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 2113  ax-9 2121  ax-ext 2703  ax-resscn 11060

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919  df-rp 12888

This theorem is referenced by:  rpcnne0  12906  rpmtmip  12913  divge1  12957  ltdifltdiv  13735  modvalr  13773  flpmodeq  13775  mulmod0  13778  negmod0  13779  modlt  13781  moddiffl  13783  modvalp1  13791  modid  13797  modid0  13798  modcyc  13807  modcyc2  13808  modadd1  13809  muladdmodid  13814  modmuladdnn0  13819  negmod  13820  modm1p1mod0  13826  modmul1  13828  2txmodxeq0  13835  2submod  13836  moddi  13843  01sqrexlem2  15147  sqrtdiv  15169  caurcvgr  15578  o1fsum  15717  divrcnv  15756  efgt1p2  16020  efgt1p  16021  rpmsubg  21366  uniioombl  25515  abelthlem8  26374  pilem1  26386  logne0  26513  logneg  26522  advlogexp  26589  logcxp  26603  cxprec  26620  cxpmul  26622  abscxp  26626  logsqrt  26638  dvcxp1  26674  dvcxp2  26675  dvsqrt  26676  cxpcn2  26681  loglesqrt  26696  relogbreexp  26710  relogbzexp  26711  relogbmul  26712  relogbdiv  26714  relogbexp  26715  relogbcxp  26720  relogbcxpb  26722  relogbf  26726  logbgt0b  26728  rlimcnp  26900  efrlim  26904  efrlimOLD  26905  cxplim  26907  sqrtlim  26908  cxploglim  26913  logdifbnd  26929  harmonicbnd4  26946  rpdmgm  26960  logfaclbnd  27158  logexprlim  27161  logfacrlim2  27162  vmadivsum  27418  dchrisum0lem1a  27422  dchrvmasumlema  27436  dchrisum0lem1  27452  dchrisum0lem2  27454  mudivsum  27466  mulogsumlem  27467  logdivsum  27469  selberg2lem  27486  selberg2  27487  pntrmax  27500  selbergr  27504  pntibndlem1  27525  pntlem3  27545  blocnilem  30779  nmcexi  32001  nmcopexi  32002  nmcfnexi  32026  dp20h  32854  dpexpp1  32883  0dp2dp  32884  sqsscirc1  33916  logdivsqrle  34658  taupilem3  37352  taupilem1  37354  poimirlem29  37688  heicant  37694  itg2addnclem3  37712  itg2gt0cn  37714  ftc1anclem6  37737  ftc1anclem8  37739  areacirclem1  37747  areacirclem4  37750  areacirc  37752  isbnd2  37822  cntotbnd  37835  heiborlem6  37855  heiborlem7  37856  dvrelog3  42097  irrapxlem5  42858  2timesgt  45328  xralrple2  45392  recnnltrp  45414  rpgtrecnn  45417  rrpsscn  45627  stirlinglem14  46124  fourierdlem73  46216  fldivmod  47368  ceildivmod  47369  divge1b  48543  divgt1b  48544  relogbmulbexp  48592  relogbdivb  48593  itschlc0yqe  48791  itschlc0xyqsol1  48797  itsclc0xyqsolr  48800  amgmwlem  49833