Theorem rpcnd 9933

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℝ⁺crp 9888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213  df-rp 9889

This theorem is referenced by:  rpcnne0d  9941  ltaddrp2d  9966  iccf1o  10239  bcp1nk  11025  bcpasc  11029  cvg1nlemcxze  11544  cvg1nlemres  11547  resqrexlemdec  11573  resqrexlemlo  11575  resqrexlemcalc2  11577  resqrexlemcalc3  11578  resqrexlemnm  11580  resqrexlemcvg  11581  resqrexlemoverl  11583  sqrtdiv  11604  absdivap  11632  bdtrilem  11801  isumrpcl  12057  expcnvap0  12065  absgtap  12073  cvgratz  12095  mertenslemi1  12098  effsumlt  12255  bitsmod  12519  pythagtriplem12  12850  pythagtriplem14  12852  pythagtriplem16  12854  limcimolemlt  15391  rpdivcxp  15638  rpcxple2  15645  rpcxplt2  15646  rpcxpsqrt  15649  rpabscxpbnd  15667  logbgcd1irr  15694  iooref1o  16659  trilpolemclim  16661  trilpolemisumle  16663  trilpolemeq1  16665  trilpolemlt1  16666