Theorem rpcnd 11750

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11709

This theorem is referenced by:  rpcnne0d  11757  ltaddrp2d  11782  iccf1o  12187  ltexp2r  12779  discr  12863  bcp1nk  12966  bcpasc  12970  sqrlem6  13836  sqrtdiv  13854  absdiv  13883  o1rlimmul  14197  isumrpcl  14414  isumltss  14419  expcnv  14435  mertenslem1  14455  bitsmod  14996  nmoi2  22344  reperflem  22429  icchmeo  22548  icopnfcnv  22549  lebnumlem3  22570  nmoleub2lem2  22724  nmoleub3  22727  minveclem3  23008  pjthlem1  23016  ovollb2lem  23063  sca2rab  23087  ovolscalem1  23088  ovolsca  23090  itg2mulc  23320  itg2cnlem2  23335  c1liplem1  23563  lhop1  23581  aalioulem4  23894  aaliou2b  23900  aaliou3lem2  23902  aaliou3lem3  23903  aaliou3lem8  23904  aaliou3lem6  23907  aaliou3lem7  23908  itgulm  23966  dvradcnv  23979  pserdvlem2  23986  abelthlem7  23996  abelthlem8  23997  lognegb  24140  logno1  24182  advlog  24200  advlogexp  24201  cxprec  24232  divcxp  24233  cxpsqrt  24249  dvcxp1  24281  cxpcn3lem  24288  loglesqrt  24299  relogbval  24310  nnlogbexp  24319  logbrec  24320  asinlem3  24398  cxplim  24498  rlimcxp  24500  cxp2limlem  24502  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  divsqrtsumlem  24506  divsqrtsumo1  24510  amgmlem  24516  zetacvg  24541  lgamucov  24564  basellem3  24609  basellem4  24610  chpval2  24743  logexprlim  24750  bclbnd  24805  bposlem9  24817  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem2  24963  chtppilim  24964  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ubb  24970  rplogsumlem1  24973  rplogsumlem2  24974  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  vmalogdivsum2  25027  log2sumbnd  25033  selberg3lem1  25046  selberg3lem2  25047  selberg4lem1  25049  selberg4  25050  selberg34r  25060  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem1  25078  pntibndlem2  25080  pntlemd  25083  pntlemc  25084  pntlemb  25086  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemo  25096  pntlem3  25098  pntleml  25100  pnt  25103  padicabvcxp  25121  ostth2lem4  25125  ostth2  25126  ostth3  25127  smcnlem  26936  blocnilem  27043  ubthlem2  27111  bcm1n  28941  probmeasb  29819  signsply0  29954  iprodgam  30881  faclimlem1  30882  faclimlem3  30884  faclim  30885  iprodfac  30886  knoppndvlem17  31689  mblfinlem3  32618  itg2addnclem3  32633  ftc1cnnclem  32653  geomcau  32725  cntotbnd  32765  heibor1lem  32778  rrndstprj2  32800  rrncmslem  32801  pell1qrgaplem  36455  pellfund14  36480  rmxyneg  36503  rmxy1  36505  rmxy0  36506  jm2.23  36581  proot1ex  36798  amgm2d  37523  amgm3d  37524  amgm4d  37525  cvgdvgrat  37534  binomcxplemnn0  37570  binomcxplemnotnn0  37577  ltdivgt1  38513  xralrple4  38530  xralrple3  38531  0ellimcdiv  38716  limclner  38718  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvdivbd  38813  stoweidlem1  38894  stoweidlem3  38896  stoweidlem7  38900  stoweidlem11  38904  stoweidlem14  38907  stoweidlem24  38917  stoweidlem25  38918  stoweidlem26  38919  stoweidlem42  38935  stoweidlem51  38944  stoweidlem59  38952  stoweidlem62  38955  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  stirlinglem4  38970  stirlinglem8  38974  stirlinglem12  38978  stirlinglem15  38981  dirkercncflem4  38999  fourierdlem30  39030  fourierdlem73  39072  fourierdlem87  39086  qndenserrnbllem  39190  hoiqssbllem2  39513  dignn0flhalflem2  42208  amgmwlem  42357  amgmlemALT  42358  amgmw2d  42359  young2d  42360