Theorem rpcn 11717

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11709

This theorem is referenced by:  rpcnne0  11726  divge1  11774  ltdifltdiv  12497  modvalr  12533  flpmodeq  12535  mulmod0  12538  negmod0  12539  modlt  12541  moddiffl  12543  modvalp1  12551  modid  12557  modid0  12558  modcyc  12567  modcyc2  12568  modadd1  12569  muladdmodid  12572  modmuladdnn0  12576  negmod  12577  modm1p1mod0  12583  modmul1  12585  2txmodxeq0  12592  2submod  12593  moddi  12600  sqrlem2  13832  sqrtdiv  13854  caurcvgr  14252  o1fsum  14386  divrcnv  14423  efgt1p2  14683  efgt1p  14684  rpmsubg  19629  uniioombl  23163  abelthlem8  23997  reefgim  24008  pilem1  24009  logne0  24130  logneg  24138  advlogexp  24201  logcxp  24215  cxprec  24232  cxpmul  24234  abscxp  24238  logsqrt  24250  dvcxp1  24281  dvcxp2  24282  dvsqrt  24283  cxpcn2  24287  loglesqrt  24299  relogbreexp  24313  relogbzexp  24314  relogbmul  24315  relogbdiv  24317  relogbexp  24318  relogbcxp  24323  relogbcxpb  24325  relogbf  24329  rlimcnp  24492  efrlim  24496  cxplim  24498  sqrtlim  24499  cxploglim  24504  logdifbnd  24520  harmonicbnd4  24537  rpdmgm  24551  logfaclbnd  24747  logexprlim  24750  logfacrlim2  24751  vmadivsum  24971  dchrisum0lem1a  24975  dchrvmasumlema  24989  dchrisum0lem1  25005  dchrisum0lem2  25007  mudivsum  25019  mulogsumlem  25020  logdivsum  25022  selberg2lem  25039  selberg2  25040  pntrmax  25053  selbergr  25057  pntibndlem1  25078  pntlem3  25098  blocnilem  27043  nmcexi  28269  nmcopexi  28270  nmcfnexi  28294  sqsscirc1  29282  taupilem3  32342  taupilem1  32344  poimirlem29  32608  heicant  32614  itg2addnclem3  32633  itg2gt0cn  32635  ftc1anclem6  32660  ftc1anclem8  32662  areacirclem1  32670  areacirclem4  32673  areacirc  32675  isbnd2  32752  cntotbnd  32765  heiborlem6  32785  heiborlem7  32786  irrapxlem5  36408  2timesgt  38441  xralrple2  38511  recnnltrp  38534  rpgtrecnn  38538  rrpsscn  38655  stirlinglem14  38980  fourierdlem73  39072  divge1b  42096  divgt1b  42097  fldivmod  42107  relogbmulbexp  42153  relogbdivb  42154  amgmwlem  42357