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

Theorem rpcnd 9453
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 9451 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 7762 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  cc 7586  +crp 9409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-resscn 7680
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rab 2402  df-in 3047  df-ss 3054  df-rp 9410
This theorem is referenced by:  rpcnne0d  9461  ltaddrp2d  9486  iccf1o  9755  bcp1nk  10476  bcpasc  10480  cvg1nlemcxze  10722  cvg1nlemres  10725  resqrexlemdec  10751  resqrexlemlo  10753  resqrexlemcalc2  10755  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemcvg  10759  resqrexlemoverl  10761  sqrtdiv  10782  absdivap  10810  bdtrilem  10978  isumrpcl  11231  expcnvap0  11239  absgtap  11247  cvgratz  11269  mertenslemi1  11272  effsumlt  11325  limcimolemlt  12729  trilpolemclim  13156  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator