Theorem rpcnd 13018

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℝ⁺crp 12974

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-rp 12975

This theorem is referenced by:  rpcnne0d  13025  ltaddrp2d  13050  prodge0ld  13082  iccf1o  13473  ltexp2r  14138  discr  14203  bcp1nk  14277  bcpasc  14281  01sqrexlem6  15194  sqrtdiv  15212  absdiv  15242  o1rlimmul  15563  isumrpcl  15789  isumltss  15794  expcnv  15810  mertenslem1  15830  bitsmod  16377  nmoi2  24247  reperflem  24334  icchmeo  24457  icopnfcnv  24458  lebnumlem3  24479  nmoleub2lem2  24632  nmoleub3  24635  minveclem3  24946  pjthlem1  24954  ovollb2lem  25005  sca2rab  25029  ovolscalem1  25030  ovolsca  25032  itg2mulc  25265  itg2cnlem2  25280  c1liplem1  25513  lhop1  25531  aalioulem4  25848  aaliou2b  25854  aaliou3lem2  25856  aaliou3lem3  25857  aaliou3lem8  25858  aaliou3lem6  25861  aaliou3lem7  25862  itgulm  25920  dvradcnv  25933  pserdvlem2  25940  abelthlem7  25950  abelthlem8  25951  lognegb  26098  logno1  26144  advlog  26162  advlogexp  26163  cxprec  26194  divcxp  26195  cxpsqrt  26211  dvcxp1  26248  cxpcn3lem  26255  loglesqrt  26266  relogbval  26277  nnlogbexp  26286  logbrec  26287  asinlem3  26376  cxplim  26476  rlimcxp  26478  cxp2limlem  26480  cxp2lim  26481  cxploglim  26482  cxploglim2  26483  divsqrtsumlem  26484  divsqrtsumo1  26488  amgmlem  26494  zetacvg  26519  lgamucov  26542  basellem3  26587  basellem4  26588  chpval2  26721  logexprlim  26728  bclbnd  26783  bposlem9  26795  chebbnd1lem3  26974  chebbnd1  26975  chtppilimlem2  26977  chtppilim  26978  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ubb  26984  rplogsumlem1  26987  rplogsumlem2  26988  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  dchrisum0  27023  mulogsumlem  27034  mulog2sumlem1  27037  mulog2sumlem2  27038  vmalogdivsum2  27041  log2sumbnd  27047  selberg3lem1  27060  selberg3lem2  27061  selberg4lem1  27063  selberg4  27064  selberg34r  27074  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem1  27092  pntibndlem2  27094  pntlemd  27097  pntlemc  27098  pntlemb  27100  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemf  27108  pntlemo  27110  pntlem3  27112  pntleml  27114  pnt  27117  padicabvcxp  27135  ostth2lem4  27139  ostth2  27140  ostth3  27141  smcnlem  29981  blocnilem  30088  ubthlem2  30155  bcm1n  32037  probmeasb  33460  signsply0  33593  iprodgam  34743  faclimlem1  34744  faclimlem3  34746  faclim  34747  iprodfac  34748  knoppndvlem17  35452  mblfinlem3  36575  itg2addnclem3  36589  ftc1cnnclem  36607  geomcau  36675  cntotbnd  36712  heibor1lem  36725  rrndstprj2  36747  rrncmslem  36748  relogbzexpd  40888  lcmineqlem21  40962  aks4d1p1p1  40976  aks4d1p6  40994  2ap1caineq  41009  exp11d  41264  pell1qrgaplem  41659  pellfund14  41684  rmxyneg  41707  rmxy1  41709  rmxy0  41710  jm2.23  41783  proot1ex  41991  amgm2d  42998  amgm3d  42999  amgm4d  43000  cvgdvgrat  43120  binomcxplemnn0  43156  binomcxplemnotnn0  43163  ltdivgt1  44114  xralrple4  44131  xralrple3  44132  0ellimcdiv  44413  limclner  44415  fprodsubrecnncnvlem  44671  fprodaddrecnncnvlem  44673  dvdivbd  44687  stoweidlem1  44765  stoweidlem3  44767  stoweidlem7  44771  stoweidlem11  44775  stoweidlem14  44778  stoweidlem24  44788  stoweidlem25  44789  stoweidlem26  44790  stoweidlem42  44806  stoweidlem51  44815  stoweidlem59  44823  stoweidlem62  44826  wallispilem4  44832  wallispilem5  44833  wallispi  44834  wallispi2lem1  44835  stirlinglem4  44841  stirlinglem8  44845  stirlinglem12  44849  stirlinglem15  44852  dirkercncflem4  44870  fourierdlem30  44901  fourierdlem73  44943  fourierdlem87  44957  qndenserrnbllem  45058  hoiqssbllem2  45387  dignn0flhalflem2  47350  itsclc0yqsol  47498  amgmwlem  47897  amgmlemALT  47898  amgmw2d  47899  young2d  47900