Theorem rpcnd 13061

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11097  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-ss 3921  df-rp 13016

This theorem is referenced by:  rpcnne0d  13068  ltaddrp2d  13093  prodge0ld  13125  iccf1o  13522  ltexp2r  14209  discr  14276  bcp1nk  14353  bcpasc  14357  01sqrexlem6  15298  sqrtdiv  15316  absdiv  15346  o1rlimmul  15670  isumrpcl  15897  isumltss  15902  expcnv  15918  mertenslem1  15938  bitsmod  16493  nmoi2  24866  reperflem  24955  icopnfcnv  25080  lebnumlem3  25101  nmoleub2lem2  25254  nmoleub3  25257  minveclem3  25567  pjthlem1  25575  ovollb2lem  25626  sca2rab  25650  ovolscalem1  25651  ovolsca  25653  itg2mulc  25885  itg2cnlem2  25900  c1liplem1  26134  lhop1  26152  aalioulem4  26475  aaliou2b  26481  aaliou3lem2  26483  aaliou3lem3  26484  aaliou3lem8  26485  aaliou3lem6  26488  aaliou3lem7  26489  itgulm  26547  dvradcnv  26560  pserdvlem2  26567  abelthlem7  26577  abelthlem8  26578  lognegb  26731  logno1  26777  advlog  26795  advlogexp  26796  cxprec  26827  divcxp  26828  cxpsqrt  26844  dvcxp1  26881  cxpcn3lem  26888  loglesqrt  26902  relogbval  26913  nnlogbexp  26922  logbrec  26923  asinlem3  27012  cxplim  27112  rlimcxp  27114  cxp2limlem  27116  cxp2lim  27117  cxploglim  27118  cxploglim2  27119  divsqrtsumlem  27120  divsqrtsumo1  27124  amgmlem  27130  zetacvg  27155  lgamucov  27178  basellem3  27223  basellem4  27224  chpval2  27358  logexprlim  27365  bclbnd  27420  bposlem9  27432  chebbnd1lem3  27611  chebbnd1  27612  chtppilimlem2  27614  chtppilim  27615  chebbnd2  27617  chto1lb  27618  chpchtlim  27619  chpo1ubb  27621  rplogsumlem1  27624  rplogsumlem2  27625  dchrvmasumlem1  27635  dchrvmasum2lem  27636  dchrisum0lema  27654  dchrisum0lem1b  27655  dchrisum0lem1  27656  dchrisum0lem2a  27657  dchrisum0lem2  27658  dchrisum0lem3  27659  dchrisum0  27660  mulogsumlem  27671  mulog2sumlem1  27674  mulog2sumlem2  27675  vmalogdivsum2  27678  log2sumbnd  27684  selberg3lem1  27697  selberg3lem2  27698  selberg4lem1  27700  selberg4  27701  selberg34r  27711  pntrlog2bndlem2  27718  pntrlog2bndlem3  27719  pntrlog2bndlem4  27720  pntrlog2bndlem5  27721  pntpbnd1a  27725  pntpbnd2  27727  pntibndlem1  27729  pntibndlem2  27731  pntlemd  27734  pntlemc  27735  pntlemb  27737  pntlemq  27741  pntlemr  27742  pntlemj  27743  pntlemf  27745  pntlemo  27747  pntlem3  27749  pntleml  27751  pnt  27754  padicabvcxp  27772  ostth2lem4  27776  ostth2  27777  ostth3  27778  smcnlem  31015  blocnilem  31122  ubthlem2  31189  bcm1n  33106  probmeasb  34786  signsply0  34904  iprodgam  36200  faclimlem1  36201  faclimlem3  36203  faclim  36204  iprodfac  36205  knoppndvlem17  37083  mblfinlem3  38276  itg2addnclem3  38290  ftc1cnnclem  38308  geomcau  38376  cntotbnd  38413  heibor1lem  38426  rrndstprj2  38448  rrncmslem  38449  relogbzexpd  42711  lcmineqlem21  42784  aks4d1p1p1  42798  aks4d1p6  42816  2ap1caineq  42880  exp11d  43055  rplog11d  43076  pell1qrgaplem  43570  pellfund14  43595  rmxyneg  43617  rmxy1  43619  rmxy0  43620  jm2.23  43693  proot1ex  43893  amgm2d  44894  amgm3d  44895  amgm4d  44896  cvgdvgrat  44993  binomcxplemnn0  45029  binomcxplemnotnn0  45036  ltdivgt1  46042  xralrple4  46058  xralrple3  46059  0ellimcdiv  46333  limclner  46335  fprodsubrecnncnvlem  46591  fprodaddrecnncnvlem  46593  dvdivbd  46607  stoweidlem1  46685  stoweidlem3  46687  stoweidlem7  46691  stoweidlem11  46695  stoweidlem14  46698  stoweidlem24  46708  stoweidlem25  46709  stoweidlem26  46710  stoweidlem42  46726  stoweidlem51  46735  stoweidlem59  46743  stoweidlem62  46746  wallispilem4  46752  wallispilem5  46753  wallispi  46754  wallispi2lem1  46755  stirlinglem4  46761  stirlinglem8  46765  stirlinglem12  46769  stirlinglem15  46772  dirkercncflem4  46790  fourierdlem30  46821  fourierdlem73  46863  fourierdlem87  46877  qndenserrnbllem  46978  hoiqssbllem2  47307  dignn0flhalflem2  49363  itsclc0yqsol  49511  amgmwlem  50569  amgmlemALT  50570  amgmw2d  50571  young2d  50572