Theorem rpcn 13112

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11179  ℝ⁺crp 13101

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-rp 13102

This theorem is used by:  rpcnne0  13120  rpmtmip  13127  divge1  13171  ltdifltdiv  13954  modvalr  13992  flpmodeq  13994  mulmod0  13997  negmod0  13998  modlt  14000  moddiffl  14002  modvalp1  14010  modid  14016  modid0  14017  modcyc  14026  modcyc2  14027  modadd1  14028  muladdmodid  14033  modmuladdnn0  14038  negmod  14039  modm1p1mod0  14045  modmul1  14047  2txmodxeq0  14054  2submod  14055  moddi  14062  01sqrexlem2  15390  sqrtdiv  15412  caurcvgr  15821  o1fsum  15960  divrcnv  16001  efgt1p2  16262  efgt1p  16263  rpmsubg  21717  uniioombl  25890  abelthlem8  26748  pilem1  26760  logne0  26889  logneg  26898  advlogexp  26965  logcxp  26979  cxprec  26996  cxpmul  26998  abscxp  27002  logsqrt  27014  dvcxp1  27050  dvcxp2  27051  dvsqrt  27052  cxpcn2  27056  loglesqrt  27071  relogbreexp  27085  relogbzexp  27086  relogbmul  27087  relogbdiv  27089  relogbexp  27090  relogbcxp  27095  relogbcxpb  27097  relogbf  27101  logbgt0b  27103  rlimcnp  27275  efrlim  27279  cxplim  27281  sqrtlim  27282  cxploglim  27287  logdifbnd  27303  harmonicbnd4  27320  rpdmgm  27334  logfaclbnd  27531  logexprlim  27534  logfacrlim2  27535  vmadivsum  27791  dchrisum0lem1a  27795  dchrvmasumlema  27809  dchrisum0lem1  27825  dchrisum0lem2  27827  mudivsum  27839  mulogsumlem  27840  logdivsum  27842  selberg2lem  27859  selberg2  27860  pntrmax  27873  selbergr  27877  pntibndlem1  27898  pntlem3  27918  blocnilem  31388  nmcexi  32610  nmcopexi  32611  nmcfnexi  32635  dp20h  33427  dpexpp1  33456  0dp2dp  33457  sqsscirc1  34522  logdivsqrle  35262  taupilem3  38208  taupilem1  38210  poimirlem29  38535  heicant  38541  itg2addnclem3  38559  itg2gt0cn  38561  ftc1anclem6  38584  ftc1anclem8  38586  areacirclem1  38594  areacirclem4  38597  areacirc  38599  isbnd2  38685  cntotbnd  38698  heiborlem6  38718  heiborlem7  38719  dvrelog3  43083  irrapxlem5  43786  2timesgt  46247  xralrple2  46310  recnnltrp  46332  rpgtrecnn  46335  rrpsscn  46544  stirlinglem14  47041  fourierdlem73  47133  fldivmod  48358  ceildivmod  48359  divge1b  49568  divgt1b  49569  relogbmulbexp  49617  relogbdivb  49618  itschlc0yqe  49816  itschlc0xyqsol1  49822  itsclc0xyqsolr  49825  amgmwlem  50931