Theorem rpcn 13158

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11225  ℝ⁺crp 13147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-rp 13148

This theorem is used by:  rpcnne0  13166  rpmtmip  13173  divge1  13217  ltdifltdiv  14001  modvalr  14039  flpmodeq  14041  mulmod0  14044  negmod0  14045  modlt  14047  moddiffl  14049  modvalp1  14057  modid  14063  modid0  14064  modcyc  14073  modcyc2  14074  modadd1  14075  muladdmodid  14080  modmuladdnn0  14085  negmod  14086  modm1p1mod0  14092  modmul1  14094  2txmodxeq0  14101  2submod  14102  moddi  14109  01sqrexlem2  15439  sqrtdiv  15461  caurcvgr  15870  o1fsum  16009  divrcnv  16050  efgt1p2  16311  efgt1p  16312  rpmsubg  21767  uniioombl  25940  abelthlem8  26796  pilem1  26808  logne0  26937  logneg  26946  advlogexp  27013  logcxp  27027  cxprec  27044  cxpmul  27046  abscxp  27050  logsqrt  27062  dvcxp1  27098  dvcxp2  27099  dvsqrt  27100  cxpcn2  27104  loglesqrt  27119  relogbreexp  27133  relogbzexp  27134  relogbmul  27135  relogbdiv  27137  relogbexp  27138  relogbcxp  27143  relogbcxpb  27145  relogbf  27149  logbgt0b  27151  rlimcnp  27323  efrlim  27327  cxplim  27329  sqrtlim  27330  cxploglim  27335  logdifbnd  27351  harmonicbnd4  27368  rpdmgm  27382  logfaclbnd  27579  logexprlim  27582  logfacrlim2  27583  vmadivsum  27839  dchrisum0lem1a  27843  dchrvmasumlema  27857  dchrisum0lem1  27873  dchrisum0lem2  27875  mudivsum  27887  mulogsumlem  27888  logdivsum  27890  selberg2lem  27907  selberg2  27908  pntrmax  27921  selbergr  27925  pntibndlem1  27946  pntlem3  27966  blocnilem  31436  nmcexi  32658  nmcopexi  32659  nmcfnexi  32683  dp20h  33515  dpexpp1  33544  0dp2dp  33545  sqsscirc1  34610  logdivsqrle  35349  taupilem3  38432  taupilem1  38434  poimirlem29  38759  heicant  38765  itg2addnclem3  38783  itg2gt0cn  38785  ftc1anclem6  38808  ftc1anclem8  38810  areacirclem1  38818  areacirclem4  38821  areacirc  38823  isbnd2  38909  cntotbnd  38922  heiborlem6  38942  heiborlem7  38943  dvrelog3  43307  irrapxlem5  44026  2timesgt  46509  xralrple2  46571  recnnltrp  46593  rpgtrecnn  46596  rrpsscn  46805  stirlinglem14  47302  fourierdlem73  47394  fldivmod  48619  ceildivmod  48620  divge1b  49829  divgt1b  49830  relogbmulbexp  49878  relogbdivb  49879  itschlc0yqe  50077  itschlc0xyqsol1  50083  itsclc0xyqsolr  50086  amgmwlem  51267