Theorem rpcnd 10110

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

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

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 8272

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 10066

This theorem is used by:  rpcnne0d  10118  ltaddrp2d  10143  iccf1o  10418  bcp1nk  11216  bcpasc  11220  bcm1n  11223  cvg1nlemcxze  11764  cvg1nlemres  11767  resqrexlemdec  11793  resqrexlemlo  11795  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemoverl  11803  sqrtdiv  11824  absdivap  11852  bdtrilem  12024  isumrpcl  12280  expcnvap0  12288  absgtap  12296  cvgratz  12318  mertenslemi1  12321  effsumlt  12478  bitsmod  12742  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  limcimolemlt  15856  logfac  16090  rpdivcxp  16108  rpcxple2  16115  rpcxplt2  16116  rpcxpsqrt  16119  rpabscxpbnd  16137  logbgcd1irr  16164  bclbnd  16268  bposlem9  16280  iooref1o  17249  trilpolemclim  17252  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257