Theorem rpcnd 9819

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

Syntax hints:   -> wi 4   e. wcel 2175   CCcc 7922   RR+crp 9774

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-in 3171  df-ss 3178  df-rp 9775

This theorem is referenced by:  rpcnne0d  9827  ltaddrp2d  9852  iccf1o  10125  bcp1nk  10905  bcpasc  10909  cvg1nlemcxze  11235  cvg1nlemres  11238  resqrexlemdec  11264  resqrexlemlo  11266  resqrexlemcalc2  11268  resqrexlemcalc3  11269  resqrexlemnm  11271  resqrexlemcvg  11272  resqrexlemoverl  11274  sqrtdiv  11295  absdivap  11323  bdtrilem  11492  isumrpcl  11747  expcnvap0  11755  absgtap  11763  cvgratz  11785  mertenslemi1  11788  effsumlt  11945  bitsmod  12209  pythagtriplem12  12540  pythagtriplem14  12542  pythagtriplem16  12544  limcimolemlt  15078  rpdivcxp  15325  rpcxple2  15332  rpcxplt2  15333  rpcxpsqrt  15336  rpabscxpbnd  15354  logbgcd1irr  15381  iooref1o  15906  trilpolemclim  15908  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913