Theorem rpcnd 13004

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℝ⁺crp 12958

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 2702  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-rp 12959

This theorem is referenced by:  rpcnne0d  13011  ltaddrp2d  13036  prodge0ld  13068  iccf1o  13464  ltexp2r  14145  discr  14212  bcp1nk  14289  bcpasc  14293  01sqrexlem6  15220  sqrtdiv  15238  absdiv  15268  o1rlimmul  15592  isumrpcl  15816  isumltss  15821  expcnv  15837  mertenslem1  15857  bitsmod  16413  nmoi2  24625  reperflem  24714  icchmeoOLD  24846  icopnfcnv  24847  lebnumlem3  24869  nmoleub2lem2  25023  nmoleub3  25026  minveclem3  25336  pjthlem1  25344  ovollb2lem  25396  sca2rab  25420  ovolscalem1  25421  ovolsca  25423  itg2mulc  25655  itg2cnlem2  25670  c1liplem1  25908  lhop1  25926  aalioulem4  26250  aaliou2b  26256  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem8  26260  aaliou3lem6  26263  aaliou3lem7  26264  itgulm  26324  dvradcnv  26337  pserdvlem2  26345  abelthlem7  26355  abelthlem8  26356  lognegb  26506  logno1  26552  advlog  26570  advlogexp  26571  cxprec  26602  divcxp  26603  cxpsqrt  26619  dvcxp1  26656  cxpcn3lem  26664  loglesqrt  26678  relogbval  26689  nnlogbexp  26698  logbrec  26699  asinlem3  26788  cxplim  26889  rlimcxp  26891  cxp2limlem  26893  cxp2lim  26894  cxploglim  26895  cxploglim2  26896  divsqrtsumlem  26897  divsqrtsumo1  26901  amgmlem  26907  zetacvg  26932  lgamucov  26955  basellem3  27000  basellem4  27001  chpval2  27136  logexprlim  27143  bclbnd  27198  bposlem9  27210  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem2  27392  chtppilim  27393  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ubb  27399  rplogsumlem1  27402  rplogsumlem2  27403  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrisum0  27438  mulogsumlem  27449  mulog2sumlem1  27452  mulog2sumlem2  27453  vmalogdivsum2  27456  log2sumbnd  27462  selberg3lem1  27475  selberg3lem2  27476  selberg4lem1  27478  selberg4  27479  selberg34r  27489  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem1  27507  pntibndlem2  27509  pntlemd  27512  pntlemc  27513  pntlemb  27515  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemf  27523  pntlemo  27525  pntlem3  27527  pntleml  27529  pnt  27532  padicabvcxp  27550  ostth2lem4  27554  ostth2  27555  ostth3  27556  smcnlem  30633  blocnilem  30740  ubthlem2  30807  bcm1n  32725  probmeasb  34428  signsply0  34549  iprodgam  35736  faclimlem1  35737  faclimlem3  35739  faclim  35740  iprodfac  35741  knoppndvlem17  36523  mblfinlem3  37660  itg2addnclem3  37674  ftc1cnnclem  37692  geomcau  37760  cntotbnd  37797  heibor1lem  37810  rrndstprj2  37832  rrncmslem  37833  relogbzexpd  41970  lcmineqlem21  42044  aks4d1p1p1  42058  aks4d1p6  42076  2ap1caineq  42140  exp11d  42321  rplog11d  42342  pell1qrgaplem  42868  pellfund14  42893  rmxyneg  42916  rmxy1  42918  rmxy0  42919  jm2.23  42992  proot1ex  43192  amgm2d  44194  amgm3d  44195  amgm4d  44196  cvgdvgrat  44309  binomcxplemnn0  44345  binomcxplemnotnn0  44352  ltdivgt1  45359  xralrple4  45376  xralrple3  45377  0ellimcdiv  45654  limclner  45656  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvdivbd  45928  stoweidlem1  46006  stoweidlem3  46008  stoweidlem7  46012  stoweidlem11  46016  stoweidlem14  46019  stoweidlem24  46029  stoweidlem25  46030  stoweidlem26  46031  stoweidlem42  46047  stoweidlem51  46056  stoweidlem59  46064  stoweidlem62  46067  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  stirlinglem4  46082  stirlinglem8  46086  stirlinglem12  46090  stirlinglem15  46093  dirkercncflem4  46111  fourierdlem30  46142  fourierdlem73  46184  fourierdlem87  46198  qndenserrnbllem  46299  hoiqssbllem2  46628  dignn0flhalflem2  48609  itsclc0yqsol  48757  amgmwlem  49795  amgmlemALT  49796  amgmw2d  49797  young2d  49798