Theorem rpcnd 12703

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-rp 12660

This theorem is referenced by:  rpcnne0d  12710  ltaddrp2d  12735  prodge0ld  12767  iccf1o  13157  ltexp2r  13819  discr  13883  bcp1nk  13959  bcpasc  13963  sqrlem6  14887  sqrtdiv  14905  absdiv  14935  o1rlimmul  15256  isumrpcl  15483  isumltss  15488  expcnv  15504  mertenslem1  15524  bitsmod  16071  nmoi2  23800  reperflem  23887  icchmeo  24010  icopnfcnv  24011  lebnumlem3  24032  nmoleub2lem2  24185  nmoleub3  24188  minveclem3  24498  pjthlem1  24506  ovollb2lem  24557  sca2rab  24581  ovolscalem1  24582  ovolsca  24584  itg2mulc  24817  itg2cnlem2  24832  c1liplem1  25065  lhop1  25083  aalioulem4  25400  aaliou2b  25406  aaliou3lem2  25408  aaliou3lem3  25409  aaliou3lem8  25410  aaliou3lem6  25413  aaliou3lem7  25414  itgulm  25472  dvradcnv  25485  pserdvlem2  25492  abelthlem7  25502  abelthlem8  25503  lognegb  25650  logno1  25696  advlog  25714  advlogexp  25715  cxprec  25746  divcxp  25747  cxpsqrt  25763  dvcxp1  25798  cxpcn3lem  25805  loglesqrt  25816  relogbval  25827  nnlogbexp  25836  logbrec  25837  asinlem3  25926  cxplim  26026  rlimcxp  26028  cxp2limlem  26030  cxp2lim  26031  cxploglim  26032  cxploglim2  26033  divsqrtsumlem  26034  divsqrtsumo1  26038  amgmlem  26044  zetacvg  26069  lgamucov  26092  basellem3  26137  basellem4  26138  chpval2  26271  logexprlim  26278  bclbnd  26333  bposlem9  26345  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem2  26527  chtppilim  26528  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ubb  26534  rplogsumlem1  26537  rplogsumlem2  26538  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  mulogsumlem  26584  mulog2sumlem1  26587  mulog2sumlem2  26588  vmalogdivsum2  26591  log2sumbnd  26597  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  selberg4  26614  selberg34r  26624  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem1  26642  pntibndlem2  26644  pntlemd  26647  pntlemc  26648  pntlemb  26650  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemo  26660  pntlem3  26662  pntleml  26664  pnt  26667  padicabvcxp  26685  ostth2lem4  26689  ostth2  26690  ostth3  26691  smcnlem  28960  blocnilem  29067  ubthlem2  29134  bcm1n  31018  probmeasb  32297  signsply0  32430  iprodgam  33614  faclimlem1  33615  faclimlem3  33617  faclim  33618  iprodfac  33619  knoppndvlem17  34635  mblfinlem3  35743  itg2addnclem3  35757  ftc1cnnclem  35775  geomcau  35844  cntotbnd  35881  heibor1lem  35894  rrndstprj2  35916  rrncmslem  35917  relogbzexpd  39910  lcmineqlem21  39985  aks4d1p1p1  39999  aks4d1p6  40017  2ap1caineq  40029  exp11d  40246  pell1qrgaplem  40611  pellfund14  40636  rmxyneg  40658  rmxy1  40660  rmxy0  40661  jm2.23  40734  proot1ex  40942  amgm2d  41698  amgm3d  41699  amgm4d  41700  cvgdvgrat  41820  binomcxplemnn0  41856  binomcxplemnotnn0  41863  ltdivgt1  42785  xralrple4  42802  xralrple3  42803  0ellimcdiv  43080  limclner  43082  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvdivbd  43354  stoweidlem1  43432  stoweidlem3  43434  stoweidlem7  43438  stoweidlem11  43442  stoweidlem14  43445  stoweidlem24  43455  stoweidlem25  43456  stoweidlem26  43457  stoweidlem42  43473  stoweidlem51  43482  stoweidlem59  43490  stoweidlem62  43493  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  stirlinglem4  43508  stirlinglem8  43512  stirlinglem12  43516  stirlinglem15  43519  dirkercncflem4  43537  fourierdlem30  43568  fourierdlem73  43610  fourierdlem87  43624  qndenserrnbllem  43725  hoiqssbllem2  44051  dignn0flhalflem2  45850  itsclc0yqsol  45998  amgmwlem  46392  amgmlemALT  46393  amgmw2d  46394  young2d  46395