Theorem rpcnd 12774

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 10869  ℝ⁺crp 12730

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-rp 12731

This theorem is referenced by:  rpcnne0d  12781  ltaddrp2d  12806  prodge0ld  12838  iccf1o  13228  ltexp2r  13891  discr  13955  bcp1nk  14031  bcpasc  14035  sqrlem6  14959  sqrtdiv  14977  absdiv  15007  o1rlimmul  15328  isumrpcl  15555  isumltss  15560  expcnv  15576  mertenslem1  15596  bitsmod  16143  nmoi2  23894  reperflem  23981  icchmeo  24104  icopnfcnv  24105  lebnumlem3  24126  nmoleub2lem2  24279  nmoleub3  24282  minveclem3  24593  pjthlem1  24601  ovollb2lem  24652  sca2rab  24676  ovolscalem1  24677  ovolsca  24679  itg2mulc  24912  itg2cnlem2  24927  c1liplem1  25160  lhop1  25178  aalioulem4  25495  aaliou2b  25501  aaliou3lem2  25503  aaliou3lem3  25504  aaliou3lem8  25505  aaliou3lem6  25508  aaliou3lem7  25509  itgulm  25567  dvradcnv  25580  pserdvlem2  25587  abelthlem7  25597  abelthlem8  25598  lognegb  25745  logno1  25791  advlog  25809  advlogexp  25810  cxprec  25841  divcxp  25842  cxpsqrt  25858  dvcxp1  25893  cxpcn3lem  25900  loglesqrt  25911  relogbval  25922  nnlogbexp  25931  logbrec  25932  asinlem3  26021  cxplim  26121  rlimcxp  26123  cxp2limlem  26125  cxp2lim  26126  cxploglim  26127  cxploglim2  26128  divsqrtsumlem  26129  divsqrtsumo1  26133  amgmlem  26139  zetacvg  26164  lgamucov  26187  basellem3  26232  basellem4  26233  chpval2  26366  logexprlim  26373  bclbnd  26428  bposlem9  26440  chebbnd1lem3  26619  chebbnd1  26620  chtppilimlem2  26622  chtppilim  26623  chebbnd2  26625  chto1lb  26626  chpchtlim  26627  chpo1ubb  26629  rplogsumlem1  26632  rplogsumlem2  26633  dchrvmasumlem1  26643  dchrvmasum2lem  26644  dchrisum0lema  26662  dchrisum0lem1b  26663  dchrisum0lem1  26664  dchrisum0lem2a  26665  dchrisum0lem2  26666  dchrisum0lem3  26667  dchrisum0  26668  mulogsumlem  26679  mulog2sumlem1  26682  mulog2sumlem2  26683  vmalogdivsum2  26686  log2sumbnd  26692  selberg3lem1  26705  selberg3lem2  26706  selberg4lem1  26708  selberg4  26709  selberg34r  26719  pntrlog2bndlem2  26726  pntrlog2bndlem3  26727  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  pntpbnd1a  26733  pntpbnd2  26735  pntibndlem1  26737  pntibndlem2  26739  pntlemd  26742  pntlemc  26743  pntlemb  26745  pntlemq  26749  pntlemr  26750  pntlemj  26751  pntlemf  26753  pntlemo  26755  pntlem3  26757  pntleml  26759  pnt  26762  padicabvcxp  26780  ostth2lem4  26784  ostth2  26785  ostth3  26786  smcnlem  29059  blocnilem  29166  ubthlem2  29233  bcm1n  31116  probmeasb  32397  signsply0  32530  iprodgam  33708  faclimlem1  33709  faclimlem3  33711  faclim  33712  iprodfac  33713  knoppndvlem17  34708  mblfinlem3  35816  itg2addnclem3  35830  ftc1cnnclem  35848  geomcau  35917  cntotbnd  35954  heibor1lem  35967  rrndstprj2  35989  rrncmslem  35990  relogbzexpd  39983  lcmineqlem21  40057  aks4d1p1p1  40071  aks4d1p6  40089  2ap1caineq  40101  exp11d  40325  pell1qrgaplem  40695  pellfund14  40720  rmxyneg  40742  rmxy1  40744  rmxy0  40745  jm2.23  40818  proot1ex  41026  amgm2d  41809  amgm3d  41810  amgm4d  41811  cvgdvgrat  41931  binomcxplemnn0  41967  binomcxplemnotnn0  41974  ltdivgt1  42895  xralrple4  42912  xralrple3  42913  0ellimcdiv  43190  limclner  43192  fprodsubrecnncnvlem  43448  fprodaddrecnncnvlem  43450  dvdivbd  43464  stoweidlem1  43542  stoweidlem3  43544  stoweidlem7  43548  stoweidlem11  43552  stoweidlem14  43555  stoweidlem24  43565  stoweidlem25  43566  stoweidlem26  43567  stoweidlem42  43583  stoweidlem51  43592  stoweidlem59  43600  stoweidlem62  43603  wallispilem4  43609  wallispilem5  43610  wallispi  43611  wallispi2lem1  43612  stirlinglem4  43618  stirlinglem8  43622  stirlinglem12  43626  stirlinglem15  43629  dirkercncflem4  43647  fourierdlem30  43678  fourierdlem73  43720  fourierdlem87  43734  qndenserrnbllem  43835  hoiqssbllem2  44161  dignn0flhalflem2  45962  itsclc0yqsol  46110  amgmwlem  46506  amgmlemALT  46507  amgmw2d  46508  young2d  46509