Theorem rpcn 11841

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  ℝ⁺crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-rp 11833

This theorem is referenced by:  rpcnne0  11850  divge1  11898  ltdifltdiv  12635  modvalr  12671  flpmodeq  12673  mulmod0  12676  negmod0  12677  modlt  12679  moddiffl  12681  modvalp1  12689  modid  12695  modid0  12696  modcyc  12705  modcyc2  12706  modadd1  12707  muladdmodid  12710  modmuladdnn0  12714  negmod  12715  modm1p1mod0  12721  modmul1  12723  2txmodxeq0  12730  2submod  12731  moddi  12738  sqrlem2  13984  sqrtdiv  14006  caurcvgr  14404  o1fsum  14545  divrcnv  14584  efgt1p2  14844  efgt1p  14845  rpmsubg  19810  uniioombl  23357  abelthlem8  24193  reefgim  24204  pilem1  24205  logne0  24326  logneg  24334  advlogexp  24401  logcxp  24415  cxprec  24432  cxpmul  24434  abscxp  24438  logsqrt  24450  dvcxp1  24481  dvcxp2  24482  dvsqrt  24483  cxpcn2  24487  loglesqrt  24499  relogbreexp  24513  relogbzexp  24514  relogbmul  24515  relogbdiv  24517  relogbexp  24518  relogbcxp  24523  relogbcxpb  24525  relogbf  24529  rlimcnp  24692  efrlim  24696  cxplim  24698  sqrtlim  24699  cxploglim  24704  logdifbnd  24720  harmonicbnd4  24737  rpdmgm  24751  logfaclbnd  24947  logexprlim  24950  logfacrlim2  24951  vmadivsum  25171  dchrisum0lem1a  25175  dchrvmasumlema  25189  dchrisum0lem1  25205  dchrisum0lem2  25207  mudivsum  25219  mulogsumlem  25220  logdivsum  25222  selberg2lem  25239  selberg2  25240  pntrmax  25253  selbergr  25257  pntibndlem1  25278  pntlem3  25298  blocnilem  27659  nmcexi  28885  nmcopexi  28886  nmcfnexi  28910  dp20h  29586  dpexpp1  29616  0dp2dp  29617  sqsscirc1  29954  logdivsqrle  30728  taupilem3  33165  taupilem1  33167  poimirlem29  33438  heicant  33444  itg2addnclem3  33463  itg2gt0cn  33465  ftc1anclem6  33490  ftc1anclem8  33492  areacirclem1  33500  areacirclem4  33503  areacirc  33505  isbnd2  33582  cntotbnd  33595  heiborlem6  33615  heiborlem7  33616  irrapxlem5  37390  2timesgt  39500  xralrple2  39570  recnnltrp  39593  rpgtrecnn  39597  rrpsscn  39820  stirlinglem14  40304  fourierdlem73  40396  divge1b  42302  divgt1b  42303  fldivmod  42313  relogbmulbexp  42355  relogbdivb  42356  amgmwlem  42548