Theorem rpcnd 9485

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  ℝ⁺crp 9441

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7712

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-in 3077  df-ss 3084  df-rp 9442

This theorem is referenced by:  rpcnne0d  9493  ltaddrp2d  9518  iccf1o  9787  bcp1nk  10508  bcpasc  10512  cvg1nlemcxze  10754  cvg1nlemres  10757  resqrexlemdec  10783  resqrexlemlo  10785  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemoverl  10793  sqrtdiv  10814  absdivap  10842  bdtrilem  11010  isumrpcl  11263  expcnvap0  11271  absgtap  11279  cvgratz  11301  mertenslemi1  11304  effsumlt  11398  limcimolemlt  12802  trilpolemclim  13229  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234