Theorem rpcnd 9911

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8013  ℝ⁺crp 9866

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210  df-rp 9867

This theorem is referenced by:  rpcnne0d  9919  ltaddrp2d  9944  iccf1o  10217  bcp1nk  11001  bcpasc  11005  cvg1nlemcxze  11514  cvg1nlemres  11517  resqrexlemdec  11543  resqrexlemlo  11545  resqrexlemcalc2  11547  resqrexlemcalc3  11548  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemoverl  11553  sqrtdiv  11574  absdivap  11602  bdtrilem  11771  isumrpcl  12026  expcnvap0  12034  absgtap  12042  cvgratz  12064  mertenslemi1  12067  effsumlt  12224  bitsmod  12488  pythagtriplem12  12819  pythagtriplem14  12821  pythagtriplem16  12823  limcimolemlt  15359  rpdivcxp  15606  rpcxple2  15613  rpcxplt2  15614  rpcxpsqrt  15617  rpabscxpbnd  15635  logbgcd1irr  15662  iooref1o  16516  trilpolemclim  16518  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523