Theorem rpcnd 12283

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

Syntax hints:   → wi 4   ∈ wcel 2081  ℂcc 10381  ℝ⁺crp 12239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-resscn 10440

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-in 3866  df-ss 3874  df-rp 12240

This theorem is referenced by:  rpcnne0d  12290  ltaddrp2d  12315  prodge0ld  12347  iccf1o  12732  ltexp2r  13387  discr  13451  bcp1nk  13527  bcpasc  13531  sqrlem6  14441  sqrtdiv  14459  absdiv  14489  o1rlimmul  14809  isumrpcl  15031  isumltss  15036  expcnv  15052  mertenslem1  15073  bitsmod  15618  nmoi2  23022  reperflem  23109  icchmeo  23228  icopnfcnv  23229  lebnumlem3  23250  nmoleub2lem2  23403  nmoleub3  23406  minveclem3  23715  pjthlem1  23723  ovollb2lem  23772  sca2rab  23796  ovolscalem1  23797  ovolsca  23799  itg2mulc  24031  itg2cnlem2  24046  c1liplem1  24276  lhop1  24294  aalioulem4  24607  aaliou2b  24613  aaliou3lem2  24615  aaliou3lem3  24616  aaliou3lem8  24617  aaliou3lem6  24620  aaliou3lem7  24621  itgulm  24679  dvradcnv  24692  pserdvlem2  24699  abelthlem7  24709  abelthlem8  24710  lognegb  24854  logno1  24900  advlog  24918  advlogexp  24919  cxprec  24950  divcxp  24951  cxpsqrt  24967  dvcxp1  25002  cxpcn3lem  25009  loglesqrt  25020  relogbval  25031  nnlogbexp  25040  logbrec  25041  asinlem3  25130  cxplim  25231  rlimcxp  25233  cxp2limlem  25235  cxp2lim  25236  cxploglim  25237  cxploglim2  25238  divsqrtsumlem  25239  divsqrtsumo1  25243  amgmlem  25249  zetacvg  25274  lgamucov  25297  basellem3  25342  basellem4  25343  chpval2  25476  logexprlim  25483  bclbnd  25538  bposlem9  25550  chebbnd1lem3  25729  chebbnd1  25730  chtppilimlem2  25732  chtppilim  25733  chebbnd2  25735  chto1lb  25736  chpchtlim  25737  chpo1ubb  25739  rplogsumlem1  25742  rplogsumlem2  25743  dchrvmasumlem1  25753  dchrvmasum2lem  25754  dchrisum0lema  25772  dchrisum0lem1b  25773  dchrisum0lem1  25774  dchrisum0lem2a  25775  dchrisum0lem2  25776  dchrisum0lem3  25777  dchrisum0  25778  mulogsumlem  25789  mulog2sumlem1  25792  mulog2sumlem2  25793  vmalogdivsum2  25796  log2sumbnd  25802  selberg3lem1  25815  selberg3lem2  25816  selberg4lem1  25818  selberg4  25819  selberg34r  25829  pntrlog2bndlem2  25836  pntrlog2bndlem3  25837  pntrlog2bndlem4  25838  pntrlog2bndlem5  25839  pntpbnd1a  25843  pntpbnd2  25845  pntibndlem1  25847  pntibndlem2  25849  pntlemd  25852  pntlemc  25853  pntlemb  25855  pntlemq  25859  pntlemr  25860  pntlemj  25861  pntlemf  25863  pntlemo  25865  pntlem3  25867  pntleml  25869  pnt  25872  padicabvcxp  25890  ostth2lem4  25894  ostth2  25895  ostth3  25896  smcnlem  28165  blocnilem  28272  ubthlem2  28339  bcm1n  30204  probmeasb  31305  signsply0  31438  iprodgam  32582  faclimlem1  32583  faclimlem3  32585  faclim  32586  iprodfac  32587  knoppndvlem17  33476  mblfinlem3  34462  itg2addnclem3  34476  ftc1cnnclem  34496  geomcau  34566  cntotbnd  34606  heibor1lem  34619  rrndstprj2  34641  rrncmslem  34642  cxpgt0d  38702  exp11d  38711  pell1qrgaplem  38955  pellfund14  38980  rmxyneg  39002  rmxy1  39004  rmxy0  39005  jm2.23  39078  proot1ex  39286  amgm2d  40037  amgm3d  40038  amgm4d  40039  cvgdvgrat  40183  binomcxplemnn0  40219  binomcxplemnotnn0  40226  ltdivgt1  41165  xralrple4  41182  xralrple3  41183  0ellimcdiv  41472  limclner  41474  fprodsubrecnncnvlem  41732  fprodaddrecnncnvlem  41734  dvdivbd  41749  stoweidlem1  41828  stoweidlem3  41830  stoweidlem7  41834  stoweidlem11  41838  stoweidlem14  41841  stoweidlem24  41851  stoweidlem25  41852  stoweidlem26  41853  stoweidlem42  41869  stoweidlem51  41878  stoweidlem59  41886  stoweidlem62  41889  wallispilem4  41895  wallispilem5  41896  wallispi  41897  wallispi2lem1  41898  stirlinglem4  41904  stirlinglem8  41908  stirlinglem12  41912  stirlinglem15  41915  dirkercncflem4  41933  fourierdlem30  41964  fourierdlem73  42006  fourierdlem87  42020  qndenserrnbllem  42121  hoiqssbllem2  42447  dignn0flhalflem2  44157  itsclc0yqsol  44232  amgmwlem  44383  amgmlemALT  44384  amgmw2d  44385  young2d  44386