Theorem rpcnd 8775

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℝ⁺crp 8734

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rab 2357  df-in 2979  df-ss 2986  df-rp 8735

This theorem is referenced by:  rpcnne0d  8783  ltaddrp2d  8808  iccf1o  9026  bcp1nk  9689  bcpasc  9693  cvg1nlemcxze  9868  cvg1nlemres  9871  resqrexlemdec  9897  resqrexlemlo  9899  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  sqrtdiv  9928  absdivap  9956