Theorem rpcnd 9938

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℂcc 8035  ℝ⁺crp 9893

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 2212  ax-resscn 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rab 2518  df-in 3205  df-ss 3212  df-rp 9894

This theorem is referenced by:  rpcnne0d  9946  ltaddrp2d  9971  iccf1o  10244  bcp1nk  11030  bcpasc  11034  cvg1nlemcxze  11565  cvg1nlemres  11568  resqrexlemdec  11594  resqrexlemlo  11596  resqrexlemcalc2  11598  resqrexlemcalc3  11599  resqrexlemnm  11601  resqrexlemcvg  11602  resqrexlemoverl  11604  sqrtdiv  11625  absdivap  11653  bdtrilem  11822  isumrpcl  12078  expcnvap0  12086  absgtap  12094  cvgratz  12116  mertenslemi1  12119  effsumlt  12276  bitsmod  12540  pythagtriplem12  12871  pythagtriplem14  12873  pythagtriplem16  12875  limcimolemlt  15417  rpdivcxp  15664  rpcxple2  15671  rpcxplt2  15672  rpcxpsqrt  15675  rpabscxpbnd  15693  logbgcd1irr  15720  iooref1o  16705  trilpolemclim  16707  trilpolemisumle  16709  trilpolemeq1  16711  trilpolemlt1  16712