Theorem rpcn 12400

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3943  df-ss 3952  df-rp 12391

This theorem is referenced by:  rpcnne0  12408  rpmtmip  12414  divge1  12458  ltdifltdiv  13205  modvalr  13241  flpmodeq  13243  mulmod0  13246  negmod0  13247  modlt  13249  moddiffl  13251  modvalp1  13259  modid  13265  modid0  13266  modcyc  13275  modcyc2  13276  modadd1  13277  muladdmodid  13280  modmuladdnn0  13284  negmod  13285  modm1p1mod0  13291  modmul1  13293  2txmodxeq0  13300  2submod  13301  moddi  13308  sqrlem2  14603  sqrtdiv  14625  caurcvgr  15030  o1fsum  15168  divrcnv  15207  efgt1p2  15467  efgt1p  15468  rpmsubg  20609  uniioombl  24190  abelthlem8  25027  pilem1  25039  logne0  25163  logneg  25171  advlogexp  25238  logcxp  25252  cxprec  25269  cxpmul  25271  abscxp  25275  logsqrt  25287  dvcxp1  25321  dvcxp2  25322  dvsqrt  25323  cxpcn2  25327  loglesqrt  25339  relogbreexp  25353  relogbzexp  25354  relogbmul  25355  relogbdiv  25357  relogbexp  25358  relogbcxp  25363  relogbcxpb  25365  relogbf  25369  logbgt0b  25371  rlimcnp  25543  efrlim  25547  cxplim  25549  sqrtlim  25550  cxploglim  25555  logdifbnd  25571  harmonicbnd4  25588  rpdmgm  25602  logfaclbnd  25798  logexprlim  25801  logfacrlim2  25802  vmadivsum  26058  dchrisum0lem1a  26062  dchrvmasumlema  26076  dchrisum0lem1  26092  dchrisum0lem2  26094  mudivsum  26106  mulogsumlem  26107  logdivsum  26109  selberg2lem  26126  selberg2  26127  pntrmax  26140  selbergr  26144  pntibndlem1  26165  pntlem3  26185  blocnilem  28581  nmcexi  29803  nmcopexi  29804  nmcfnexi  29828  dp20h  30555  dpexpp1  30584  0dp2dp  30585  sqsscirc1  31151  logdivsqrle  31921  taupilem3  34603  taupilem1  34605  poimirlem29  34936  heicant  34942  itg2addnclem3  34960  itg2gt0cn  34962  ftc1anclem6  34987  ftc1anclem8  34989  areacirclem1  34997  areacirclem4  35000  areacirc  35002  isbnd2  35076  cntotbnd  35089  heiborlem6  35109  heiborlem7  35110  irrapxlem5  39443  2timesgt  41574  xralrple2  41642  recnnltrp  41665  rpgtrecnn  41669  rrpsscn  41889  stirlinglem14  42392  fourierdlem73  42484  divge1b  44587  divgt1b  44588  fldivmod  44598  relogbmulbexp  44641  relogbdivb  44642  itschlc0yqe  44767  itschlc0xyqsol1  44773  itsclc0xyqsolr  44776  amgmwlem  44923