Theorem rpcnd 12997

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℝ⁺crp 12951

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 11125

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 3406  df-ss 3931  df-rp 12952

This theorem is referenced by:  rpcnne0d  13004  ltaddrp2d  13029  prodge0ld  13061  iccf1o  13457  ltexp2r  14138  discr  14205  bcp1nk  14282  bcpasc  14286  01sqrexlem6  15213  sqrtdiv  15231  absdiv  15261  o1rlimmul  15585  isumrpcl  15809  isumltss  15814  expcnv  15830  mertenslem1  15850  bitsmod  16406  nmoi2  24618  reperflem  24707  icchmeoOLD  24839  icopnfcnv  24840  lebnumlem3  24862  nmoleub2lem2  25016  nmoleub3  25019  minveclem3  25329  pjthlem1  25337  ovollb2lem  25389  sca2rab  25413  ovolscalem1  25414  ovolsca  25416  itg2mulc  25648  itg2cnlem2  25663  c1liplem1  25901  lhop1  25919  aalioulem4  26243  aaliou2b  26249  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem8  26253  aaliou3lem6  26256  aaliou3lem7  26257  itgulm  26317  dvradcnv  26330  pserdvlem2  26338  abelthlem7  26348  abelthlem8  26349  lognegb  26499  logno1  26545  advlog  26563  advlogexp  26564  cxprec  26595  divcxp  26596  cxpsqrt  26612  dvcxp1  26649  cxpcn3lem  26657  loglesqrt  26671  relogbval  26682  nnlogbexp  26691  logbrec  26692  asinlem3  26781  cxplim  26882  rlimcxp  26884  cxp2limlem  26886  cxp2lim  26887  cxploglim  26888  cxploglim2  26889  divsqrtsumlem  26890  divsqrtsumo1  26894  amgmlem  26900  zetacvg  26925  lgamucov  26948  basellem3  26993  basellem4  26994  chpval2  27129  logexprlim  27136  bclbnd  27191  bposlem9  27203  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem2  27385  chtppilim  27386  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ubb  27392  rplogsumlem1  27395  rplogsumlem2  27396  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  mulogsumlem  27442  mulog2sumlem1  27445  mulog2sumlem2  27446  vmalogdivsum2  27449  log2sumbnd  27455  selberg3lem1  27468  selberg3lem2  27469  selberg4lem1  27471  selberg4  27472  selberg34r  27482  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem1  27500  pntibndlem2  27502  pntlemd  27505  pntlemc  27506  pntlemb  27508  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemo  27518  pntlem3  27520  pntleml  27522  pnt  27525  padicabvcxp  27543  ostth2lem4  27547  ostth2  27548  ostth3  27549  smcnlem  30626  blocnilem  30733  ubthlem2  30800  bcm1n  32718  probmeasb  34421  signsply0  34542  iprodgam  35729  faclimlem1  35730  faclimlem3  35732  faclim  35733  iprodfac  35734  knoppndvlem17  36516  mblfinlem3  37653  itg2addnclem3  37667  ftc1cnnclem  37685  geomcau  37753  cntotbnd  37790  heibor1lem  37803  rrndstprj2  37825  rrncmslem  37826  relogbzexpd  41963  lcmineqlem21  42037  aks4d1p1p1  42051  aks4d1p6  42069  2ap1caineq  42133  exp11d  42314  rplog11d  42335  pell1qrgaplem  42861  pellfund14  42886  rmxyneg  42909  rmxy1  42911  rmxy0  42912  jm2.23  42985  proot1ex  43185  amgm2d  44187  amgm3d  44188  amgm4d  44189  cvgdvgrat  44302  binomcxplemnn0  44338  binomcxplemnotnn0  44345  ltdivgt1  45352  xralrple4  45369  xralrple3  45370  0ellimcdiv  45647  limclner  45649  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvdivbd  45921  stoweidlem1  45999  stoweidlem3  46001  stoweidlem7  46005  stoweidlem11  46009  stoweidlem14  46012  stoweidlem24  46022  stoweidlem25  46023  stoweidlem26  46024  stoweidlem42  46040  stoweidlem51  46049  stoweidlem59  46057  stoweidlem62  46060  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  stirlinglem4  46075  stirlinglem8  46079  stirlinglem12  46083  stirlinglem15  46086  dirkercncflem4  46104  fourierdlem30  46135  fourierdlem73  46177  fourierdlem87  46191  qndenserrnbllem  46292  hoiqssbllem2  46621  dignn0flhalflem2  48605  itsclc0yqsol  48753  amgmwlem  49791  amgmlemALT  49792  amgmw2d  49793  young2d  49794