Theorem rpcnd 13079

Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem rpcnd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 13077	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11289	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℝ⁺crp 13034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-rp 13035

This theorem is referenced by:  rpcnne0d  13086  ltaddrp2d  13111  prodge0ld  13143  iccf1o  13536  ltexp2r  14213  discr  14279  bcp1nk  14356  bcpasc  14360  01sqrexlem6  15286  sqrtdiv  15304  absdiv  15334  o1rlimmul  15655  isumrpcl  15879  isumltss  15884  expcnv  15900  mertenslem1  15920  bitsmod  16473  nmoi2  24751  reperflem  24840  icchmeoOLD  24972  icopnfcnv  24973  lebnumlem3  24995  nmoleub2lem2  25149  nmoleub3  25152  minveclem3  25463  pjthlem1  25471  ovollb2lem  25523  sca2rab  25547  ovolscalem1  25548  ovolsca  25550  itg2mulc  25782  itg2cnlem2  25797  c1liplem1  26035  lhop1  26053  aalioulem4  26377  aaliou2b  26383  aaliou3lem2  26385  aaliou3lem3  26386  aaliou3lem8  26387  aaliou3lem6  26390  aaliou3lem7  26391  itgulm  26451  dvradcnv  26464  pserdvlem2  26472  abelthlem7  26482  abelthlem8  26483  lognegb  26632  logno1  26678  advlog  26696  advlogexp  26697  cxprec  26728  divcxp  26729  cxpsqrt  26745  dvcxp1  26782  cxpcn3lem  26790  loglesqrt  26804  relogbval  26815  nnlogbexp  26824  logbrec  26825  asinlem3  26914  cxplim  27015  rlimcxp  27017  cxp2limlem  27019  cxp2lim  27020  cxploglim  27021  cxploglim2  27022  divsqrtsumlem  27023  divsqrtsumo1  27027  amgmlem  27033  zetacvg  27058  lgamucov  27081  basellem3  27126  basellem4  27127  chpval2  27262  logexprlim  27269  bclbnd  27324  bposlem9  27336  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem2  27518  chtppilim  27519  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ubb  27525  rplogsumlem1  27528  rplogsumlem2  27529  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrisum0  27564  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  vmalogdivsum2  27582  log2sumbnd  27588  selberg3lem1  27601  selberg3lem2  27602  selberg4lem1  27604  selberg4  27605  selberg34r  27615  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem1  27633  pntibndlem2  27635  pntlemd  27638  pntlemc  27639  pntlemb  27641  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemo  27651  pntlem3  27653  pntleml  27655  pnt  27658  padicabvcxp  27676  ostth2lem4  27680  ostth2  27681  ostth3  27682  smcnlem  30716  blocnilem  30823  ubthlem2  30890  bcm1n  32797  probmeasb  34432  signsply0  34566  iprodgam  35742  faclimlem1  35743  faclimlem3  35745  faclim  35746  iprodfac  35747  knoppndvlem17  36529  mblfinlem3  37666  itg2addnclem3  37680  ftc1cnnclem  37698  geomcau  37766  cntotbnd  37803  heibor1lem  37816  rrndstprj2  37838  rrncmslem  37839  relogbzexpd  41976  lcmineqlem21  42050  aks4d1p1p1  42064  aks4d1p6  42082  2ap1caineq  42146  exp11d  42361  rplog11d  42383  pell1qrgaplem  42884  pellfund14  42909  rmxyneg  42932  rmxy1  42934  rmxy0  42935  jm2.23  43008  proot1ex  43208  amgm2d  44211  amgm3d  44212  amgm4d  44213  cvgdvgrat  44332  binomcxplemnn0  44368  binomcxplemnotnn0  44375  ltdivgt1  45367  xralrple4  45384  xralrple3  45385  0ellimcdiv  45664  limclner  45666  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  dvdivbd  45938  stoweidlem1  46016  stoweidlem3  46018  stoweidlem7  46022  stoweidlem11  46026  stoweidlem14  46029  stoweidlem24  46039  stoweidlem25  46040  stoweidlem26  46041  stoweidlem42  46057  stoweidlem51  46066  stoweidlem59  46074  stoweidlem62  46077  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  stirlinglem4  46092  stirlinglem8  46096  stirlinglem12  46100  stirlinglem15  46103  dirkercncflem4  46121  fourierdlem30  46152  fourierdlem73  46194  fourierdlem87  46208  qndenserrnbllem  46309  hoiqssbllem2  46638  dignn0flhalflem2  48537  itsclc0yqsol  48685  amgmwlem  49321  amgmlemALT  49322  amgmw2d  49323  young2d  49324