Theorem rpcnd 10037

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8130  ℝ⁺crp 9992

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3219  df-ss 3226  df-rp 9993

This theorem is referenced by:  rpcnne0d  10045  ltaddrp2d  10070  iccf1o  10344  bcp1nk  11132  bcpasc  11136  bcm1n  11139  cvg1nlemcxze  11675  cvg1nlemres  11678  resqrexlemdec  11704  resqrexlemlo  11706  resqrexlemcalc2  11708  resqrexlemcalc3  11709  resqrexlemnm  11711  resqrexlemcvg  11712  resqrexlemoverl  11714  sqrtdiv  11735  absdivap  11763  bdtrilem  11932  isumrpcl  12188  expcnvap0  12196  absgtap  12204  cvgratz  12226  mertenslemi1  12229  effsumlt  12386  bitsmod  12650  pythagtriplem12  12981  pythagtriplem14  12983  pythagtriplem16  12985  limcimolemlt  15578  rpdivcxp  15825  rpcxple2  15832  rpcxplt2  15833  rpcxpsqrt  15836  rpabscxpbnd  15854  logbgcd1irr  15881  iooref1o  16867  trilpolemclim  16869  trilpolemisumle  16871  trilpolemeq1  16873  trilpolemlt1  16874