Theorem rpcnd 13076

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-ss 3979  df-rp 13032

This theorem is referenced by:  rpcnne0d  13083  ltaddrp2d  13108  prodge0ld  13140  iccf1o  13532  ltexp2r  14209  discr  14275  bcp1nk  14352  bcpasc  14356  01sqrexlem6  15282  sqrtdiv  15300  absdiv  15330  o1rlimmul  15651  isumrpcl  15875  isumltss  15880  expcnv  15896  mertenslem1  15916  bitsmod  16469  nmoi2  24766  reperflem  24853  icchmeoOLD  24985  icopnfcnv  24986  lebnumlem3  25008  nmoleub2lem2  25162  nmoleub3  25165  minveclem3  25476  pjthlem1  25484  ovollb2lem  25536  sca2rab  25560  ovolscalem1  25561  ovolsca  25563  itg2mulc  25796  itg2cnlem2  25811  c1liplem1  26049  lhop1  26067  aalioulem4  26391  aaliou2b  26397  aaliou3lem2  26399  aaliou3lem3  26400  aaliou3lem8  26401  aaliou3lem6  26404  aaliou3lem7  26405  itgulm  26465  dvradcnv  26478  pserdvlem2  26486  abelthlem7  26496  abelthlem8  26497  lognegb  26646  logno1  26692  advlog  26710  advlogexp  26711  cxprec  26742  divcxp  26743  cxpsqrt  26759  dvcxp1  26796  cxpcn3lem  26804  loglesqrt  26818  relogbval  26829  nnlogbexp  26838  logbrec  26839  asinlem3  26928  cxplim  27029  rlimcxp  27031  cxp2limlem  27033  cxp2lim  27034  cxploglim  27035  cxploglim2  27036  divsqrtsumlem  27037  divsqrtsumo1  27041  amgmlem  27047  zetacvg  27072  lgamucov  27095  basellem3  27140  basellem4  27141  chpval2  27276  logexprlim  27283  bclbnd  27338  bposlem9  27350  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem2  27532  chtppilim  27533  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ubb  27539  rplogsumlem1  27542  rplogsumlem2  27543  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  dchrisum0  27578  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  vmalogdivsum2  27596  log2sumbnd  27602  selberg3lem1  27615  selberg3lem2  27616  selberg4lem1  27618  selberg4  27619  selberg34r  27629  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem1  27647  pntibndlem2  27649  pntlemd  27652  pntlemc  27653  pntlemb  27655  pntlemq  27659  pntlemr  27660  pntlemj  27661  pntlemf  27663  pntlemo  27665  pntlem3  27667  pntleml  27669  pnt  27672  padicabvcxp  27690  ostth2lem4  27694  ostth2  27695  ostth3  27696  smcnlem  30725  blocnilem  30832  ubthlem2  30899  bcm1n  32802  probmeasb  34411  signsply0  34544  iprodgam  35721  faclimlem1  35722  faclimlem3  35724  faclim  35725  iprodfac  35726  knoppndvlem17  36510  mblfinlem3  37645  itg2addnclem3  37659  ftc1cnnclem  37677  geomcau  37745  cntotbnd  37782  heibor1lem  37795  rrndstprj2  37817  rrncmslem  37818  relogbzexpd  41956  lcmineqlem21  42030  aks4d1p1p1  42044  aks4d1p6  42062  2ap1caineq  42126  exp11d  42339  rplog11d  42361  pell1qrgaplem  42860  pellfund14  42885  rmxyneg  42908  rmxy1  42910  rmxy0  42911  jm2.23  42984  proot1ex  43184  amgm2d  44187  amgm3d  44188  amgm4d  44189  cvgdvgrat  44308  binomcxplemnn0  44344  binomcxplemnotnn0  44351  ltdivgt1  45305  xralrple4  45322  xralrple3  45323  0ellimcdiv  45604  limclner  45606  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  dvdivbd  45878  stoweidlem1  45956  stoweidlem3  45958  stoweidlem7  45962  stoweidlem11  45966  stoweidlem14  45969  stoweidlem24  45979  stoweidlem25  45980  stoweidlem26  45981  stoweidlem42  45997  stoweidlem51  46006  stoweidlem59  46014  stoweidlem62  46017  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  stirlinglem4  46032  stirlinglem8  46036  stirlinglem12  46040  stirlinglem15  46043  dirkercncflem4  46061  fourierdlem30  46092  fourierdlem73  46134  fourierdlem87  46148  qndenserrnbllem  46249  hoiqssbllem2  46578  dignn0flhalflem2  48465  itsclc0yqsol  48613  amgmwlem  49032  amgmlemALT  49033  amgmw2d  49034  young2d  49035