Theorem rpcnd 13018

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-rp 12975

This theorem is referenced by:  rpcnne0d  13025  ltaddrp2d  13050  prodge0ld  13082  iccf1o  13473  ltexp2r  14138  discr  14203  bcp1nk  14277  bcpasc  14281  01sqrexlem6  15194  sqrtdiv  15212  absdiv  15242  o1rlimmul  15563  isumrpcl  15789  isumltss  15794  expcnv  15810  mertenslem1  15830  bitsmod  16377  nmoi2  24247  reperflem  24334  icchmeo  24457  icopnfcnv  24458  lebnumlem3  24479  nmoleub2lem2  24632  nmoleub3  24635  minveclem3  24946  pjthlem1  24954  ovollb2lem  25005  sca2rab  25029  ovolscalem1  25030  ovolsca  25032  itg2mulc  25265  itg2cnlem2  25280  c1liplem1  25513  lhop1  25531  aalioulem4  25848  aaliou2b  25854  aaliou3lem2  25856  aaliou3lem3  25857  aaliou3lem8  25858  aaliou3lem6  25861  aaliou3lem7  25862  itgulm  25920  dvradcnv  25933  pserdvlem2  25940  abelthlem7  25950  abelthlem8  25951  lognegb  26098  logno1  26144  advlog  26162  advlogexp  26163  cxprec  26194  divcxp  26195  cxpsqrt  26211  dvcxp1  26248  cxpcn3lem  26255  loglesqrt  26266  relogbval  26277  nnlogbexp  26286  logbrec  26287  asinlem3  26376  cxplim  26476  rlimcxp  26478  cxp2limlem  26480  cxp2lim  26481  cxploglim  26482  cxploglim2  26483  divsqrtsumlem  26484  divsqrtsumo1  26488  amgmlem  26494  zetacvg  26519  lgamucov  26542  basellem3  26587  basellem4  26588  chpval2  26721  logexprlim  26728  bclbnd  26783  bposlem9  26795  chebbnd1lem3  26974  chebbnd1  26975  chtppilimlem2  26977  chtppilim  26978  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ubb  26984  rplogsumlem1  26987  rplogsumlem2  26988  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  dchrisum0  27023  mulogsumlem  27034  mulog2sumlem1  27037  mulog2sumlem2  27038  vmalogdivsum2  27041  log2sumbnd  27047  selberg3lem1  27060  selberg3lem2  27061  selberg4lem1  27063  selberg4  27064  selberg34r  27074  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem1  27092  pntibndlem2  27094  pntlemd  27097  pntlemc  27098  pntlemb  27100  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemf  27108  pntlemo  27110  pntlem3  27112  pntleml  27114  pnt  27117  padicabvcxp  27135  ostth2lem4  27139  ostth2  27140  ostth3  27141  smcnlem  29950  blocnilem  30057  ubthlem2  30124  bcm1n  32006  probmeasb  33429  signsply0  33562  iprodgam  34712  faclimlem1  34713  faclimlem3  34715  faclim  34716  iprodfac  34717  gg-icchmeo  35170  knoppndvlem17  35404  mblfinlem3  36527  itg2addnclem3  36541  ftc1cnnclem  36559  geomcau  36627  cntotbnd  36664  heibor1lem  36677  rrndstprj2  36699  rrncmslem  36700  relogbzexpd  40840  lcmineqlem21  40914  aks4d1p1p1  40928  aks4d1p6  40946  2ap1caineq  40961  exp11d  41216  pell1qrgaplem  41611  pellfund14  41636  rmxyneg  41659  rmxy1  41661  rmxy0  41662  jm2.23  41735  proot1ex  41943  amgm2d  42950  amgm3d  42951  amgm4d  42952  cvgdvgrat  43072  binomcxplemnn0  43108  binomcxplemnotnn0  43115  ltdivgt1  44066  xralrple4  44083  xralrple3  44084  0ellimcdiv  44365  limclner  44367  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  dvdivbd  44639  stoweidlem1  44717  stoweidlem3  44719  stoweidlem7  44723  stoweidlem11  44727  stoweidlem14  44730  stoweidlem24  44740  stoweidlem25  44741  stoweidlem26  44742  stoweidlem42  44758  stoweidlem51  44767  stoweidlem59  44775  stoweidlem62  44778  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  stirlinglem4  44793  stirlinglem8  44797  stirlinglem12  44801  stirlinglem15  44804  dirkercncflem4  44822  fourierdlem30  44853  fourierdlem73  44895  fourierdlem87  44909  qndenserrnbllem  45010  hoiqssbllem2  45339  dignn0flhalflem2  47302  itsclc0yqsol  47450  amgmwlem  47849  amgmlemALT  47850  amgmw2d  47851  young2d  47852