Theorem rpcnd 9926

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8023  ℝ⁺crp 9881

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 8117

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 3204  df-ss 3211  df-rp 9882

This theorem is referenced by:  rpcnne0d  9934  ltaddrp2d  9959  iccf1o  10232  bcp1nk  11017  bcpasc  11021  cvg1nlemcxze  11536  cvg1nlemres  11539  resqrexlemdec  11565  resqrexlemlo  11567  resqrexlemcalc2  11569  resqrexlemcalc3  11570  resqrexlemnm  11572  resqrexlemcvg  11573  resqrexlemoverl  11575  sqrtdiv  11596  absdivap  11624  bdtrilem  11793  isumrpcl  12048  expcnvap0  12056  absgtap  12064  cvgratz  12086  mertenslemi1  12089  effsumlt  12246  bitsmod  12510  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem16  12845  limcimolemlt  15381  rpdivcxp  15628  rpcxple2  15635  rpcxplt2  15636  rpcxpsqrt  15639  rpabscxpbnd  15657  logbgcd1irr  15684  iooref1o  16588  trilpolemclim  16590  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595