Theorem rpcn 12561

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℂcc 10692  ℝ⁺crp 12551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-resscn 10751

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-rp 12552

This theorem is referenced by:  rpcnne0  12569  rpmtmip  12575  divge1  12619  ltdifltdiv  13374  modvalr  13410  flpmodeq  13412  mulmod0  13415  negmod0  13416  modlt  13418  moddiffl  13420  modvalp1  13428  modid  13434  modid0  13435  modcyc  13444  modcyc2  13445  modadd1  13446  muladdmodid  13449  modmuladdnn0  13453  negmod  13454  modm1p1mod0  13460  modmul1  13462  2txmodxeq0  13469  2submod  13470  moddi  13477  sqrlem2  14772  sqrtdiv  14794  caurcvgr  15202  o1fsum  15340  divrcnv  15379  efgt1p2  15638  efgt1p  15639  rpmsubg  20381  uniioombl  24440  abelthlem8  25285  pilem1  25297  logne0  25422  logneg  25430  advlogexp  25497  logcxp  25511  cxprec  25528  cxpmul  25530  abscxp  25534  logsqrt  25546  dvcxp1  25580  dvcxp2  25581  dvsqrt  25582  cxpcn2  25586  loglesqrt  25598  relogbreexp  25612  relogbzexp  25613  relogbmul  25614  relogbdiv  25616  relogbexp  25617  relogbcxp  25622  relogbcxpb  25624  relogbf  25628  logbgt0b  25630  rlimcnp  25802  efrlim  25806  cxplim  25808  sqrtlim  25809  cxploglim  25814  logdifbnd  25830  harmonicbnd4  25847  rpdmgm  25861  logfaclbnd  26057  logexprlim  26060  logfacrlim2  26061  vmadivsum  26317  dchrisum0lem1a  26321  dchrvmasumlema  26335  dchrisum0lem1  26351  dchrisum0lem2  26353  mudivsum  26365  mulogsumlem  26366  logdivsum  26368  selberg2lem  26385  selberg2  26386  pntrmax  26399  selbergr  26403  pntibndlem1  26424  pntlem3  26444  blocnilem  28839  nmcexi  30061  nmcopexi  30062  nmcfnexi  30086  dp20h  30827  dpexpp1  30856  0dp2dp  30857  sqsscirc1  31526  logdivsqrle  32296  taupilem3  35173  taupilem1  35175  poimirlem29  35492  heicant  35498  itg2addnclem3  35516  itg2gt0cn  35518  ftc1anclem6  35541  ftc1anclem8  35543  areacirclem1  35551  areacirclem4  35554  areacirc  35556  isbnd2  35627  cntotbnd  35640  heiborlem6  35660  heiborlem7  35661  dvrelog3  39755  irrapxlem5  40292  2timesgt  42440  xralrple2  42507  recnnltrp  42530  rpgtrecnn  42533  rrpsscn  42747  stirlinglem14  43246  fourierdlem73  43338  divge1b  45469  divgt1b  45470  fldivmod  45480  relogbmulbexp  45523  relogbdivb  45524  itschlc0yqe  45722  itschlc0xyqsol1  45728  itsclc0xyqsolr  45731  amgmwlem  46120