Theorem rpcnd 13167

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11199  ℝ⁺crp 13121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-rp 13122

This theorem is used by:  rpcnne0d  13174  ltaddrp2d  13199  prodge0ld  13231  iccf1o  13628  ltexp2r  14317  discr  14385  bcp1nk  14462  bcpasc  14466  01sqrexlem6  15415  sqrtdiv  15433  absdiv  15463  o1rlimmul  15787  isumrpcl  16013  isumltss  16018  expcnv  16034  mertenslem1  16054  bitsmod  16607  nmoi2  25050  reperflem  25139  icopnfcnv  25264  lebnumlem3  25285  nmoleub2lem2  25438  nmoleub3  25441  minveclem3  25751  pjthlem1  25759  ovollb2lem  25810  sca2rab  25834  ovolscalem1  25835  ovolsca  25837  itg2mulc  26069  itg2cnlem2  26084  c1liplem1  26317  lhop1  26335  aalioulem4  26663  aaliou2b  26669  aaliou3lem2  26671  aaliou3lem3  26672  aaliou3lem8  26673  aaliou3lem6  26676  aaliou3lem7  26677  itgulm  26736  dvradcnv  26749  pserdvlem2  26756  abelthlem7  26766  abelthlem8  26767  lognegb  26919  logno1  26965  advlog  26983  advlogexp  26984  cxprec  27015  divcxp  27016  cxpsqrt  27032  dvcxp1  27069  cxpcn3lem  27076  loglesqrt  27090  relogbval  27101  nnlogbexp  27110  logbrec  27111  asinlem3  27200  cxplim  27300  rlimcxp  27302  cxp2limlem  27304  cxp2lim  27305  cxploglim  27306  cxploglim2  27307  divsqrtsumlem  27308  divsqrtsumo1  27312  amgmlem  27318  zetacvg  27343  lgamucov  27366  basellem3  27411  basellem4  27412  basellem8  27416  chpval2  27546  logexprlim  27553  bclbnd  27608  bposlem9  27620  chebbnd1lem3  27799  chebbnd1  27800  chtppilimlem2  27802  chtppilim  27803  chebbnd2  27805  chto1lb  27806  chpchtlim  27807  chpo1ubb  27809  rplogsumlem1  27812  rplogsumlem2  27813  dchrvmasumlem1  27823  dchrvmasum2lem  27824  dchrisum0lema  27842  dchrisum0lem1b  27843  dchrisum0lem1  27844  dchrisum0lem2a  27845  dchrisum0lem2  27846  dchrisum0lem3  27847  dchrisum0  27848  mulogsumlem  27859  mulog2sumlem1  27862  mulog2sumlem2  27863  vmalogdivsum2  27866  log2sumbnd  27872  selberg3lem1  27885  selberg3lem2  27886  selberg4lem1  27888  selberg4  27889  selberg34r  27899  pntrlog2bndlem2  27906  pntrlog2bndlem3  27907  pntrlog2bndlem4  27908  pntrlog2bndlem5  27909  pntpbnd1a  27913  pntpbnd2  27915  pntibndlem1  27917  pntibndlem2  27919  pntlemd  27922  pntlemc  27923  pntlemb  27925  pntlemq  27929  pntlemr  27930  pntlemj  27931  pntlemf  27933  pntlemo  27935  pntlem3  27937  pntleml  27939  pnt  27942  padicabvcxp  27960  ostth2lem4  27964  ostth2  27965  ostth3  27966  smcnlem  31300  blocnilem  31407  ubthlem2  31474  bcm1n  33430  probmeasb  35105  signsply0  35223  iprodgam  36582  faclimlem1  36583  faclimlem3  36585  faclim  36586  iprodfac  36587  knoppndvlem17  37469  mblfinlem3  38653  itg2addnclem3  38667  ftc1cnnclem  38685  geomcau  38769  cntotbnd  38806  heibor1lem  38819  rrndstprj2  38841  rrncmslem  38842  relogbzexpd  43102  lcmineqlem21  43175  aks4d1p1p1  43189  aks4d1p6  43207  2ap1caineq  43271  exp11d  43459  rplog11d  43474  pell1qrgaplem  43956  pellfund14  43981  rmxyneg  44003  rmxy1  44005  rmxy0  44006  jm2.23  44079  proot1ex  44274  amgm2d  45274  amgm3d  45275  amgm4d  45276  cvgdvgrat  45373  binomcxplemnn0  45409  binomcxplemnotnn0  45416  ltdivgt1  46444  xralrple4  46460  xralrple3  46461  0ellimcdiv  46735  limclner  46737  fprodsubrecnncnvlem  46993  fprodaddrecnncnvlem  46995  dvdivbd  47009  stoweidlem1  47087  stoweidlem3  47089  stoweidlem7  47093  stoweidlem11  47097  stoweidlem14  47100  stoweidlem24  47110  stoweidlem25  47111  stoweidlem26  47112  stoweidlem42  47128  stoweidlem51  47137  stoweidlem59  47145  stoweidlem62  47148  wallispilem4  47154  wallispilem5  47155  wallispi  47156  wallispi2lem1  47157  stirlinglem4  47163  stirlinglem8  47167  stirlinglem12  47171  stirlinglem15  47174  dirkercncflem4  47192  fourierdlem30  47223  fourierdlem73  47265  fourierdlem87  47279  qndenserrnbllem  47380  hoiqssbllem2  47709  dignn0flhalflem2  49804  itsclc0yqsol  49952  amgmwlem  51063  amgmlemALT  51064  amgmw2d  51065  young2d  51066