Theorem rpcnd 9902

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8005  ℝ⁺crp 9857

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 8099

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 9858

This theorem is referenced by:  rpcnne0d  9910  ltaddrp2d  9935  iccf1o  10208  bcp1nk  10992  bcpasc  10996  cvg1nlemcxze  11501  cvg1nlemres  11504  resqrexlemdec  11530  resqrexlemlo  11532  resqrexlemcalc2  11534  resqrexlemcalc3  11535  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemoverl  11540  sqrtdiv  11561  absdivap  11589  bdtrilem  11758  isumrpcl  12013  expcnvap0  12021  absgtap  12029  cvgratz  12051  mertenslemi1  12054  effsumlt  12211  bitsmod  12475  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem16  12810  limcimolemlt  15346  rpdivcxp  15593  rpcxple2  15600  rpcxplt2  15601  rpcxpsqrt  15604  rpabscxpbnd  15622  logbgcd1irr  15649  iooref1o  16432  trilpolemclim  16434  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439