Theorem rpcnd 9827

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7930  ℝ⁺crp 9782

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8024

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-in 3173  df-ss 3180  df-rp 9783

This theorem is referenced by:  rpcnne0d  9835  ltaddrp2d  9860  iccf1o  10133  bcp1nk  10914  bcpasc  10918  cvg1nlemcxze  11337  cvg1nlemres  11340  resqrexlemdec  11366  resqrexlemlo  11368  resqrexlemcalc2  11370  resqrexlemcalc3  11371  resqrexlemnm  11373  resqrexlemcvg  11374  resqrexlemoverl  11376  sqrtdiv  11397  absdivap  11425  bdtrilem  11594  isumrpcl  11849  expcnvap0  11857  absgtap  11865  cvgratz  11887  mertenslemi1  11890  effsumlt  12047  bitsmod  12311  pythagtriplem12  12642  pythagtriplem14  12644  pythagtriplem16  12646  limcimolemlt  15180  rpdivcxp  15427  rpcxple2  15434  rpcxplt2  15435  rpcxpsqrt  15438  rpabscxpbnd  15456  logbgcd1irr  15483  iooref1o  16047  trilpolemclim  16049  trilpolemisumle  16051  trilpolemeq1  16053  trilpolemlt1  16054