Theorem rpcn 12916

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℝ⁺crp 12905

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 2708  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-rp 12906

This theorem is referenced by:  rpcnne0  12924  rpmtmip  12931  divge1  12975  ltdifltdiv  13754  modvalr  13792  flpmodeq  13794  mulmod0  13797  negmod0  13798  modlt  13800  moddiffl  13802  modvalp1  13810  modid  13816  modid0  13817  modcyc  13826  modcyc2  13827  modadd1  13828  muladdmodid  13833  modmuladdnn0  13838  negmod  13839  modm1p1mod0  13845  modmul1  13847  2txmodxeq0  13854  2submod  13855  moddi  13862  01sqrexlem2  15166  sqrtdiv  15188  caurcvgr  15597  o1fsum  15736  divrcnv  15775  efgt1p2  16039  efgt1p  16040  rpmsubg  21386  uniioombl  25546  abelthlem8  26405  pilem1  26417  logne0  26544  logneg  26553  advlogexp  26620  logcxp  26634  cxprec  26651  cxpmul  26653  abscxp  26657  logsqrt  26669  dvcxp1  26705  dvcxp2  26706  dvsqrt  26707  cxpcn2  26712  loglesqrt  26727  relogbreexp  26741  relogbzexp  26742  relogbmul  26743  relogbdiv  26745  relogbexp  26746  relogbcxp  26751  relogbcxpb  26753  relogbf  26757  logbgt0b  26759  rlimcnp  26931  efrlim  26935  efrlimOLD  26936  cxplim  26938  sqrtlim  26939  cxploglim  26944  logdifbnd  26960  harmonicbnd4  26977  rpdmgm  26991  logfaclbnd  27189  logexprlim  27192  logfacrlim2  27193  vmadivsum  27449  dchrisum0lem1a  27453  dchrvmasumlema  27467  dchrisum0lem1  27483  dchrisum0lem2  27485  mudivsum  27497  mulogsumlem  27498  logdivsum  27500  selberg2lem  27517  selberg2  27518  pntrmax  27531  selbergr  27535  pntibndlem1  27556  pntlem3  27576  blocnilem  30879  nmcexi  32101  nmcopexi  32102  nmcfnexi  32126  dp20h  32960  dpexpp1  32989  0dp2dp  32990  sqsscirc1  34065  logdivsqrle  34807  taupilem3  37520  taupilem1  37522  poimirlem29  37846  heicant  37852  itg2addnclem3  37870  itg2gt0cn  37872  ftc1anclem6  37895  ftc1anclem8  37897  areacirclem1  37905  areacirclem4  37908  areacirc  37910  isbnd2  37980  cntotbnd  37993  heiborlem6  38013  heiborlem7  38014  dvrelog3  42315  irrapxlem5  43064  2timesgt  45532  xralrple2  45595  recnnltrp  45617  rpgtrecnn  45620  rrpsscn  45830  stirlinglem14  46327  fourierdlem73  46419  fldivmod  47580  ceildivmod  47581  divge1b  48754  divgt1b  48755  relogbmulbexp  48803  relogbdivb  48804  itschlc0yqe  49002  itschlc0xyqsol1  49008  itsclc0xyqsolr  49011  amgmwlem  50043