Theorem rpcnd 9700

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 9698	. 2 |- ( ph -> A e. RR )
3	2	recnd 7988	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7811   RR+crp 9655

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 7905

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 3137  df-ss 3144  df-rp 9656

This theorem is referenced by:  rpcnne0d  9708  ltaddrp2d  9733  iccf1o  10006  bcp1nk  10744  bcpasc  10748  cvg1nlemcxze  10993  cvg1nlemres  10996  resqrexlemdec  11022  resqrexlemlo  11024  resqrexlemcalc2  11026  resqrexlemcalc3  11027  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemoverl  11032  sqrtdiv  11053  absdivap  11081  bdtrilem  11249  isumrpcl  11504  expcnvap0  11512  absgtap  11520  cvgratz  11542  mertenslemi1  11545  effsumlt  11702  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  limcimolemlt  14172  rpdivcxp  14371  rpcxple2  14377  rpcxplt2  14378  rpcxpsqrt  14381  rpabscxpbnd  14398  logbgcd1irr  14424  iooref1o  14821  trilpolemclim  14823  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828