Theorem rpcnd 10082

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8171  ℝ⁺crp 10037

This theorem was proved from 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 8265

This theorem 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 10038

This theorem is referenced by:  rpcnne0d  10090  ltaddrp2d  10115  iccf1o  10390  bcp1nk  11183  bcpasc  11187  bcm1n  11190  cvg1nlemcxze  11731  cvg1nlemres  11734  resqrexlemdec  11760  resqrexlemlo  11762  resqrexlemcalc2  11764  resqrexlemcalc3  11765  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemoverl  11770  sqrtdiv  11791  absdivap  11819  bdtrilem  11988  isumrpcl  12244  expcnvap0  12252  absgtap  12260  cvgratz  12282  mertenslemi1  12285  effsumlt  12442  bitsmod  12706  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem16  13041  limcimolemlt  15748  logfac  15978  rpdivcxp  15996  rpcxple2  16003  rpcxplt2  16004  rpcxpsqrt  16007  rpabscxpbnd  16025  logbgcd1irr  16052  iooref1o  17057  trilpolemclim  17059  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064