Theorem rpcnd 12955

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11028  ℝ⁺crp 12909

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-ss 3919  df-rp 12910

This theorem is referenced by:  rpcnne0d  12962  ltaddrp2d  12987  prodge0ld  13019  iccf1o  13416  ltexp2r  14100  discr  14167  bcp1nk  14244  bcpasc  14248  01sqrexlem6  15174  sqrtdiv  15192  absdiv  15222  o1rlimmul  15546  isumrpcl  15770  isumltss  15775  expcnv  15791  mertenslem1  15811  bitsmod  16367  nmoi2  24678  reperflem  24767  icchmeoOLD  24899  icopnfcnv  24900  lebnumlem3  24922  nmoleub2lem2  25076  nmoleub3  25079  minveclem3  25389  pjthlem1  25397  ovollb2lem  25449  sca2rab  25473  ovolscalem1  25474  ovolsca  25476  itg2mulc  25708  itg2cnlem2  25723  c1liplem1  25961  lhop1  25979  aalioulem4  26303  aaliou2b  26309  aaliou3lem2  26311  aaliou3lem3  26312  aaliou3lem8  26313  aaliou3lem6  26316  aaliou3lem7  26317  itgulm  26377  dvradcnv  26390  pserdvlem2  26398  abelthlem7  26408  abelthlem8  26409  lognegb  26559  logno1  26605  advlog  26623  advlogexp  26624  cxprec  26655  divcxp  26656  cxpsqrt  26672  dvcxp1  26709  cxpcn3lem  26717  loglesqrt  26731  relogbval  26742  nnlogbexp  26751  logbrec  26752  asinlem3  26841  cxplim  26942  rlimcxp  26944  cxp2limlem  26946  cxp2lim  26947  cxploglim  26948  cxploglim2  26949  divsqrtsumlem  26950  divsqrtsumo1  26954  amgmlem  26960  zetacvg  26985  lgamucov  27008  basellem3  27053  basellem4  27054  chpval2  27189  logexprlim  27196  bclbnd  27251  bposlem9  27263  chebbnd1lem3  27442  chebbnd1  27443  chtppilimlem2  27445  chtppilim  27446  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ubb  27452  rplogsumlem1  27455  rplogsumlem2  27456  dchrvmasumlem1  27466  dchrvmasum2lem  27467  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  dchrisum0  27491  mulogsumlem  27502  mulog2sumlem1  27505  mulog2sumlem2  27506  vmalogdivsum2  27509  log2sumbnd  27515  selberg3lem1  27528  selberg3lem2  27529  selberg4lem1  27531  selberg4  27532  selberg34r  27542  pntrlog2bndlem2  27549  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  pntpbnd1a  27556  pntpbnd2  27558  pntibndlem1  27560  pntibndlem2  27562  pntlemd  27565  pntlemc  27566  pntlemb  27568  pntlemq  27572  pntlemr  27573  pntlemj  27574  pntlemf  27576  pntlemo  27578  pntlem3  27580  pntleml  27582  pnt  27585  padicabvcxp  27603  ostth2lem4  27607  ostth2  27608  ostth3  27609  smcnlem  30755  blocnilem  30862  ubthlem2  30929  bcm1n  32856  probmeasb  34568  signsply0  34689  iprodgam  35917  faclimlem1  35918  faclimlem3  35920  faclim  35921  iprodfac  35922  knoppndvlem17  36703  mblfinlem3  37831  itg2addnclem3  37845  ftc1cnnclem  37863  geomcau  37931  cntotbnd  37968  heibor1lem  37981  rrndstprj2  38003  rrncmslem  38004  relogbzexpd  42266  lcmineqlem21  42340  aks4d1p1p1  42354  aks4d1p6  42372  2ap1caineq  42436  exp11d  42617  rplog11d  42638  pell1qrgaplem  43151  pellfund14  43176  rmxyneg  43198  rmxy1  43200  rmxy0  43201  jm2.23  43274  proot1ex  43474  amgm2d  44475  amgm3d  44476  amgm4d  44477  cvgdvgrat  44590  binomcxplemnn0  44626  binomcxplemnotnn0  44633  ltdivgt1  45637  xralrple4  45653  xralrple3  45654  0ellimcdiv  45929  limclner  45931  fprodsubrecnncnvlem  46187  fprodaddrecnncnvlem  46189  dvdivbd  46203  stoweidlem1  46281  stoweidlem3  46283  stoweidlem7  46287  stoweidlem11  46291  stoweidlem14  46294  stoweidlem24  46304  stoweidlem25  46305  stoweidlem26  46306  stoweidlem42  46322  stoweidlem51  46331  stoweidlem59  46339  stoweidlem62  46342  wallispilem4  46348  wallispilem5  46349  wallispi  46350  wallispi2lem1  46351  stirlinglem4  46357  stirlinglem8  46361  stirlinglem12  46365  stirlinglem15  46368  dirkercncflem4  46386  fourierdlem30  46417  fourierdlem73  46459  fourierdlem87  46473  qndenserrnbllem  46574  hoiqssbllem2  46903  dignn0flhalflem2  48898  itsclc0yqsol  49046  amgmwlem  50083  amgmlemALT  50084  amgmw2d  50085  young2d  50086