Theorem rpcnd 9932

Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpcnd	|- ( ph -> A e. CC )

Proof of Theorem rpcnd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 9930	. 2 |- ( ph -> A e. RR )
3	2	recnd 8207	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8029   RR+crp 9887

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 2213  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213  df-rp 9888

This theorem is referenced by:  rpcnne0d  9940  ltaddrp2d  9965  iccf1o  10238  bcp1nk  11023  bcpasc  11027  cvg1nlemcxze  11542  cvg1nlemres  11545  resqrexlemdec  11571  resqrexlemlo  11573  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemoverl  11581  sqrtdiv  11602  absdivap  11630  bdtrilem  11799  isumrpcl  12054  expcnvap0  12062  absgtap  12070  cvgratz  12092  mertenslemi1  12095  effsumlt  12252  bitsmod  12516  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  limcimolemlt  15387  rpdivcxp  15634  rpcxple2  15641  rpcxplt2  15642  rpcxpsqrt  15645  rpabscxpbnd  15663  logbgcd1irr  15690  iooref1o  16638  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645