Theorem rpcnd 10052

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  ℝ⁺crp 10007

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3220  df-ss 3227  df-rp 10008

This theorem is referenced by:  rpcnne0d  10060  ltaddrp2d  10085  iccf1o  10360  bcp1nk  11152  bcpasc  11156  bcm1n  11159  cvg1nlemcxze  11695  cvg1nlemres  11698  resqrexlemdec  11724  resqrexlemlo  11726  resqrexlemcalc2  11728  resqrexlemcalc3  11729  resqrexlemnm  11731  resqrexlemcvg  11732  resqrexlemoverl  11734  sqrtdiv  11755  absdivap  11783  bdtrilem  11952  isumrpcl  12208  expcnvap0  12216  absgtap  12224  cvgratz  12246  mertenslemi1  12249  effsumlt  12406  bitsmod  12670  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem16  13005  limcimolemlt  15658  rpdivcxp  15905  rpcxple2  15912  rpcxplt2  15913  rpcxpsqrt  15916  rpabscxpbnd  15934  logbgcd1irr  15961  iooref1o  16957  trilpolemclim  16959  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964