Theorem rpcn 12768

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

Syntax hints:   → wi 4   ∈ wcel 2101  ℂcc 10897  ℝ⁺crp 12758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704  ax-resscn 10956

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3224  df-v 3436  df-in 3896  df-ss 3906  df-rp 12759

This theorem is referenced by:  rpcnne0  12776  rpmtmip  12782  divge1  12826  ltdifltdiv  13582  modvalr  13620  flpmodeq  13622  mulmod0  13625  negmod0  13626  modlt  13628  moddiffl  13630  modvalp1  13638  modid  13644  modid0  13645  modcyc  13654  modcyc2  13655  modadd1  13656  muladdmodid  13659  modmuladdnn0  13663  negmod  13664  modm1p1mod0  13670  modmul1  13672  2txmodxeq0  13679  2submod  13680  moddi  13687  sqrlem2  14983  sqrtdiv  15005  caurcvgr  15413  o1fsum  15553  divrcnv  15592  efgt1p2  15851  efgt1p  15852  rpmsubg  20690  uniioombl  24781  abelthlem8  25626  pilem1  25638  logne0  25763  logneg  25771  advlogexp  25838  logcxp  25852  cxprec  25869  cxpmul  25871  abscxp  25875  logsqrt  25887  dvcxp1  25921  dvcxp2  25922  dvsqrt  25923  cxpcn2  25927  loglesqrt  25939  relogbreexp  25953  relogbzexp  25954  relogbmul  25955  relogbdiv  25957  relogbexp  25958  relogbcxp  25963  relogbcxpb  25965  relogbf  25969  logbgt0b  25971  rlimcnp  26143  efrlim  26147  cxplim  26149  sqrtlim  26150  cxploglim  26155  logdifbnd  26171  harmonicbnd4  26188  rpdmgm  26202  logfaclbnd  26398  logexprlim  26401  logfacrlim2  26402  vmadivsum  26658  dchrisum0lem1a  26662  dchrvmasumlema  26676  dchrisum0lem1  26692  dchrisum0lem2  26694  mudivsum  26706  mulogsumlem  26707  logdivsum  26709  selberg2lem  26726  selberg2  26727  pntrmax  26740  selbergr  26744  pntibndlem1  26765  pntlem3  26785  blocnilem  29194  nmcexi  30416  nmcopexi  30417  nmcfnexi  30441  dp20h  31181  dpexpp1  31210  0dp2dp  31211  sqsscirc1  31886  logdivsqrle  32658  taupilem3  35518  taupilem1  35520  poimirlem29  35834  heicant  35840  itg2addnclem3  35858  itg2gt0cn  35860  ftc1anclem6  35883  ftc1anclem8  35885  areacirclem1  35893  areacirclem4  35896  areacirc  35898  isbnd2  35969  cntotbnd  35982  heiborlem6  36002  heiborlem7  36003  dvrelog3  40099  irrapxlem5  40671  2timesgt  42861  xralrple2  42927  recnnltrp  42950  rpgtrecnn  42953  rrpsscn  43164  stirlinglem14  43663  fourierdlem73  43755  divge1b  45893  divgt1b  45894  fldivmod  45904  relogbmulbexp  45947  relogbdivb  45948  itschlc0yqe  46146  itschlc0xyqsol1  46152  itsclc0xyqsolr  46155  amgmwlem  46546