Theorem rpcnd 12928

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10996  ℝ⁺crp 12882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-resscn 11055

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-ss 3917  df-rp 12883

This theorem is referenced by:  rpcnne0d  12935  ltaddrp2d  12960  prodge0ld  12992  iccf1o  13388  ltexp2r  14072  discr  14139  bcp1nk  14216  bcpasc  14220  01sqrexlem6  15146  sqrtdiv  15164  absdiv  15194  o1rlimmul  15518  isumrpcl  15742  isumltss  15747  expcnv  15763  mertenslem1  15783  bitsmod  16339  nmoi2  24638  reperflem  24727  icchmeoOLD  24859  icopnfcnv  24860  lebnumlem3  24882  nmoleub2lem2  25036  nmoleub3  25039  minveclem3  25349  pjthlem1  25357  ovollb2lem  25409  sca2rab  25433  ovolscalem1  25434  ovolsca  25436  itg2mulc  25668  itg2cnlem2  25683  c1liplem1  25921  lhop1  25939  aalioulem4  26263  aaliou2b  26269  aaliou3lem2  26271  aaliou3lem3  26272  aaliou3lem8  26273  aaliou3lem6  26276  aaliou3lem7  26277  itgulm  26337  dvradcnv  26350  pserdvlem2  26358  abelthlem7  26368  abelthlem8  26369  lognegb  26519  logno1  26565  advlog  26583  advlogexp  26584  cxprec  26615  divcxp  26616  cxpsqrt  26632  dvcxp1  26669  cxpcn3lem  26677  loglesqrt  26691  relogbval  26702  nnlogbexp  26711  logbrec  26712  asinlem3  26801  cxplim  26902  rlimcxp  26904  cxp2limlem  26906  cxp2lim  26907  cxploglim  26908  cxploglim2  26909  divsqrtsumlem  26910  divsqrtsumo1  26914  amgmlem  26920  zetacvg  26945  lgamucov  26968  basellem3  27013  basellem4  27014  chpval2  27149  logexprlim  27156  bclbnd  27211  bposlem9  27223  chebbnd1lem3  27402  chebbnd1  27403  chtppilimlem2  27405  chtppilim  27406  chebbnd2  27408  chto1lb  27409  chpchtlim  27410  chpo1ubb  27412  rplogsumlem1  27415  rplogsumlem2  27416  dchrvmasumlem1  27426  dchrvmasum2lem  27427  dchrisum0lema  27445  dchrisum0lem1b  27446  dchrisum0lem1  27447  dchrisum0lem2a  27448  dchrisum0lem2  27449  dchrisum0lem3  27450  dchrisum0  27451  mulogsumlem  27462  mulog2sumlem1  27465  mulog2sumlem2  27466  vmalogdivsum2  27469  log2sumbnd  27475  selberg3lem1  27488  selberg3lem2  27489  selberg4lem1  27491  selberg4  27492  selberg34r  27502  pntrlog2bndlem2  27509  pntrlog2bndlem3  27510  pntrlog2bndlem4  27511  pntrlog2bndlem5  27512  pntpbnd1a  27516  pntpbnd2  27518  pntibndlem1  27520  pntibndlem2  27522  pntlemd  27525  pntlemc  27526  pntlemb  27528  pntlemq  27532  pntlemr  27533  pntlemj  27534  pntlemf  27536  pntlemo  27538  pntlem3  27540  pntleml  27542  pnt  27545  padicabvcxp  27563  ostth2lem4  27567  ostth2  27568  ostth3  27569  smcnlem  30667  blocnilem  30774  ubthlem2  30841  bcm1n  32767  probmeasb  34433  signsply0  34554  iprodgam  35754  faclimlem1  35755  faclimlem3  35757  faclim  35758  iprodfac  35759  knoppndvlem17  36541  mblfinlem3  37678  itg2addnclem3  37692  ftc1cnnclem  37710  geomcau  37778  cntotbnd  37815  heibor1lem  37828  rrndstprj2  37850  rrncmslem  37851  relogbzexpd  41987  lcmineqlem21  42061  aks4d1p1p1  42075  aks4d1p6  42093  2ap1caineq  42157  exp11d  42338  rplog11d  42359  pell1qrgaplem  42885  pellfund14  42910  rmxyneg  42932  rmxy1  42934  rmxy0  42935  jm2.23  43008  proot1ex  43208  amgm2d  44210  amgm3d  44211  amgm4d  44212  cvgdvgrat  44325  binomcxplemnn0  44361  binomcxplemnotnn0  44368  ltdivgt1  45374  xralrple4  45390  xralrple3  45391  0ellimcdiv  45666  limclner  45668  fprodsubrecnncnvlem  45924  fprodaddrecnncnvlem  45926  dvdivbd  45940  stoweidlem1  46018  stoweidlem3  46020  stoweidlem7  46024  stoweidlem11  46028  stoweidlem14  46031  stoweidlem24  46041  stoweidlem25  46042  stoweidlem26  46043  stoweidlem42  46059  stoweidlem51  46068  stoweidlem59  46076  stoweidlem62  46079  wallispilem4  46085  wallispilem5  46086  wallispi  46087  wallispi2lem1  46088  stirlinglem4  46094  stirlinglem8  46098  stirlinglem12  46102  stirlinglem15  46105  dirkercncflem4  46123  fourierdlem30  46154  fourierdlem73  46196  fourierdlem87  46210  qndenserrnbllem  46311  hoiqssbllem2  46640  dignn0flhalflem2  48627  itsclc0yqsol  48775  amgmwlem  49813  amgmlemALT  49814  amgmw2d  49815  young2d  49816