Theorem rpcnd 9855

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

Syntax hints:   → wi 4   ∈ wcel 2178  ℂcc 7958  ℝ⁺crp 9810

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 2189  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-in 3180  df-ss 3187  df-rp 9811

This theorem is referenced by:  rpcnne0d  9863  ltaddrp2d  9888  iccf1o  10161  bcp1nk  10944  bcpasc  10948  cvg1nlemcxze  11408  cvg1nlemres  11411  resqrexlemdec  11437  resqrexlemlo  11439  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemoverl  11447  sqrtdiv  11468  absdivap  11496  bdtrilem  11665  isumrpcl  11920  expcnvap0  11928  absgtap  11936  cvgratz  11958  mertenslemi1  11961  effsumlt  12118  bitsmod  12382  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  limcimolemlt  15251  rpdivcxp  15498  rpcxple2  15505  rpcxplt2  15506  rpcxpsqrt  15509  rpabscxpbnd  15527  logbgcd1irr  15554  iooref1o  16175  trilpolemclim  16177  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182