Theorem rpcnd 9933

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   RR+crp 9888

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 8124

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 9889

This theorem is referenced by:  rpcnne0d  9941  ltaddrp2d  9966  iccf1o  10239  bcp1nk  11025  bcpasc  11029  cvg1nlemcxze  11560  cvg1nlemres  11563  resqrexlemdec  11589  resqrexlemlo  11591  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemoverl  11599  sqrtdiv  11620  absdivap  11648  bdtrilem  11817  isumrpcl  12073  expcnvap0  12081  absgtap  12089  cvgratz  12111  mertenslemi1  12114  effsumlt  12271  bitsmod  12535  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  limcimolemlt  15407  rpdivcxp  15654  rpcxple2  15661  rpcxplt2  15662  rpcxpsqrt  15665  rpabscxpbnd  15683  logbgcd1irr  15710  iooref1o  16689  trilpolemclim  16691  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696