Theorem rpcnd 9696

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7808  ℝ⁺crp 9651

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3135  df-ss 3142  df-rp 9652

This theorem is referenced by:  rpcnne0d  9704  ltaddrp2d  9729  iccf1o  10002  bcp1nk  10737  bcpasc  10741  cvg1nlemcxze  10986  cvg1nlemres  10989  resqrexlemdec  11015  resqrexlemlo  11017  resqrexlemcalc2  11019  resqrexlemcalc3  11020  resqrexlemnm  11022  resqrexlemcvg  11023  resqrexlemoverl  11025  sqrtdiv  11046  absdivap  11074  bdtrilem  11242  isumrpcl  11497  expcnvap0  11505  absgtap  11513  cvgratz  11535  mertenslemi1  11538  effsumlt  11695  pythagtriplem12  12269  pythagtriplem14  12271  pythagtriplem16  12273  limcimolemlt  14064  rpdivcxp  14263  rpcxple2  14269  rpcxplt2  14270  rpcxpsqrt  14273  rpabscxpbnd  14290  logbgcd1irr  14316  iooref1o  14702  trilpolemclim  14704  trilpolemisumle  14706  trilpolemeq1  14708  trilpolemlt1  14709