Theorem rpcnd 12957

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11026  ℝ⁺crp 12911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922  df-rp 12912

This theorem is referenced by:  rpcnne0d  12964  ltaddrp2d  12989  prodge0ld  13021  iccf1o  13417  ltexp2r  14098  discr  14165  bcp1nk  14242  bcpasc  14246  01sqrexlem6  15172  sqrtdiv  15190  absdiv  15220  o1rlimmul  15544  isumrpcl  15768  isumltss  15773  expcnv  15789  mertenslem1  15809  bitsmod  16365  nmoi2  24634  reperflem  24723  icchmeoOLD  24855  icopnfcnv  24856  lebnumlem3  24878  nmoleub2lem2  25032  nmoleub3  25035  minveclem3  25345  pjthlem1  25353  ovollb2lem  25405  sca2rab  25429  ovolscalem1  25430  ovolsca  25432  itg2mulc  25664  itg2cnlem2  25679  c1liplem1  25917  lhop1  25935  aalioulem4  26259  aaliou2b  26265  aaliou3lem2  26267  aaliou3lem3  26268  aaliou3lem8  26269  aaliou3lem6  26272  aaliou3lem7  26273  itgulm  26333  dvradcnv  26346  pserdvlem2  26354  abelthlem7  26364  abelthlem8  26365  lognegb  26515  logno1  26561  advlog  26579  advlogexp  26580  cxprec  26611  divcxp  26612  cxpsqrt  26628  dvcxp1  26665  cxpcn3lem  26673  loglesqrt  26687  relogbval  26698  nnlogbexp  26707  logbrec  26708  asinlem3  26797  cxplim  26898  rlimcxp  26900  cxp2limlem  26902  cxp2lim  26903  cxploglim  26904  cxploglim2  26905  divsqrtsumlem  26906  divsqrtsumo1  26910  amgmlem  26916  zetacvg  26941  lgamucov  26964  basellem3  27009  basellem4  27010  chpval2  27145  logexprlim  27152  bclbnd  27207  bposlem9  27219  chebbnd1lem3  27398  chebbnd1  27399  chtppilimlem2  27401  chtppilim  27402  chebbnd2  27404  chto1lb  27405  chpchtlim  27406  chpo1ubb  27408  rplogsumlem1  27411  rplogsumlem2  27412  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrisum0lema  27441  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  dchrisum0  27447  mulogsumlem  27458  mulog2sumlem1  27461  mulog2sumlem2  27462  vmalogdivsum2  27465  log2sumbnd  27471  selberg3lem1  27484  selberg3lem2  27485  selberg4lem1  27487  selberg4  27488  selberg34r  27498  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem1  27516  pntibndlem2  27518  pntlemd  27521  pntlemc  27522  pntlemb  27524  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemf  27532  pntlemo  27534  pntlem3  27536  pntleml  27538  pnt  27541  padicabvcxp  27559  ostth2lem4  27563  ostth2  27564  ostth3  27565  smcnlem  30659  blocnilem  30766  ubthlem2  30833  bcm1n  32751  probmeasb  34397  signsply0  34518  iprodgam  35714  faclimlem1  35715  faclimlem3  35717  faclim  35718  iprodfac  35719  knoppndvlem17  36501  mblfinlem3  37638  itg2addnclem3  37652  ftc1cnnclem  37670  geomcau  37738  cntotbnd  37775  heibor1lem  37788  rrndstprj2  37810  rrncmslem  37811  relogbzexpd  41948  lcmineqlem21  42022  aks4d1p1p1  42036  aks4d1p6  42054  2ap1caineq  42118  exp11d  42299  rplog11d  42320  pell1qrgaplem  42846  pellfund14  42871  rmxyneg  42893  rmxy1  42895  rmxy0  42896  jm2.23  42969  proot1ex  43169  amgm2d  44171  amgm3d  44172  amgm4d  44173  cvgdvgrat  44286  binomcxplemnn0  44322  binomcxplemnotnn0  44329  ltdivgt1  45336  xralrple4  45353  xralrple3  45354  0ellimcdiv  45631  limclner  45633  fprodsubrecnncnvlem  45889  fprodaddrecnncnvlem  45891  dvdivbd  45905  stoweidlem1  45983  stoweidlem3  45985  stoweidlem7  45989  stoweidlem11  45993  stoweidlem14  45996  stoweidlem24  46006  stoweidlem25  46007  stoweidlem26  46008  stoweidlem42  46024  stoweidlem51  46033  stoweidlem59  46041  stoweidlem62  46044  wallispilem4  46050  wallispilem5  46051  wallispi  46052  wallispi2lem1  46053  stirlinglem4  46059  stirlinglem8  46063  stirlinglem12  46067  stirlinglem15  46070  dirkercncflem4  46088  fourierdlem30  46119  fourierdlem73  46161  fourierdlem87  46175  qndenserrnbllem  46276  hoiqssbllem2  46605  dignn0flhalflem2  48589  itsclc0yqsol  48737  amgmwlem  49775  amgmlemALT  49776  amgmw2d  49777  young2d  49778