Theorem rpcnd 9862

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℂcc 7965  ℝ⁺crp 9817

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-resscn 8059

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rab 2497  df-in 3183  df-ss 3190  df-rp 9818

This theorem is referenced by:  rpcnne0d  9870  ltaddrp2d  9895  iccf1o  10168  bcp1nk  10951  bcpasc  10955  cvg1nlemcxze  11459  cvg1nlemres  11462  resqrexlemdec  11488  resqrexlemlo  11490  resqrexlemcalc2  11492  resqrexlemcalc3  11493  resqrexlemnm  11495  resqrexlemcvg  11496  resqrexlemoverl  11498  sqrtdiv  11519  absdivap  11547  bdtrilem  11716  isumrpcl  11971  expcnvap0  11979  absgtap  11987  cvgratz  12009  mertenslemi1  12012  effsumlt  12169  bitsmod  12433  pythagtriplem12  12764  pythagtriplem14  12766  pythagtriplem16  12768  limcimolemlt  15303  rpdivcxp  15550  rpcxple2  15557  rpcxplt2  15558  rpcxpsqrt  15561  rpabscxpbnd  15579  logbgcd1irr  15606  iooref1o  16313  trilpolemclim  16315  trilpolemisumle  16317  trilpolemeq1  16319  trilpolemlt1  16320