Theorem rpcnd 10117

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8184  ℝ⁺crp 10072

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8278

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233  df-rp 10073

This theorem is used by:  rpcnne0d  10125  ltaddrp2d  10150  iccf1o  10425  bcp1nk  11223  bcpasc  11227  bcm1n  11230  cvg1nlemcxze  11771  cvg1nlemres  11774  resqrexlemdec  11800  resqrexlemlo  11802  resqrexlemcalc2  11804  resqrexlemcalc3  11805  resqrexlemnm  11807  resqrexlemcvg  11808  resqrexlemoverl  11810  sqrtdiv  11831  absdivap  11859  bdtrilem  12031  isumrpcl  12287  expcnvap0  12295  absgtap  12303  cvgratz  12325  mertenslemi1  12328  effsumlt  12485  bitsmod  12749  pythagtriplem12  13084  pythagtriplem14  13086  pythagtriplem16  13088  limcimolemlt  15902  logfac  16138  rpdivcxp  16156  rpcxple2  16165  rpcxplt2  16166  rpcxpsqrt  16169  rpabscxpbnd  16187  efnthr  16188  logbgcd1irr  16215  bclbnd  16319  bposlem9  16331  iooref1o  17301  trilpolemclim  17304  trilpolemisumle  17306  trilpolemeq1  17308  trilpolemlt1  17309