Theorem rpcnd 9630

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7747  ℝ⁺crp 9585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rab 2452  df-in 3121  df-ss 3128  df-rp 9586

This theorem is referenced by:  rpcnne0d  9638  ltaddrp2d  9663  iccf1o  9936  bcp1nk  10671  bcpasc  10675  cvg1nlemcxze  10920  cvg1nlemres  10923  resqrexlemdec  10949  resqrexlemlo  10951  resqrexlemcalc2  10953  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemoverl  10959  sqrtdiv  10980  absdivap  11008  bdtrilem  11176  isumrpcl  11431  expcnvap0  11439  absgtap  11447  cvgratz  11469  mertenslemi1  11472  effsumlt  11629  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  limcimolemlt  13233  rpdivcxp  13432  rpcxple2  13438  rpcxplt2  13439  rpcxpsqrt  13442  rpabscxpbnd  13459  logbgcd1irr  13485  iooref1o  13873  trilpolemclim  13875  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880