Theorem rpcnd 9692

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7804   RR+crp 9647

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 7898

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 3135  df-ss 3142  df-rp 9648

This theorem is referenced by:  rpcnne0d  9700  ltaddrp2d  9725  iccf1o  9998  bcp1nk  10733  bcpasc  10737  cvg1nlemcxze  10982  cvg1nlemres  10985  resqrexlemdec  11011  resqrexlemlo  11013  resqrexlemcalc2  11015  resqrexlemcalc3  11016  resqrexlemnm  11018  resqrexlemcvg  11019  resqrexlemoverl  11021  sqrtdiv  11042  absdivap  11070  bdtrilem  11238  isumrpcl  11493  expcnvap0  11501  absgtap  11509  cvgratz  11531  mertenslemi1  11534  effsumlt  11691  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  limcimolemlt  13915  rpdivcxp  14114  rpcxple2  14120  rpcxplt2  14121  rpcxpsqrt  14124  rpabscxpbnd  14141  logbgcd1irr  14167  iooref1o  14553  trilpolemclim  14555  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560