Theorem rpcnd 12968

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11058  ℝ⁺crp 12924

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-rp 12925

This theorem is referenced by:  rpcnne0d  12975  ltaddrp2d  13000  prodge0ld  13032  iccf1o  13423  ltexp2r  14088  discr  14153  bcp1nk  14227  bcpasc  14231  01sqrexlem6  15144  sqrtdiv  15162  absdiv  15192  o1rlimmul  15513  isumrpcl  15739  isumltss  15744  expcnv  15760  mertenslem1  15780  bitsmod  16327  nmoi2  24131  reperflem  24218  icchmeo  24341  icopnfcnv  24342  lebnumlem3  24363  nmoleub2lem2  24516  nmoleub3  24519  minveclem3  24830  pjthlem1  24838  ovollb2lem  24889  sca2rab  24913  ovolscalem1  24914  ovolsca  24916  itg2mulc  25149  itg2cnlem2  25164  c1liplem1  25397  lhop1  25415  aalioulem4  25732  aaliou2b  25738  aaliou3lem2  25740  aaliou3lem3  25741  aaliou3lem8  25742  aaliou3lem6  25745  aaliou3lem7  25746  itgulm  25804  dvradcnv  25817  pserdvlem2  25824  abelthlem7  25834  abelthlem8  25835  lognegb  25982  logno1  26028  advlog  26046  advlogexp  26047  cxprec  26078  divcxp  26079  cxpsqrt  26095  dvcxp1  26130  cxpcn3lem  26137  loglesqrt  26148  relogbval  26159  nnlogbexp  26168  logbrec  26169  asinlem3  26258  cxplim  26358  rlimcxp  26360  cxp2limlem  26362  cxp2lim  26363  cxploglim  26364  cxploglim2  26365  divsqrtsumlem  26366  divsqrtsumo1  26370  amgmlem  26376  zetacvg  26401  lgamucov  26424  basellem3  26469  basellem4  26470  chpval2  26603  logexprlim  26610  bclbnd  26665  bposlem9  26677  chebbnd1lem3  26856  chebbnd1  26857  chtppilimlem2  26859  chtppilim  26860  chebbnd2  26862  chto1lb  26863  chpchtlim  26864  chpo1ubb  26866  rplogsumlem1  26869  rplogsumlem2  26870  dchrvmasumlem1  26880  dchrvmasum2lem  26881  dchrisum0lema  26899  dchrisum0lem1b  26900  dchrisum0lem1  26901  dchrisum0lem2a  26902  dchrisum0lem2  26903  dchrisum0lem3  26904  dchrisum0  26905  mulogsumlem  26916  mulog2sumlem1  26919  mulog2sumlem2  26920  vmalogdivsum2  26923  log2sumbnd  26929  selberg3lem1  26942  selberg3lem2  26943  selberg4lem1  26945  selberg4  26946  selberg34r  26956  pntrlog2bndlem2  26963  pntrlog2bndlem3  26964  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntpbnd1a  26970  pntpbnd2  26972  pntibndlem1  26974  pntibndlem2  26976  pntlemd  26979  pntlemc  26980  pntlemb  26982  pntlemq  26986  pntlemr  26987  pntlemj  26988  pntlemf  26990  pntlemo  26992  pntlem3  26994  pntleml  26996  pnt  26999  padicabvcxp  27017  ostth2lem4  27021  ostth2  27022  ostth3  27023  smcnlem  29702  blocnilem  29809  ubthlem2  29876  bcm1n  31766  probmeasb  33119  signsply0  33252  iprodgam  34401  faclimlem1  34402  faclimlem3  34404  faclim  34405  iprodfac  34406  knoppndvlem17  35067  mblfinlem3  36190  itg2addnclem3  36204  ftc1cnnclem  36222  geomcau  36291  cntotbnd  36328  heibor1lem  36341  rrndstprj2  36363  rrncmslem  36364  relogbzexpd  40505  lcmineqlem21  40579  aks4d1p1p1  40593  aks4d1p6  40611  2ap1caineq  40626  exp11d  40869  pell1qrgaplem  41254  pellfund14  41279  rmxyneg  41302  rmxy1  41304  rmxy0  41305  jm2.23  41378  proot1ex  41586  amgm2d  42593  amgm3d  42594  amgm4d  42595  cvgdvgrat  42715  binomcxplemnn0  42751  binomcxplemnotnn0  42758  ltdivgt1  43711  xralrple4  43728  xralrple3  43729  0ellimcdiv  44010  limclner  44012  fprodsubrecnncnvlem  44268  fprodaddrecnncnvlem  44270  dvdivbd  44284  stoweidlem1  44362  stoweidlem3  44364  stoweidlem7  44368  stoweidlem11  44372  stoweidlem14  44375  stoweidlem24  44385  stoweidlem25  44386  stoweidlem26  44387  stoweidlem42  44403  stoweidlem51  44412  stoweidlem59  44420  stoweidlem62  44423  wallispilem4  44429  wallispilem5  44430  wallispi  44431  wallispi2lem1  44432  stirlinglem4  44438  stirlinglem8  44442  stirlinglem12  44446  stirlinglem15  44449  dirkercncflem4  44467  fourierdlem30  44498  fourierdlem73  44540  fourierdlem87  44554  qndenserrnbllem  44655  hoiqssbllem2  44984  dignn0flhalflem2  46822  itsclc0yqsol  46970  amgmwlem  47369  amgmlemALT  47370  amgmw2d  47371  young2d  47372