Theorem rpcnd 12946

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11014  ℝ⁺crp 12900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-ss 3916  df-rp 12901

This theorem is referenced by:  rpcnne0d  12953  ltaddrp2d  12978  prodge0ld  13010  iccf1o  13406  ltexp2r  14090  discr  14157  bcp1nk  14234  bcpasc  14238  01sqrexlem6  15164  sqrtdiv  15182  absdiv  15212  o1rlimmul  15536  isumrpcl  15760  isumltss  15765  expcnv  15781  mertenslem1  15801  bitsmod  16357  nmoi2  24655  reperflem  24744  icchmeoOLD  24876  icopnfcnv  24877  lebnumlem3  24899  nmoleub2lem2  25053  nmoleub3  25056  minveclem3  25366  pjthlem1  25374  ovollb2lem  25426  sca2rab  25450  ovolscalem1  25451  ovolsca  25453  itg2mulc  25685  itg2cnlem2  25700  c1liplem1  25938  lhop1  25956  aalioulem4  26280  aaliou2b  26286  aaliou3lem2  26288  aaliou3lem3  26289  aaliou3lem8  26290  aaliou3lem6  26293  aaliou3lem7  26294  itgulm  26354  dvradcnv  26367  pserdvlem2  26375  abelthlem7  26385  abelthlem8  26386  lognegb  26536  logno1  26582  advlog  26600  advlogexp  26601  cxprec  26632  divcxp  26633  cxpsqrt  26649  dvcxp1  26686  cxpcn3lem  26694  loglesqrt  26708  relogbval  26719  nnlogbexp  26728  logbrec  26729  asinlem3  26818  cxplim  26919  rlimcxp  26921  cxp2limlem  26923  cxp2lim  26924  cxploglim  26925  cxploglim2  26926  divsqrtsumlem  26927  divsqrtsumo1  26931  amgmlem  26937  zetacvg  26962  lgamucov  26985  basellem3  27030  basellem4  27031  chpval2  27166  logexprlim  27173  bclbnd  27228  bposlem9  27240  chebbnd1lem3  27419  chebbnd1  27420  chtppilimlem2  27422  chtppilim  27423  chebbnd2  27425  chto1lb  27426  chpchtlim  27427  chpo1ubb  27429  rplogsumlem1  27432  rplogsumlem2  27433  dchrvmasumlem1  27443  dchrvmasum2lem  27444  dchrisum0lema  27462  dchrisum0lem1b  27463  dchrisum0lem1  27464  dchrisum0lem2a  27465  dchrisum0lem2  27466  dchrisum0lem3  27467  dchrisum0  27468  mulogsumlem  27479  mulog2sumlem1  27482  mulog2sumlem2  27483  vmalogdivsum2  27486  log2sumbnd  27492  selberg3lem1  27505  selberg3lem2  27506  selberg4lem1  27508  selberg4  27509  selberg34r  27519  pntrlog2bndlem2  27526  pntrlog2bndlem3  27527  pntrlog2bndlem4  27528  pntrlog2bndlem5  27529  pntpbnd1a  27533  pntpbnd2  27535  pntibndlem1  27537  pntibndlem2  27539  pntlemd  27542  pntlemc  27543  pntlemb  27545  pntlemq  27549  pntlemr  27550  pntlemj  27551  pntlemf  27553  pntlemo  27555  pntlem3  27557  pntleml  27559  pnt  27562  padicabvcxp  27580  ostth2lem4  27584  ostth2  27585  ostth3  27586  smcnlem  30688  blocnilem  30795  ubthlem2  30862  bcm1n  32788  probmeasb  34454  signsply0  34575  iprodgam  35797  faclimlem1  35798  faclimlem3  35800  faclim  35801  iprodfac  35802  knoppndvlem17  36583  mblfinlem3  37709  itg2addnclem3  37723  ftc1cnnclem  37741  geomcau  37809  cntotbnd  37846  heibor1lem  37859  rrndstprj2  37881  rrncmslem  37882  relogbzexpd  42078  lcmineqlem21  42152  aks4d1p1p1  42166  aks4d1p6  42184  2ap1caineq  42248  exp11d  42434  rplog11d  42455  pell1qrgaplem  42980  pellfund14  43005  rmxyneg  43027  rmxy1  43029  rmxy0  43030  jm2.23  43103  proot1ex  43303  amgm2d  44305  amgm3d  44306  amgm4d  44307  cvgdvgrat  44420  binomcxplemnn0  44456  binomcxplemnotnn0  44463  ltdivgt1  45469  xralrple4  45485  xralrple3  45486  0ellimcdiv  45761  limclner  45763  fprodsubrecnncnvlem  46019  fprodaddrecnncnvlem  46021  dvdivbd  46035  stoweidlem1  46113  stoweidlem3  46115  stoweidlem7  46119  stoweidlem11  46123  stoweidlem14  46126  stoweidlem24  46136  stoweidlem25  46137  stoweidlem26  46138  stoweidlem42  46154  stoweidlem51  46163  stoweidlem59  46171  stoweidlem62  46174  wallispilem4  46180  wallispilem5  46181  wallispi  46182  wallispi2lem1  46183  stirlinglem4  46189  stirlinglem8  46193  stirlinglem12  46197  stirlinglem15  46200  dirkercncflem4  46218  fourierdlem30  46249  fourierdlem73  46291  fourierdlem87  46305  qndenserrnbllem  46406  hoiqssbllem2  46735  dignn0flhalflem2  48731  itsclc0yqsol  48879  amgmwlem  49917  amgmlemALT  49918  amgmw2d  49919  young2d  49920