Theorem rpcnd 12630

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10727  ℝ⁺crp 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-resscn 10786

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883  df-rp 12587

This theorem is referenced by:  rpcnne0d  12637  ltaddrp2d  12662  prodge0ld  12694  iccf1o  13084  ltexp2r  13743  discr  13807  bcp1nk  13883  bcpasc  13887  sqrlem6  14811  sqrtdiv  14829  absdiv  14859  o1rlimmul  15180  isumrpcl  15407  isumltss  15412  expcnv  15428  mertenslem1  15448  bitsmod  15995  nmoi2  23628  reperflem  23715  icchmeo  23838  icopnfcnv  23839  lebnumlem3  23860  nmoleub2lem2  24013  nmoleub3  24016  minveclem3  24326  pjthlem1  24334  ovollb2lem  24385  sca2rab  24409  ovolscalem1  24410  ovolsca  24412  itg2mulc  24645  itg2cnlem2  24660  c1liplem1  24893  lhop1  24911  aalioulem4  25228  aaliou2b  25234  aaliou3lem2  25236  aaliou3lem3  25237  aaliou3lem8  25238  aaliou3lem6  25241  aaliou3lem7  25242  itgulm  25300  dvradcnv  25313  pserdvlem2  25320  abelthlem7  25330  abelthlem8  25331  lognegb  25478  logno1  25524  advlog  25542  advlogexp  25543  cxprec  25574  divcxp  25575  cxpsqrt  25591  dvcxp1  25626  cxpcn3lem  25633  loglesqrt  25644  relogbval  25655  nnlogbexp  25664  logbrec  25665  asinlem3  25754  cxplim  25854  rlimcxp  25856  cxp2limlem  25858  cxp2lim  25859  cxploglim  25860  cxploglim2  25861  divsqrtsumlem  25862  divsqrtsumo1  25866  amgmlem  25872  zetacvg  25897  lgamucov  25920  basellem3  25965  basellem4  25966  chpval2  26099  logexprlim  26106  bclbnd  26161  bposlem9  26173  chebbnd1lem3  26352  chebbnd1  26353  chtppilimlem2  26355  chtppilim  26356  chebbnd2  26358  chto1lb  26359  chpchtlim  26360  chpo1ubb  26362  rplogsumlem1  26365  rplogsumlem2  26366  dchrvmasumlem1  26376  dchrvmasum2lem  26377  dchrisum0lema  26395  dchrisum0lem1b  26396  dchrisum0lem1  26397  dchrisum0lem2a  26398  dchrisum0lem2  26399  dchrisum0lem3  26400  dchrisum0  26401  mulogsumlem  26412  mulog2sumlem1  26415  mulog2sumlem2  26416  vmalogdivsum2  26419  log2sumbnd  26425  selberg3lem1  26438  selberg3lem2  26439  selberg4lem1  26441  selberg4  26442  selberg34r  26452  pntrlog2bndlem2  26459  pntrlog2bndlem3  26460  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  pntpbnd1a  26466  pntpbnd2  26468  pntibndlem1  26470  pntibndlem2  26472  pntlemd  26475  pntlemc  26476  pntlemb  26478  pntlemq  26482  pntlemr  26483  pntlemj  26484  pntlemf  26486  pntlemo  26488  pntlem3  26490  pntleml  26492  pnt  26495  padicabvcxp  26513  ostth2lem4  26517  ostth2  26518  ostth3  26519  smcnlem  28778  blocnilem  28885  ubthlem2  28952  bcm1n  30836  probmeasb  32109  signsply0  32242  iprodgam  33426  faclimlem1  33427  faclimlem3  33429  faclim  33430  iprodfac  33431  knoppndvlem17  34445  mblfinlem3  35553  itg2addnclem3  35567  ftc1cnnclem  35585  geomcau  35654  cntotbnd  35691  heibor1lem  35704  rrndstprj2  35726  rrncmslem  35727  relogbzexpd  39716  lcmineqlem21  39791  aks4d1p1p1  39804  2ap1caineq  39823  exp11d  40033  cxpgt0d  40052  pell1qrgaplem  40398  pellfund14  40423  rmxyneg  40445  rmxy1  40447  rmxy0  40448  jm2.23  40521  proot1ex  40729  amgm2d  41487  amgm3d  41488  amgm4d  41489  cvgdvgrat  41604  binomcxplemnn0  41640  binomcxplemnotnn0  41647  ltdivgt1  42568  xralrple4  42585  xralrple3  42586  0ellimcdiv  42865  limclner  42867  fprodsubrecnncnvlem  43123  fprodaddrecnncnvlem  43125  dvdivbd  43139  stoweidlem1  43217  stoweidlem3  43219  stoweidlem7  43223  stoweidlem11  43227  stoweidlem14  43230  stoweidlem24  43240  stoweidlem25  43241  stoweidlem26  43242  stoweidlem42  43258  stoweidlem51  43267  stoweidlem59  43275  stoweidlem62  43278  wallispilem4  43284  wallispilem5  43285  wallispi  43286  wallispi2lem1  43287  stirlinglem4  43293  stirlinglem8  43297  stirlinglem12  43301  stirlinglem15  43304  dirkercncflem4  43322  fourierdlem30  43353  fourierdlem73  43395  fourierdlem87  43409  qndenserrnbllem  43510  hoiqssbllem2  43836  dignn0flhalflem2  45635  itsclc0yqsol  45783  amgmwlem  46177  amgmlemALT  46178  amgmw2d  46179  young2d  46180