Theorem rpcnd 9698

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  ℝ⁺crp 9653

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3136  df-ss 3143  df-rp 9654

This theorem is referenced by:  rpcnne0d  9706  ltaddrp2d  9731  iccf1o  10004  bcp1nk  10742  bcpasc  10746  cvg1nlemcxze  10991  cvg1nlemres  10994  resqrexlemdec  11020  resqrexlemlo  11022  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemoverl  11030  sqrtdiv  11051  absdivap  11079  bdtrilem  11247  isumrpcl  11502  expcnvap0  11510  absgtap  11518  cvgratz  11540  mertenslemi1  11543  effsumlt  11700  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  limcimolemlt  14136  rpdivcxp  14335  rpcxple2  14341  rpcxplt2  14342  rpcxpsqrt  14345  rpabscxpbnd  14362  logbgcd1irr  14388  iooref1o  14785  trilpolemclim  14787  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792