Theorem rpcnd 10101

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 10099	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8354	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8177  ℝ⁺crp 10056

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 8271

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 10057

This theorem is used by:  rpcnne0d  10109  ltaddrp2d  10134  iccf1o  10409  bcp1nk  11202  bcpasc  11206  bcm1n  11209  cvg1nlemcxze  11750  cvg1nlemres  11753  resqrexlemdec  11779  resqrexlemlo  11781  resqrexlemcalc2  11783  resqrexlemcalc3  11784  resqrexlemnm  11786  resqrexlemcvg  11787  resqrexlemoverl  11789  sqrtdiv  11810  absdivap  11838  bdtrilem  12007  isumrpcl  12263  expcnvap0  12271  absgtap  12279  cvgratz  12301  mertenslemi1  12304  effsumlt  12461  bitsmod  12725  pythagtriplem12  13056  pythagtriplem14  13058  pythagtriplem16  13060  limcimolemlt  15767  logfac  16001  rpdivcxp  16019  rpcxple2  16026  rpcxplt2  16027  rpcxpsqrt  16030  rpabscxpbnd  16048  logbgcd1irr  16075  bclbnd  16127  iooref1o  17095  trilpolemclim  17097  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102