Theorem rpcnd 10115

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 10113	. 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 10070

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 10071

This theorem is used by:  rpcnne0d  10123  ltaddrp2d  10148  iccf1o  10423  bcp1nk  11221  bcpasc  11225  bcm1n  11228  cvg1nlemcxze  11769  cvg1nlemres  11772  resqrexlemdec  11798  resqrexlemlo  11800  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemoverl  11808  sqrtdiv  11829  absdivap  11857  bdtrilem  12029  isumrpcl  12285  expcnvap0  12293  absgtap  12301  cvgratz  12323  mertenslemi1  12326  effsumlt  12483  bitsmod  12747  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  limcimolemlt  15907  logfac  16143  rpdivcxp  16161  rpcxple2  16170  rpcxplt2  16171  rpcxpsqrt  16174  rpabscxpbnd  16192  efnthr  16193  logbgcd1irr  16220  bclbnd  16324  bposlem9  16336  iooref1o  17306  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314