Theorem rpcnd 12157

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

Syntax hints:   → wi 4   ∈ wcel 2166  ℂcc 10249  ℝ⁺crp 12111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-resscn 10308

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-in 3804  df-ss 3811  df-rp 12112

This theorem is referenced by:  rpcnne0d  12164  ltaddrp2d  12189  prodge0ld  12221  iccf1o  12608  ltexp2r  13210  discr  13294  bcp1nk  13396  bcpasc  13400  sqrlem6  14364  sqrtdiv  14382  absdiv  14411  o1rlimmul  14725  isumrpcl  14948  isumltss  14953  expcnv  14969  mertenslem1  14988  bitsmod  15530  nmoi2  22903  reperflem  22990  icchmeo  23109  icopnfcnv  23110  lebnumlem3  23131  nmoleub2lem2  23284  nmoleub3  23287  minveclem3  23596  pjthlem1  23604  ovollb2lem  23653  sca2rab  23677  ovolscalem1  23678  ovolsca  23680  itg2mulc  23912  itg2cnlem2  23927  c1liplem1  24157  lhop1  24175  aalioulem4  24488  aaliou2b  24494  aaliou3lem2  24496  aaliou3lem3  24497  aaliou3lem8  24498  aaliou3lem6  24501  aaliou3lem7  24502  itgulm  24560  dvradcnv  24573  pserdvlem2  24580  abelthlem7  24590  abelthlem8  24591  lognegb  24734  logno1  24780  advlog  24798  advlogexp  24799  cxprec  24830  divcxp  24831  cxpsqrt  24847  dvcxp1  24882  cxpcn3lem  24889  loglesqrt  24900  relogbval  24911  nnlogbexp  24920  logbrec  24921  asinlem3  25010  cxplim  25110  rlimcxp  25112  cxp2limlem  25114  cxp2lim  25115  cxploglim  25116  cxploglim2  25117  divsqrtsumlem  25118  divsqrtsumo1  25122  amgmlem  25128  zetacvg  25153  lgamucov  25176  basellem3  25221  basellem4  25222  chpval2  25355  logexprlim  25362  bclbnd  25417  bposlem9  25429  chebbnd1lem3  25572  chebbnd1  25573  chtppilimlem2  25575  chtppilim  25576  chebbnd2  25578  chto1lb  25579  chpchtlim  25580  chpo1ubb  25582  rplogsumlem1  25585  rplogsumlem2  25586  dchrvmasumlem1  25596  dchrvmasum2lem  25597  dchrisum0lema  25615  dchrisum0lem1b  25616  dchrisum0lem1  25617  dchrisum0lem2a  25618  dchrisum0lem2  25619  dchrisum0lem3  25620  dchrisum0  25621  mulogsumlem  25632  mulog2sumlem1  25635  mulog2sumlem2  25636  vmalogdivsum2  25639  log2sumbnd  25645  selberg3lem1  25658  selberg3lem2  25659  selberg4lem1  25661  selberg4  25662  selberg34r  25672  pntrlog2bndlem2  25679  pntrlog2bndlem3  25680  pntrlog2bndlem4  25681  pntrlog2bndlem5  25682  pntpbnd1a  25686  pntpbnd2  25688  pntibndlem1  25690  pntibndlem2  25692  pntlemd  25695  pntlemc  25696  pntlemb  25698  pntlemq  25702  pntlemr  25703  pntlemj  25704  pntlemf  25706  pntlemo  25708  pntlem3  25710  pntleml  25712  pnt  25715  padicabvcxp  25733  ostth2lem4  25737  ostth2  25738  ostth3  25739  smcnlem  28106  blocnilem  28213  ubthlem2  28281  bcm1n  30100  probmeasb  31037  signsply0  31174  iprodgam  32169  faclimlem1  32170  faclimlem3  32172  faclim  32173  iprodfac  32174  knoppndvlem17  33050  mblfinlem3  33991  itg2addnclem3  34005  ftc1cnnclem  34025  geomcau  34096  cntotbnd  34136  heibor1lem  34149  rrndstprj2  34171  rrncmslem  34172  pell1qrgaplem  38280  pellfund14  38305  rmxyneg  38327  rmxy1  38329  rmxy0  38330  jm2.23  38405  proot1ex  38621  amgm2d  39340  amgm3d  39341  amgm4d  39342  cvgdvgrat  39351  binomcxplemnn0  39387  binomcxplemnotnn0  39394  ltdivgt1  40368  xralrple4  40385  xralrple3  40386  0ellimcdiv  40675  limclner  40677  fprodsubrecnncnvlem  40915  fprodaddrecnncnvlem  40917  dvdivbd  40932  stoweidlem1  41011  stoweidlem3  41013  stoweidlem7  41017  stoweidlem11  41021  stoweidlem14  41024  stoweidlem24  41034  stoweidlem25  41035  stoweidlem26  41036  stoweidlem42  41052  stoweidlem51  41061  stoweidlem59  41069  stoweidlem62  41072  wallispilem4  41078  wallispilem5  41079  wallispi  41080  wallispi2lem1  41081  stirlinglem4  41087  stirlinglem8  41091  stirlinglem12  41095  stirlinglem15  41098  dirkercncflem4  41116  fourierdlem30  41147  fourierdlem73  41189  fourierdlem87  41203  qndenserrnbllem  41304  hoiqssbllem2  41630  dignn0flhalflem2  43256  itsclc0lem4  43310  amgmwlem  43443  amgmlemALT  43444  amgmw2d  43445  young2d  43446