Theorem rpcnd 13136

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11170  ℝ⁺crp 13090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11229

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3915  df-rp 13091

This theorem is used by:  rpcnne0d  13143  ltaddrp2d  13168  prodge0ld  13200  iccf1o  13597  ltexp2r  14285  discr  14352  bcp1nk  14429  bcpasc  14433  01sqrexlem6  15382  sqrtdiv  15400  absdiv  15430  o1rlimmul  15754  isumrpcl  15980  isumltss  15985  expcnv  16001  mertenslem1  16021  bitsmod  16574  nmoi2  25011  reperflem  25100  icopnfcnv  25225  lebnumlem3  25246  nmoleub2lem2  25399  nmoleub3  25402  minveclem3  25712  pjthlem1  25720  ovollb2lem  25771  sca2rab  25795  ovolscalem1  25796  ovolsca  25798  itg2mulc  26030  itg2cnlem2  26045  c1liplem1  26278  lhop1  26296  aalioulem4  26626  aaliou2b  26632  aaliou3lem2  26634  aaliou3lem3  26635  aaliou3lem8  26636  aaliou3lem6  26639  aaliou3lem7  26640  itgulm  26699  dvradcnv  26712  pserdvlem2  26719  abelthlem7  26729  abelthlem8  26730  lognegb  26882  logno1  26928  advlog  26946  advlogexp  26947  cxprec  26978  divcxp  26979  cxpsqrt  26995  dvcxp1  27032  cxpcn3lem  27039  loglesqrt  27053  relogbval  27064  nnlogbexp  27073  logbrec  27074  asinlem3  27163  cxplim  27263  rlimcxp  27265  cxp2limlem  27267  cxp2lim  27268  cxploglim  27269  cxploglim2  27270  divsqrtsumlem  27271  divsqrtsumo1  27275  amgmlem  27281  zetacvg  27306  lgamucov  27329  basellem3  27374  basellem4  27375  basellem8  27379  chpval2  27509  logexprlim  27516  bclbnd  27571  bposlem9  27583  chebbnd1lem3  27762  chebbnd1  27763  chtppilimlem2  27765  chtppilim  27766  chebbnd2  27768  chto1lb  27769  chpchtlim  27770  chpo1ubb  27772  rplogsumlem1  27775  rplogsumlem2  27776  dchrvmasumlem1  27786  dchrvmasum2lem  27787  dchrisum0lema  27805  dchrisum0lem1b  27806  dchrisum0lem1  27807  dchrisum0lem2a  27808  dchrisum0lem2  27809  dchrisum0lem3  27810  dchrisum0  27811  mulogsumlem  27822  mulog2sumlem1  27825  mulog2sumlem2  27826  vmalogdivsum2  27829  log2sumbnd  27835  selberg3lem1  27848  selberg3lem2  27849  selberg4lem1  27851  selberg4  27852  selberg34r  27862  pntrlog2bndlem2  27869  pntrlog2bndlem3  27870  pntrlog2bndlem4  27871  pntrlog2bndlem5  27872  pntpbnd1a  27876  pntpbnd2  27878  pntibndlem1  27880  pntibndlem2  27882  pntlemd  27885  pntlemc  27886  pntlemb  27888  pntlemq  27892  pntlemr  27893  pntlemj  27894  pntlemf  27896  pntlemo  27898  pntlem3  27900  pntleml  27902  pnt  27905  padicabvcxp  27923  ostth2lem4  27927  ostth2  27928  ostth3  27929  smcnlem  31233  blocnilem  31340  ubthlem2  31407  bcm1n  33321  probmeasb  34997  signsply0  35115  iprodgam  36428  faclimlem1  36429  faclimlem3  36431  faclim  36432  iprodfac  36433  knoppndvlem17  37316  mblfinlem3  38497  itg2addnclem3  38511  ftc1cnnclem  38529  geomcau  38613  cntotbnd  38650  heibor1lem  38663  rrndstprj2  38685  rrncmslem  38686  relogbzexpd  42946  lcmineqlem21  43019  aks4d1p1p1  43033  aks4d1p6  43051  2ap1caineq  43115  exp11d  43305  rplog11d  43326  pell1qrgaplem  43818  pellfund14  43843  rmxyneg  43865  rmxy1  43867  rmxy0  43868  jm2.23  43941  proot1ex  44141  amgm2d  45142  amgm3d  45143  amgm4d  45144  cvgdvgrat  45241  binomcxplemnn0  45277  binomcxplemnotnn0  45284  ltdivgt1  46290  xralrple4  46306  xralrple3  46307  0ellimcdiv  46581  limclner  46583  fprodsubrecnncnvlem  46839  fprodaddrecnncnvlem  46841  dvdivbd  46855  stoweidlem1  46933  stoweidlem3  46935  stoweidlem7  46939  stoweidlem11  46943  stoweidlem14  46946  stoweidlem24  46956  stoweidlem25  46957  stoweidlem26  46958  stoweidlem42  46974  stoweidlem51  46983  stoweidlem59  46991  stoweidlem62  46994  wallispilem4  47000  wallispilem5  47001  wallispi  47002  wallispi2lem1  47003  stirlinglem4  47009  stirlinglem8  47013  stirlinglem12  47017  stirlinglem15  47020  dirkercncflem4  47038  fourierdlem30  47069  fourierdlem73  47111  fourierdlem87  47125  qndenserrnbllem  47226  hoiqssbllem2  47555  dignn0flhalflem2  49650  itsclc0yqsol  49798  amgmwlem  50909  amgmlemALT  50910  amgmw2d  50911  young2d  50912