Theorem rpcnd 13090

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 13088	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11264	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

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

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 2734  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-rp 13045

This theorem is used by:  rpcnne0d  13097  ltaddrp2d  13122  prodge0ld  13154  iccf1o  13551  ltexp2r  14239  discr  14306  bcp1nk  14383  bcpasc  14387  01sqrexlem6  15336  sqrtdiv  15354  absdiv  15384  o1rlimmul  15708  isumrpcl  15934  isumltss  15939  expcnv  15955  mertenslem1  15975  bitsmod  16530  nmoi2  24960  reperflem  25049  icopnfcnv  25174  lebnumlem3  25195  nmoleub2lem2  25348  nmoleub3  25351  minveclem3  25661  pjthlem1  25669  ovollb2lem  25720  sca2rab  25744  ovolscalem1  25745  ovolsca  25747  itg2mulc  25979  itg2cnlem2  25994  c1liplem1  26228  lhop1  26246  aalioulem4  26571  aaliou2b  26577  aaliou3lem2  26579  aaliou3lem3  26580  aaliou3lem8  26581  aaliou3lem6  26584  aaliou3lem7  26585  itgulm  26644  dvradcnv  26657  pserdvlem2  26664  abelthlem7  26674  abelthlem8  26675  lognegb  26828  logno1  26874  advlog  26892  advlogexp  26893  cxprec  26924  divcxp  26925  cxpsqrt  26941  dvcxp1  26978  cxpcn3lem  26985  loglesqrt  26999  relogbval  27010  nnlogbexp  27019  logbrec  27020  asinlem3  27109  cxplim  27209  rlimcxp  27211  cxp2limlem  27213  cxp2lim  27214  cxploglim  27215  cxploglim2  27216  divsqrtsumlem  27217  divsqrtsumo1  27221  amgmlem  27227  zetacvg  27252  lgamucov  27275  basellem3  27320  basellem4  27321  basellem8  27325  chpval2  27455  logexprlim  27462  bclbnd  27517  bposlem9  27529  chebbnd1lem3  27708  chebbnd1  27709  chtppilimlem2  27711  chtppilim  27712  chebbnd2  27714  chto1lb  27715  chpchtlim  27716  chpo1ubb  27718  rplogsumlem1  27721  rplogsumlem2  27722  dchrvmasumlem1  27732  dchrvmasum2lem  27733  dchrisum0lema  27751  dchrisum0lem1b  27752  dchrisum0lem1  27753  dchrisum0lem2a  27754  dchrisum0lem2  27755  dchrisum0lem3  27756  dchrisum0  27757  mulogsumlem  27768  mulog2sumlem1  27771  mulog2sumlem2  27772  vmalogdivsum2  27775  log2sumbnd  27781  selberg3lem1  27794  selberg3lem2  27795  selberg4lem1  27797  selberg4  27798  selberg34r  27808  pntrlog2bndlem2  27815  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntpbnd1a  27822  pntpbnd2  27824  pntibndlem1  27826  pntibndlem2  27828  pntlemd  27831  pntlemc  27832  pntlemb  27834  pntlemq  27838  pntlemr  27839  pntlemj  27840  pntlemf  27842  pntlemo  27844  pntlem3  27846  pntleml  27848  pnt  27851  padicabvcxp  27869  ostth2lem4  27873  ostth2  27874  ostth3  27875  smcnlem  31179  blocnilem  31286  ubthlem2  31353  bcm1n  33268  probmeasb  34943  signsply0  35061  iprodgam  36323  faclimlem1  36324  faclimlem3  36326  faclim  36327  iprodfac  36328  knoppndvlem17  37227  mblfinlem3  38410  itg2addnclem3  38424  ftc1cnnclem  38442  geomcau  38511  cntotbnd  38548  heibor1lem  38561  rrndstprj2  38583  rrncmslem  38584  relogbzexpd  42844  lcmineqlem21  42917  aks4d1p1p1  42931  aks4d1p6  42949  2ap1caineq  43013  exp11d  43203  rplog11d  43224  pell1qrgaplem  43716  pellfund14  43741  rmxyneg  43763  rmxy1  43765  rmxy0  43766  jm2.23  43839  proot1ex  44039  amgm2d  45040  amgm3d  45041  amgm4d  45042  cvgdvgrat  45139  binomcxplemnn0  45175  binomcxplemnotnn0  45182  ltdivgt1  46188  xralrple4  46204  xralrple3  46205  0ellimcdiv  46479  limclner  46481  fprodsubrecnncnvlem  46737  fprodaddrecnncnvlem  46739  dvdivbd  46753  stoweidlem1  46831  stoweidlem3  46833  stoweidlem7  46837  stoweidlem11  46841  stoweidlem14  46844  stoweidlem24  46854  stoweidlem25  46855  stoweidlem26  46856  stoweidlem42  46872  stoweidlem51  46881  stoweidlem59  46889  stoweidlem62  46892  wallispilem4  46898  wallispilem5  46899  wallispi  46900  wallispi2lem1  46901  stirlinglem4  46907  stirlinglem8  46911  stirlinglem12  46915  stirlinglem15  46918  dirkercncflem4  46936  fourierdlem30  46967  fourierdlem73  47009  fourierdlem87  47023  qndenserrnbllem  47124  hoiqssbllem2  47453  dignn0flhalflem2  49548  itsclc0yqsol  49696  amgmwlem  50822  amgmlemALT  50823  amgmw2d  50824  young2d  50825