Theorem rpcnd 13068

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ℂcc 11104  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11163

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-ss 3921  df-rp 13023

This theorem is used by:  rpcnne0d  13075  ltaddrp2d  13100  prodge0ld  13132  iccf1o  13529  ltexp2r  14216  discr  14283  bcp1nk  14360  bcpasc  14364  01sqrexlem6  15305  sqrtdiv  15323  absdiv  15353  o1rlimmul  15677  isumrpcl  15904  isumltss  15909  expcnv  15925  mertenslem1  15945  bitsmod  16500  nmoi2  24898  reperflem  24987  icopnfcnv  25112  lebnumlem3  25133  nmoleub2lem2  25286  nmoleub3  25289  minveclem3  25599  pjthlem1  25607  ovollb2lem  25658  sca2rab  25682  ovolscalem1  25683  ovolsca  25685  itg2mulc  25917  itg2cnlem2  25932  c1liplem1  26166  lhop1  26184  aalioulem4  26509  aaliou2b  26515  aaliou3lem2  26517  aaliou3lem3  26518  aaliou3lem8  26519  aaliou3lem6  26522  aaliou3lem7  26523  itgulm  26582  dvradcnv  26595  pserdvlem2  26602  abelthlem7  26612  abelthlem8  26613  lognegb  26766  logno1  26812  advlog  26830  advlogexp  26831  cxprec  26862  divcxp  26863  cxpsqrt  26879  dvcxp1  26916  cxpcn3lem  26923  loglesqrt  26937  relogbval  26948  nnlogbexp  26957  logbrec  26958  asinlem3  27047  cxplim  27147  rlimcxp  27149  cxp2limlem  27151  cxp2lim  27152  cxploglim  27153  cxploglim2  27154  divsqrtsumlem  27155  divsqrtsumo1  27159  amgmlem  27165  zetacvg  27190  lgamucov  27213  basellem3  27258  basellem4  27259  basellem8  27263  chpval2  27393  logexprlim  27400  bclbnd  27455  bposlem9  27467  chebbnd1lem3  27646  chebbnd1  27647  chtppilimlem2  27649  chtppilim  27650  chebbnd2  27652  chto1lb  27653  chpchtlim  27654  chpo1ubb  27656  rplogsumlem1  27659  rplogsumlem2  27660  dchrvmasumlem1  27670  dchrvmasum2lem  27671  dchrisum0lema  27689  dchrisum0lem1b  27690  dchrisum0lem1  27691  dchrisum0lem2a  27692  dchrisum0lem2  27693  dchrisum0lem3  27694  dchrisum0  27695  mulogsumlem  27706  mulog2sumlem1  27709  mulog2sumlem2  27710  vmalogdivsum2  27713  log2sumbnd  27719  selberg3lem1  27732  selberg3lem2  27733  selberg4lem1  27735  selberg4  27736  selberg34r  27746  pntrlog2bndlem2  27753  pntrlog2bndlem3  27754  pntrlog2bndlem4  27755  pntrlog2bndlem5  27756  pntpbnd1a  27760  pntpbnd2  27762  pntibndlem1  27764  pntibndlem2  27766  pntlemd  27769  pntlemc  27770  pntlemb  27772  pntlemq  27776  pntlemr  27777  pntlemj  27778  pntlemf  27780  pntlemo  27782  pntlem3  27784  pntleml  27786  pnt  27789  padicabvcxp  27807  ostth2lem4  27811  ostth2  27812  ostth3  27813  smcnlem  31060  blocnilem  31167  ubthlem2  31234  bcm1n  33151  probmeasb  34829  signsply0  34947  iprodgam  36242  faclimlem1  36243  faclimlem3  36245  faclim  36246  iprodfac  36247  knoppndvlem17  37145  mblfinlem3  38338  itg2addnclem3  38352  ftc1cnnclem  38370  geomcau  38438  cntotbnd  38475  heibor1lem  38488  rrndstprj2  38510  rrncmslem  38511  relogbzexpd  42771  lcmineqlem21  42844  aks4d1p1p1  42858  aks4d1p6  42876  2ap1caineq  42940  exp11d  43115  rplog11d  43136  pell1qrgaplem  43628  pellfund14  43653  rmxyneg  43675  rmxy1  43677  rmxy0  43678  jm2.23  43751  proot1ex  43951  amgm2d  44952  amgm3d  44953  amgm4d  44954  cvgdvgrat  45051  binomcxplemnn0  45087  binomcxplemnotnn0  45094  ltdivgt1  46100  xralrple4  46116  xralrple3  46117  0ellimcdiv  46391  limclner  46393  fprodsubrecnncnvlem  46649  fprodaddrecnncnvlem  46651  dvdivbd  46665  stoweidlem1  46743  stoweidlem3  46745  stoweidlem7  46749  stoweidlem11  46753  stoweidlem14  46756  stoweidlem24  46766  stoweidlem25  46767  stoweidlem26  46768  stoweidlem42  46784  stoweidlem51  46793  stoweidlem59  46801  stoweidlem62  46804  wallispilem4  46810  wallispilem5  46811  wallispi  46812  wallispi2lem1  46813  stirlinglem4  46819  stirlinglem8  46823  stirlinglem12  46827  stirlinglem15  46830  dirkercncflem4  46848  fourierdlem30  46879  fourierdlem73  46921  fourierdlem87  46935  qndenserrnbllem  47036  hoiqssbllem2  47365  dignn0flhalflem2  49424  itsclc0yqsol  49572  amgmwlem  50677  amgmlemALT  50678  amgmw2d  50679  young2d  50680