Theorem rpcnd 12434

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3943  df-ss 3952  df-rp 12391

This theorem is referenced by:  rpcnne0d  12441  ltaddrp2d  12466  prodge0ld  12498  iccf1o  12883  ltexp2r  13538  discr  13602  bcp1nk  13678  bcpasc  13682  sqrlem6  14607  sqrtdiv  14625  absdiv  14655  o1rlimmul  14975  isumrpcl  15198  isumltss  15203  expcnv  15219  mertenslem1  15240  bitsmod  15785  nmoi2  23339  reperflem  23426  icchmeo  23545  icopnfcnv  23546  lebnumlem3  23567  nmoleub2lem2  23720  nmoleub3  23723  minveclem3  24032  pjthlem1  24040  ovollb2lem  24089  sca2rab  24113  ovolscalem1  24114  ovolsca  24116  itg2mulc  24348  itg2cnlem2  24363  c1liplem1  24593  lhop1  24611  aalioulem4  24924  aaliou2b  24930  aaliou3lem2  24932  aaliou3lem3  24933  aaliou3lem8  24934  aaliou3lem6  24937  aaliou3lem7  24938  itgulm  24996  dvradcnv  25009  pserdvlem2  25016  abelthlem7  25026  abelthlem8  25027  lognegb  25173  logno1  25219  advlog  25237  advlogexp  25238  cxprec  25269  divcxp  25270  cxpsqrt  25286  dvcxp1  25321  cxpcn3lem  25328  loglesqrt  25339  relogbval  25350  nnlogbexp  25359  logbrec  25360  asinlem3  25449  cxplim  25549  rlimcxp  25551  cxp2limlem  25553  cxp2lim  25554  cxploglim  25555  cxploglim2  25556  divsqrtsumlem  25557  divsqrtsumo1  25561  amgmlem  25567  zetacvg  25592  lgamucov  25615  basellem3  25660  basellem4  25661  chpval2  25794  logexprlim  25801  bclbnd  25856  bposlem9  25868  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem2  26050  chtppilim  26051  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ubb  26057  rplogsumlem1  26060  rplogsumlem2  26061  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  dchrisum0  26096  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  vmalogdivsum2  26114  log2sumbnd  26120  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  selberg4  26137  selberg34r  26147  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem1  26165  pntibndlem2  26167  pntlemd  26170  pntlemc  26171  pntlemb  26173  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemo  26183  pntlem3  26185  pntleml  26187  pnt  26190  padicabvcxp  26208  ostth2lem4  26212  ostth2  26213  ostth3  26214  smcnlem  28474  blocnilem  28581  ubthlem2  28648  bcm1n  30518  probmeasb  31688  signsply0  31821  iprodgam  32974  faclimlem1  32975  faclimlem3  32977  faclim  32978  iprodfac  32979  knoppndvlem17  33867  mblfinlem3  34946  itg2addnclem3  34960  ftc1cnnclem  34980  geomcau  35049  cntotbnd  35089  heibor1lem  35102  rrndstprj2  35124  rrncmslem  35125  cxpgt0d  39229  exp11d  39238  pell1qrgaplem  39519  pellfund14  39544  rmxyneg  39566  rmxy1  39568  rmxy0  39569  jm2.23  39642  proot1ex  39850  amgm2d  40600  amgm3d  40601  amgm4d  40602  cvgdvgrat  40694  binomcxplemnn0  40730  binomcxplemnotnn0  40737  ltdivgt1  41673  xralrple4  41690  xralrple3  41691  0ellimcdiv  41979  limclner  41981  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  dvdivbd  42257  stoweidlem1  42335  stoweidlem3  42337  stoweidlem7  42341  stoweidlem11  42345  stoweidlem14  42348  stoweidlem24  42358  stoweidlem25  42359  stoweidlem26  42360  stoweidlem42  42376  stoweidlem51  42385  stoweidlem59  42393  stoweidlem62  42396  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  stirlinglem4  42411  stirlinglem8  42415  stirlinglem12  42419  stirlinglem15  42422  dirkercncflem4  42440  fourierdlem30  42471  fourierdlem73  42513  fourierdlem87  42527  qndenserrnbllem  42628  hoiqssbllem2  42954  dignn0flhalflem2  44725  itsclc0yqsol  44800  amgmwlem  44952  amgmlemALT  44953  amgmw2d  44954  young2d  44955