Theorem rpcnd 12977

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11025  ℝ⁺crp 12931

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 11084

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 3391  df-ss 3907  df-rp 12932

This theorem is referenced by:  rpcnne0d  12984  ltaddrp2d  13009  prodge0ld  13041  iccf1o  13438  ltexp2r  14124  discr  14191  bcp1nk  14268  bcpasc  14272  01sqrexlem6  15198  sqrtdiv  15216  absdiv  15246  o1rlimmul  15570  isumrpcl  15797  isumltss  15802  expcnv  15818  mertenslem1  15838  bitsmod  16394  nmoi2  24704  reperflem  24793  icopnfcnv  24918  lebnumlem3  24939  nmoleub2lem2  25092  nmoleub3  25095  minveclem3  25405  pjthlem1  25413  ovollb2lem  25464  sca2rab  25488  ovolscalem1  25489  ovolsca  25491  itg2mulc  25723  itg2cnlem2  25738  c1liplem1  25973  lhop1  25991  aalioulem4  26314  aaliou2b  26320  aaliou3lem2  26322  aaliou3lem3  26323  aaliou3lem8  26324  aaliou3lem6  26327  aaliou3lem7  26328  itgulm  26388  dvradcnv  26401  pserdvlem2  26409  abelthlem7  26419  abelthlem8  26420  lognegb  26570  logno1  26616  advlog  26634  advlogexp  26635  cxprec  26666  divcxp  26667  cxpsqrt  26683  dvcxp1  26720  cxpcn3lem  26728  loglesqrt  26742  relogbval  26753  nnlogbexp  26762  logbrec  26763  asinlem3  26852  cxplim  26953  rlimcxp  26955  cxp2limlem  26957  cxp2lim  26958  cxploglim  26959  cxploglim2  26960  divsqrtsumlem  26961  divsqrtsumo1  26965  amgmlem  26971  zetacvg  26996  lgamucov  27019  basellem3  27064  basellem4  27065  chpval2  27200  logexprlim  27207  bclbnd  27262  bposlem9  27274  chebbnd1lem3  27453  chebbnd1  27454  chtppilimlem2  27456  chtppilim  27457  chebbnd2  27459  chto1lb  27460  chpchtlim  27461  chpo1ubb  27463  rplogsumlem1  27466  rplogsumlem2  27467  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrisum0lema  27496  dchrisum0lem1b  27497  dchrisum0lem1  27498  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrisum0lem3  27501  dchrisum0  27502  mulogsumlem  27513  mulog2sumlem1  27516  mulog2sumlem2  27517  vmalogdivsum2  27520  log2sumbnd  27526  selberg3lem1  27539  selberg3lem2  27540  selberg4lem1  27542  selberg4  27543  selberg34r  27553  pntrlog2bndlem2  27560  pntrlog2bndlem3  27561  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  pntpbnd1a  27567  pntpbnd2  27569  pntibndlem1  27571  pntibndlem2  27573  pntlemd  27576  pntlemc  27577  pntlemb  27579  pntlemq  27583  pntlemr  27584  pntlemj  27585  pntlemf  27587  pntlemo  27589  pntlem3  27591  pntleml  27593  pnt  27596  padicabvcxp  27614  ostth2lem4  27618  ostth2  27619  ostth3  27620  smcnlem  30788  blocnilem  30895  ubthlem2  30962  bcm1n  32888  probmeasb  34595  signsply0  34716  iprodgam  35945  faclimlem1  35946  faclimlem3  35948  faclim  35949  iprodfac  35950  knoppndvlem17  36801  mblfinlem3  37991  itg2addnclem3  38005  ftc1cnnclem  38023  geomcau  38091  cntotbnd  38128  heibor1lem  38141  rrndstprj2  38163  rrncmslem  38164  relogbzexpd  42426  lcmineqlem21  42499  aks4d1p1p1  42513  aks4d1p6  42531  2ap1caineq  42595  exp11d  42769  rplog11d  42790  pell1qrgaplem  43316  pellfund14  43341  rmxyneg  43363  rmxy1  43365  rmxy0  43366  jm2.23  43439  proot1ex  43639  amgm2d  44640  amgm3d  44641  amgm4d  44642  cvgdvgrat  44755  binomcxplemnn0  44791  binomcxplemnotnn0  44798  ltdivgt1  45801  xralrple4  45817  xralrple3  45818  0ellimcdiv  46092  limclner  46094  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  dvdivbd  46366  stoweidlem1  46444  stoweidlem3  46446  stoweidlem7  46450  stoweidlem11  46454  stoweidlem14  46457  stoweidlem24  46467  stoweidlem25  46468  stoweidlem26  46469  stoweidlem42  46485  stoweidlem51  46494  stoweidlem59  46502  stoweidlem62  46505  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  stirlinglem4  46520  stirlinglem8  46524  stirlinglem12  46528  stirlinglem15  46531  dirkercncflem4  46549  fourierdlem30  46580  fourierdlem73  46622  fourierdlem87  46636  qndenserrnbllem  46737  hoiqssbllem2  47066  dignn0flhalflem2  49089  itsclc0yqsol  49237  amgmwlem  50274  amgmlemALT  50275  amgmw2d  50276  young2d  50277