Theorem rpcn 12922

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11026  ℝ⁺crp 12911

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 2701  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922  df-rp 12912

This theorem is referenced by:  rpcnne0  12930  rpmtmip  12937  divge1  12981  ltdifltdiv  13756  modvalr  13794  flpmodeq  13796  mulmod0  13799  negmod0  13800  modlt  13802  moddiffl  13804  modvalp1  13812  modid  13818  modid0  13819  modcyc  13828  modcyc2  13829  modadd1  13830  muladdmodid  13835  modmuladdnn0  13840  negmod  13841  modm1p1mod0  13847  modmul1  13849  2txmodxeq0  13856  2submod  13857  moddi  13864  01sqrexlem2  15168  sqrtdiv  15190  caurcvgr  15599  o1fsum  15738  divrcnv  15777  efgt1p2  16041  efgt1p  16042  rpmsubg  21356  uniioombl  25506  abelthlem8  26365  pilem1  26377  logne0  26504  logneg  26513  advlogexp  26580  logcxp  26594  cxprec  26611  cxpmul  26613  abscxp  26617  logsqrt  26629  dvcxp1  26665  dvcxp2  26666  dvsqrt  26667  cxpcn2  26672  loglesqrt  26687  relogbreexp  26701  relogbzexp  26702  relogbmul  26703  relogbdiv  26705  relogbexp  26706  relogbcxp  26711  relogbcxpb  26713  relogbf  26717  logbgt0b  26719  rlimcnp  26891  efrlim  26895  efrlimOLD  26896  cxplim  26898  sqrtlim  26899  cxploglim  26904  logdifbnd  26920  harmonicbnd4  26937  rpdmgm  26951  logfaclbnd  27149  logexprlim  27152  logfacrlim2  27153  vmadivsum  27409  dchrisum0lem1a  27413  dchrvmasumlema  27427  dchrisum0lem1  27443  dchrisum0lem2  27445  mudivsum  27457  mulogsumlem  27458  logdivsum  27460  selberg2lem  27477  selberg2  27478  pntrmax  27491  selbergr  27495  pntibndlem1  27516  pntlem3  27536  blocnilem  30766  nmcexi  31988  nmcopexi  31989  nmcfnexi  32013  dp20h  32832  dpexpp1  32861  0dp2dp  32862  sqsscirc1  33874  logdivsqrle  34617  taupilem3  37292  taupilem1  37294  poimirlem29  37628  heicant  37634  itg2addnclem3  37652  itg2gt0cn  37654  ftc1anclem6  37677  ftc1anclem8  37679  areacirclem1  37687  areacirclem4  37690  areacirc  37692  isbnd2  37762  cntotbnd  37775  heiborlem6  37795  heiborlem7  37796  dvrelog3  42038  irrapxlem5  42799  2timesgt  45270  xralrple2  45334  recnnltrp  45357  rpgtrecnn  45360  rrpsscn  45570  stirlinglem14  46069  fourierdlem73  46161  fldivmod  47323  ceildivmod  47324  divge1b  48498  divgt1b  48499  relogbmulbexp  48547  relogbdivb  48548  itschlc0yqe  48746  itschlc0xyqsol1  48752  itsclc0xyqsolr  48755  amgmwlem  49788