Theorem rpcnd 12939

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  ℝ⁺crp 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-rp 12894

This theorem is referenced by:  rpcnne0d  12946  ltaddrp2d  12971  prodge0ld  13003  iccf1o  13399  ltexp2r  14080  discr  14147  bcp1nk  14224  bcpasc  14228  01sqrexlem6  15154  sqrtdiv  15172  absdiv  15202  o1rlimmul  15526  isumrpcl  15750  isumltss  15755  expcnv  15771  mertenslem1  15791  bitsmod  16347  nmoi2  24616  reperflem  24705  icchmeoOLD  24837  icopnfcnv  24838  lebnumlem3  24860  nmoleub2lem2  25014  nmoleub3  25017  minveclem3  25327  pjthlem1  25335  ovollb2lem  25387  sca2rab  25411  ovolscalem1  25412  ovolsca  25414  itg2mulc  25646  itg2cnlem2  25661  c1liplem1  25899  lhop1  25917  aalioulem4  26241  aaliou2b  26247  aaliou3lem2  26249  aaliou3lem3  26250  aaliou3lem8  26251  aaliou3lem6  26254  aaliou3lem7  26255  itgulm  26315  dvradcnv  26328  pserdvlem2  26336  abelthlem7  26346  abelthlem8  26347  lognegb  26497  logno1  26543  advlog  26561  advlogexp  26562  cxprec  26593  divcxp  26594  cxpsqrt  26610  dvcxp1  26647  cxpcn3lem  26655  loglesqrt  26669  relogbval  26680  nnlogbexp  26689  logbrec  26690  asinlem3  26779  cxplim  26880  rlimcxp  26882  cxp2limlem  26884  cxp2lim  26885  cxploglim  26886  cxploglim2  26887  divsqrtsumlem  26888  divsqrtsumo1  26892  amgmlem  26898  zetacvg  26923  lgamucov  26946  basellem3  26991  basellem4  26992  chpval2  27127  logexprlim  27134  bclbnd  27189  bposlem9  27201  chebbnd1lem3  27380  chebbnd1  27381  chtppilimlem2  27383  chtppilim  27384  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ubb  27390  rplogsumlem1  27393  rplogsumlem2  27394  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0lem3  27428  dchrisum0  27429  mulogsumlem  27440  mulog2sumlem1  27443  mulog2sumlem2  27444  vmalogdivsum2  27447  log2sumbnd  27453  selberg3lem1  27466  selberg3lem2  27467  selberg4lem1  27469  selberg4  27470  selberg34r  27480  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntpbnd1a  27494  pntpbnd2  27496  pntibndlem1  27498  pntibndlem2  27500  pntlemd  27503  pntlemc  27504  pntlemb  27506  pntlemq  27510  pntlemr  27511  pntlemj  27512  pntlemf  27514  pntlemo  27516  pntlem3  27518  pntleml  27520  pnt  27523  padicabvcxp  27541  ostth2lem4  27545  ostth2  27546  ostth3  27547  smcnlem  30645  blocnilem  30752  ubthlem2  30819  bcm1n  32747  probmeasb  34414  signsply0  34535  iprodgam  35735  faclimlem1  35736  faclimlem3  35738  faclim  35739  iprodfac  35740  knoppndvlem17  36522  mblfinlem3  37659  itg2addnclem3  37673  ftc1cnnclem  37691  geomcau  37759  cntotbnd  37796  heibor1lem  37809  rrndstprj2  37831  rrncmslem  37832  relogbzexpd  41968  lcmineqlem21  42042  aks4d1p1p1  42056  aks4d1p6  42074  2ap1caineq  42138  exp11d  42319  rplog11d  42340  pell1qrgaplem  42866  pellfund14  42891  rmxyneg  42913  rmxy1  42915  rmxy0  42916  jm2.23  42989  proot1ex  43189  amgm2d  44191  amgm3d  44192  amgm4d  44193  cvgdvgrat  44306  binomcxplemnn0  44342  binomcxplemnotnn0  44349  ltdivgt1  45356  xralrple4  45372  xralrple3  45373  0ellimcdiv  45650  limclner  45652  fprodsubrecnncnvlem  45908  fprodaddrecnncnvlem  45910  dvdivbd  45924  stoweidlem1  46002  stoweidlem3  46004  stoweidlem7  46008  stoweidlem11  46012  stoweidlem14  46015  stoweidlem24  46025  stoweidlem25  46026  stoweidlem26  46027  stoweidlem42  46043  stoweidlem51  46052  stoweidlem59  46060  stoweidlem62  46063  wallispilem4  46069  wallispilem5  46070  wallispi  46071  wallispi2lem1  46072  stirlinglem4  46078  stirlinglem8  46082  stirlinglem12  46086  stirlinglem15  46089  dirkercncflem4  46107  fourierdlem30  46138  fourierdlem73  46180  fourierdlem87  46194  qndenserrnbllem  46295  hoiqssbllem2  46624  dignn0flhalflem2  48621  itsclc0yqsol  48769  amgmwlem  49807  amgmlemALT  49808  amgmw2d  49809  young2d  49810