Theorem rpcnd 10110

Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem rpcnd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 10108	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8355	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8178  ℝ⁺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  16092  rpdivcxp  16110  rpcxple2  16119  rpcxplt2  16120  rpcxpsqrt  16123  rpabscxpbnd  16141  efnthr  16142  logbgcd1irr  16169  bclbnd  16273  bposlem9  16285  iooref1o  17254  trilpolemclim  17257  trilpolemisumle  17259  trilpolemeq1  17261  trilpolemlt1  17262