Theorem rpcnd 12963

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-rp 12918

This theorem is referenced by:  rpcnne0d  12970  ltaddrp2d  12995  prodge0ld  13027  iccf1o  13424  ltexp2r  14108  discr  14175  bcp1nk  14252  bcpasc  14256  01sqrexlem6  15182  sqrtdiv  15200  absdiv  15230  o1rlimmul  15554  isumrpcl  15778  isumltss  15783  expcnv  15799  mertenslem1  15819  bitsmod  16375  nmoi2  24686  reperflem  24775  icchmeoOLD  24907  icopnfcnv  24908  lebnumlem3  24930  nmoleub2lem2  25084  nmoleub3  25087  minveclem3  25397  pjthlem1  25405  ovollb2lem  25457  sca2rab  25481  ovolscalem1  25482  ovolsca  25484  itg2mulc  25716  itg2cnlem2  25731  c1liplem1  25969  lhop1  25987  aalioulem4  26311  aaliou2b  26317  aaliou3lem2  26319  aaliou3lem3  26320  aaliou3lem8  26321  aaliou3lem6  26324  aaliou3lem7  26325  itgulm  26385  dvradcnv  26398  pserdvlem2  26406  abelthlem7  26416  abelthlem8  26417  lognegb  26567  logno1  26613  advlog  26631  advlogexp  26632  cxprec  26663  divcxp  26664  cxpsqrt  26680  dvcxp1  26717  cxpcn3lem  26725  loglesqrt  26739  relogbval  26750  nnlogbexp  26759  logbrec  26760  asinlem3  26849  cxplim  26950  rlimcxp  26952  cxp2limlem  26954  cxp2lim  26955  cxploglim  26956  cxploglim2  26957  divsqrtsumlem  26958  divsqrtsumo1  26962  amgmlem  26968  zetacvg  26993  lgamucov  27016  basellem3  27061  basellem4  27062  chpval2  27197  logexprlim  27204  bclbnd  27259  bposlem9  27271  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem2  27453  chtppilim  27454  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ubb  27460  rplogsumlem1  27463  rplogsumlem2  27464  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrisum0  27499  mulogsumlem  27510  mulog2sumlem1  27513  mulog2sumlem2  27514  vmalogdivsum2  27517  log2sumbnd  27523  selberg3lem1  27536  selberg3lem2  27537  selberg4lem1  27539  selberg4  27540  selberg34r  27550  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem1  27568  pntibndlem2  27570  pntlemd  27573  pntlemc  27574  pntlemb  27576  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemo  27586  pntlem3  27588  pntleml  27590  pnt  27593  padicabvcxp  27611  ostth2lem4  27615  ostth2  27616  ostth3  27617  smcnlem  30784  blocnilem  30891  ubthlem2  30958  bcm1n  32885  probmeasb  34607  signsply0  34728  iprodgam  35955  faclimlem1  35956  faclimlem3  35958  faclim  35959  iprodfac  35960  knoppndvlem17  36747  mblfinlem3  37899  itg2addnclem3  37913  ftc1cnnclem  37931  geomcau  37999  cntotbnd  38036  heibor1lem  38049  rrndstprj2  38071  rrncmslem  38072  relogbzexpd  42334  lcmineqlem21  42408  aks4d1p1p1  42422  aks4d1p6  42440  2ap1caineq  42504  exp11d  42685  rplog11d  42706  pell1qrgaplem  43219  pellfund14  43244  rmxyneg  43266  rmxy1  43268  rmxy0  43269  jm2.23  43342  proot1ex  43542  amgm2d  44543  amgm3d  44544  amgm4d  44545  cvgdvgrat  44658  binomcxplemnn0  44694  binomcxplemnotnn0  44701  ltdivgt1  45704  xralrple4  45720  xralrple3  45721  0ellimcdiv  45996  limclner  45998  fprodsubrecnncnvlem  46254  fprodaddrecnncnvlem  46256  dvdivbd  46270  stoweidlem1  46348  stoweidlem3  46350  stoweidlem7  46354  stoweidlem11  46358  stoweidlem14  46361  stoweidlem24  46371  stoweidlem25  46372  stoweidlem26  46373  stoweidlem42  46389  stoweidlem51  46398  stoweidlem59  46406  stoweidlem62  46409  wallispilem4  46415  wallispilem5  46416  wallispi  46417  wallispi2lem1  46418  stirlinglem4  46424  stirlinglem8  46428  stirlinglem12  46432  stirlinglem15  46435  dirkercncflem4  46453  fourierdlem30  46484  fourierdlem73  46526  fourierdlem87  46540  qndenserrnbllem  46641  hoiqssbllem2  46970  dignn0flhalflem2  48965  itsclc0yqsol  49113  amgmwlem  50150  amgmlemALT  50151  amgmw2d  50152  young2d  50153