Theorem rpcnd 12879

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 10974  ℝ⁺crp 12835

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 2708  ax-resscn 11033

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-in 3908  df-ss 3918  df-rp 12836

This theorem is referenced by:  rpcnne0d  12886  ltaddrp2d  12911  prodge0ld  12943  iccf1o  13333  ltexp2r  13996  discr  14060  bcp1nk  14136  bcpasc  14140  sqrlem6  15058  sqrtdiv  15076  absdiv  15106  o1rlimmul  15427  isumrpcl  15654  isumltss  15659  expcnv  15675  mertenslem1  15695  bitsmod  16242  nmoi2  23999  reperflem  24086  icchmeo  24209  icopnfcnv  24210  lebnumlem3  24231  nmoleub2lem2  24384  nmoleub3  24387  minveclem3  24698  pjthlem1  24706  ovollb2lem  24757  sca2rab  24781  ovolscalem1  24782  ovolsca  24784  itg2mulc  25017  itg2cnlem2  25032  c1liplem1  25265  lhop1  25283  aalioulem4  25600  aaliou2b  25606  aaliou3lem2  25608  aaliou3lem3  25609  aaliou3lem8  25610  aaliou3lem6  25613  aaliou3lem7  25614  itgulm  25672  dvradcnv  25685  pserdvlem2  25692  abelthlem7  25702  abelthlem8  25703  lognegb  25850  logno1  25896  advlog  25914  advlogexp  25915  cxprec  25946  divcxp  25947  cxpsqrt  25963  dvcxp1  25998  cxpcn3lem  26005  loglesqrt  26016  relogbval  26027  nnlogbexp  26036  logbrec  26037  asinlem3  26126  cxplim  26226  rlimcxp  26228  cxp2limlem  26230  cxp2lim  26231  cxploglim  26232  cxploglim2  26233  divsqrtsumlem  26234  divsqrtsumo1  26238  amgmlem  26244  zetacvg  26269  lgamucov  26292  basellem3  26337  basellem4  26338  chpval2  26471  logexprlim  26478  bclbnd  26533  bposlem9  26545  chebbnd1lem3  26724  chebbnd1  26725  chtppilimlem2  26727  chtppilim  26728  chebbnd2  26730  chto1lb  26731  chpchtlim  26732  chpo1ubb  26734  rplogsumlem1  26737  rplogsumlem2  26738  dchrvmasumlem1  26748  dchrvmasum2lem  26749  dchrisum0lema  26767  dchrisum0lem1b  26768  dchrisum0lem1  26769  dchrisum0lem2a  26770  dchrisum0lem2  26771  dchrisum0lem3  26772  dchrisum0  26773  mulogsumlem  26784  mulog2sumlem1  26787  mulog2sumlem2  26788  vmalogdivsum2  26791  log2sumbnd  26797  selberg3lem1  26810  selberg3lem2  26811  selberg4lem1  26813  selberg4  26814  selberg34r  26824  pntrlog2bndlem2  26831  pntrlog2bndlem3  26832  pntrlog2bndlem4  26833  pntrlog2bndlem5  26834  pntpbnd1a  26838  pntpbnd2  26840  pntibndlem1  26842  pntibndlem2  26844  pntlemd  26847  pntlemc  26848  pntlemb  26850  pntlemq  26854  pntlemr  26855  pntlemj  26856  pntlemf  26858  pntlemo  26860  pntlem3  26862  pntleml  26864  pnt  26867  padicabvcxp  26885  ostth2lem4  26889  ostth2  26890  ostth3  26891  smcnlem  29346  blocnilem  29453  ubthlem2  29520  bcm1n  31401  probmeasb  32695  signsply0  32828  iprodgam  33998  faclimlem1  33999  faclimlem3  34001  faclim  34002  iprodfac  34003  knoppndvlem17  34845  mblfinlem3  35972  itg2addnclem3  35986  ftc1cnnclem  36004  geomcau  36073  cntotbnd  36110  heibor1lem  36123  rrndstprj2  36145  rrncmslem  36146  relogbzexpd  40288  lcmineqlem21  40362  aks4d1p1p1  40376  aks4d1p6  40394  2ap1caineq  40409  exp11d  40636  pell1qrgaplem  41008  pellfund14  41033  rmxyneg  41056  rmxy1  41058  rmxy0  41059  jm2.23  41132  proot1ex  41340  amgm2d  42182  amgm3d  42183  amgm4d  42184  cvgdvgrat  42304  binomcxplemnn0  42340  binomcxplemnotnn0  42347  ltdivgt1  43282  xralrple4  43299  xralrple3  43300  0ellimcdiv  43578  limclner  43580  fprodsubrecnncnvlem  43836  fprodaddrecnncnvlem  43838  dvdivbd  43852  stoweidlem1  43930  stoweidlem3  43932  stoweidlem7  43936  stoweidlem11  43940  stoweidlem14  43943  stoweidlem24  43953  stoweidlem25  43954  stoweidlem26  43955  stoweidlem42  43971  stoweidlem51  43980  stoweidlem59  43988  stoweidlem62  43991  wallispilem4  43997  wallispilem5  43998  wallispi  43999  wallispi2lem1  44000  stirlinglem4  44006  stirlinglem8  44010  stirlinglem12  44014  stirlinglem15  44017  dirkercncflem4  44035  fourierdlem30  44066  fourierdlem73  44108  fourierdlem87  44122  qndenserrnbllem  44223  hoiqssbllem2  44550  dignn0flhalflem2  46380  itsclc0yqsol  46528  amgmwlem  46924  amgmlemALT  46925  amgmw2d  46926  young2d  46927