ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rpcnd GIF version

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
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 9694 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 7984 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator