Theorem rpcnd 10116

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8183   RR+crp 10071

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233  df-rp 10072

This theorem is used by:  rpcnne0d  10124  ltaddrp2d  10149  iccf1o  10424  bcp1nk  11222  bcpasc  11226  bcm1n  11229  cvg1nlemcxze  11770  cvg1nlemres  11773  resqrexlemdec  11799  resqrexlemlo  11801  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  sqrtdiv  11830  absdivap  11858  bdtrilem  12030  isumrpcl  12286  expcnvap0  12294  absgtap  12302  cvgratz  12324  mertenslemi1  12327  effsumlt  12484  bitsmod  12748  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  limcimolemlt  15890  logfac  16126  rpdivcxp  16144  rpcxple2  16153  rpcxplt2  16154  rpcxpsqrt  16157  rpabscxpbnd  16175  efnthr  16176  logbgcd1irr  16203  bclbnd  16307  bposlem9  16319  iooref1o  17289  trilpolemclim  17292  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297